:: ZFREFLE1 semantic presentation begin Lm1: {} in omega by ORDINAL1:def_11; Lm2: omega is limit_ordinal by ORDINAL1:def_11; definition let M be non empty set ; let F be Subset of WFF; predM |= F means :Def1: :: ZFREFLE1:def 1 for H being ZF-formula st H in F holds M |= H; end; :: deftheorem Def1 defines |= ZFREFLE1:def_1_:_ for M being non empty set for F being Subset of WFF holds ( M |= F iff for H being ZF-formula st H in F holds M |= H ); definition let M1, M2 be non empty set ; predM1 <==> M2 means :: ZFREFLE1:def 2 for H being ZF-formula st Free H = {} holds ( M1 |= H iff M2 |= H ); reflexivity for M1 being non empty set for H being ZF-formula st Free H = {} holds ( M1 |= H iff M1 |= H ) ; symmetry for M1, M2 being non empty set st ( for H being ZF-formula st Free H = {} holds ( M1 |= H iff M2 |= H ) ) holds for H being ZF-formula st Free H = {} holds ( M2 |= H iff M1 |= H ) ; predM1 is_elementary_subsystem_of M2 means :: ZFREFLE1:def 3 ( M1 c= M2 & ( for H being ZF-formula for v being Function of VAR,M1 holds ( M1,v |= H iff M2,M2 ! v |= H ) ) ); reflexivity for M1 being non empty set holds ( M1 c= M1 & ( for H being ZF-formula for v being Function of VAR,M1 holds ( M1,v |= H iff M1,M1 ! v |= H ) ) ) by ZF_LANG1:def_1; end; :: deftheorem defines <==> ZFREFLE1:def_2_:_ for M1, M2 being non empty set holds ( M1 <==> M2 iff for H being ZF-formula st Free H = {} holds ( M1 |= H iff M2 |= H ) ); :: deftheorem defines is_elementary_subsystem_of ZFREFLE1:def_3_:_ for M1, M2 being non empty set holds ( M1 is_elementary_subsystem_of M2 iff ( M1 c= M2 & ( for H being ZF-formula for v being Function of VAR,M1 holds ( M1,v |= H iff M2,M2 ! v |= H ) ) ) ); defpred S1[ set ] means ( \$1 = the_axiom_of_extensionality or \$1 = the_axiom_of_pairs or \$1 = the_axiom_of_unions or \$1 = the_axiom_of_infinity or \$1 = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & \$1 = the_axiom_of_substitution_for H ) ); definition func ZF-axioms -> set means :Def4: :: ZFREFLE1:def 4 for e being set holds ( e in it iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ); existence ex b1 being set st for e being set holds ( e in b1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) proof thus ex X being set st for e being set holds ( e in X iff ( e in WFF & S1[e] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ( for e being set holds ( e in b1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being set holds ( e in b2 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) holds b1 = b2 proof defpred S2[ set ] means ( \$1 in WFF & S1[\$1] ); let X1, X2 be set ; ::_thesis: ( ( for e being set holds ( e in X1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being set holds ( e in X2 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) implies X1 = X2 ) assume that A1: for e being set holds ( e in X1 iff S2[e] ) and A2: for e being set holds ( e in X2 iff S2[e] ) ; ::_thesis: X1 = X2 thus X1 = X2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum end; end; :: deftheorem Def4 defines ZF-axioms ZFREFLE1:def_4_:_ for b1 being set holds ( b1 = ZF-axioms iff for e being set holds ( e in b1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ); definition :: original: ZF-axioms redefine func ZF-axioms -> Subset of WFF; coherence ZF-axioms is Subset of WFF proof ZF-axioms c= WFF proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ZF-axioms or e in WFF ) thus ( not e in ZF-axioms or e in WFF ) by Def4; ::_thesis: verum end; hence ZF-axioms is Subset of WFF ; ::_thesis: verum end; end; theorem :: ZFREFLE1:1 for M being non empty set holds M |= {} WFF proof let M be non empty set ; ::_thesis: M |= {} WFF let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in {} WFF implies M |= H ) thus ( H in {} WFF implies M |= H ) ; ::_thesis: verum end; theorem :: ZFREFLE1:2 for M being non empty set for F1, F2 being Subset of WFF st F1 c= F2 & M |= F2 holds M |= F1 proof let M be non empty set ; ::_thesis: for F1, F2 being Subset of WFF st F1 c= F2 & M |= F2 holds M |= F1 let F1, F2 be Subset of WFF; ::_thesis: ( F1 c= F2 & M |= F2 implies M |= F1 ) assume A1: ( F1 c= F2 & M |= F2 ) ; ::_thesis: M |= F1 let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F1 implies M |= H ) assume H in F1 ; ::_thesis: M |= H hence M |= H by A1, Def1; ::_thesis: verum end; theorem :: ZFREFLE1:3 for M being non empty set for F1, F2 being Subset of WFF st M |= F1 & M |= F2 holds M |= F1 \/ F2 proof let M be non empty set ; ::_thesis: for F1, F2 being Subset of WFF st M |= F1 & M |= F2 holds M |= F1 \/ F2 let F1, F2 be Subset of WFF; ::_thesis: ( M |= F1 & M |= F2 implies M |= F1 \/ F2 ) assume A1: ( M |= F1 & M |= F2 ) ; ::_thesis: M |= F1 \/ F2 let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F1 \/ F2 implies M |= H ) assume H in F1 \/ F2 ; ::_thesis: M |= H then ( H in F1 or H in F2 ) by XBOOLE_0:def_3; hence M |= H by A1, Def1; ::_thesis: verum end; theorem Th4: :: ZFREFLE1:4 for M being non empty set st M is being_a_model_of_ZF holds M |= ZF-axioms proof let M be non empty set ; ::_thesis: ( M is being_a_model_of_ZF implies M |= ZF-axioms ) assume A1: ( M is epsilon-transitive & M |= the_axiom_of_pairs & M |= the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds M |= the_axiom_of_substitution_for H ) ) ; :: according to ZF_MODEL:def_12 ::_thesis: M |= ZF-axioms let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in ZF-axioms implies M |= H ) assume H in ZF-axioms ; ::_thesis: M |= H then ( H = the_axiom_of_extensionality or H = the_axiom_of_pairs or H = the_axiom_of_unions or H = the_axiom_of_infinity or H = the_axiom_of_power_sets or ex H1 being ZF-formula st ( {(x. 0),(x. 1),(x. 2)} misses Free H1 & H = the_axiom_of_substitution_for H1 ) ) by Def4; hence M |= H by A1, ZFMODEL1:1; ::_thesis: verum end; theorem Th5: :: ZFREFLE1:5 for M being non empty set st M |= ZF-axioms & M is epsilon-transitive holds M is being_a_model_of_ZF proof let M be non empty set ; ::_thesis: ( M |= ZF-axioms & M is epsilon-transitive implies M is being_a_model_of_ZF ) the_axiom_of_power_sets in WFF by ZF_LANG:4; then A1: the_axiom_of_power_sets in ZF-axioms by Def4; the_axiom_of_infinity in WFF by ZF_LANG:4; then A2: the_axiom_of_infinity in ZF-axioms by Def4; the_axiom_of_unions in WFF by ZF_LANG:4; then A3: the_axiom_of_unions in ZF-axioms by Def4; assume that A4: for H being ZF-formula st H in ZF-axioms holds M |= H and A5: M is epsilon-transitive ; :: according to ZFREFLE1:def_1 ::_thesis: M is being_a_model_of_ZF the_axiom_of_pairs in WFF by ZF_LANG:4; then the_axiom_of_pairs in ZF-axioms by Def4; hence ( M is epsilon-transitive & M |= the_axiom_of_pairs & M |= the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets ) by A4, A5, A3, A2, A1; :: according to ZF_MODEL:def_12 ::_thesis: for b1 being M7( NAT ) holds ( not {(x. 0),(x. 1),(x. 2)} misses Free b1 or M |= the_axiom_of_substitution_for b1 ) let H be ZF-formula; ::_thesis: ( not {(x. 0),(x. 1),(x. 2)} misses Free H or M |= the_axiom_of_substitution_for H ) assume A6: {(x. 0),(x. 1),(x. 2)} misses Free H ; ::_thesis: M |= the_axiom_of_substitution_for H the_axiom_of_substitution_for H in WFF by ZF_LANG:4; then the_axiom_of_substitution_for H in ZF-axioms by A6, Def4; hence M |= the_axiom_of_substitution_for H by A4; ::_thesis: verum end; theorem Th6: :: ZFREFLE1:6 for H being ZF-formula ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) proof let H be ZF-formula; ::_thesis: ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) defpred S2[ Element of NAT ] means for H being ZF-formula st card (Free H) = \$1 holds ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ); A1: for i being Element of NAT st S2[i] holds S2[i + 1] proof let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] ) assume A2: S2[i] ; ::_thesis: S2[i + 1] let H be ZF-formula; ::_thesis: ( card (Free H) = i + 1 implies ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) ) set e = the Element of Free H; assume A3: card (Free H) = i + 1 ; ::_thesis: ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) then A4: Free H <> {} by CARD_1:27, NAT_1:5; then reconsider x = the Element of Free H as Variable by TARSKI:def_3; A5: {x} c= Free H by A4, ZFMISC_1:31; A6: Free (All (x,H)) = (Free H) \ {x} by ZF_LANG1:62; x in {x} by ZFMISC_1:31; then A7: not x in Free (All (x,H)) by A6, XBOOLE_0:def_5; (Free (All (x,H))) \/ {x} = (Free H) \/ {x} by A6, XBOOLE_1:39; then (Free (All (x,H))) \/ {x} = Free H by A5, XBOOLE_1:12; then (card (Free (All (x,H)))) + 1 = card (Free H) by A7, CARD_2:41; then consider S being ZF-formula such that A8: Free S = {} and A9: for M being non empty set holds ( M |= S iff M |= All (x,H) ) by A2, A3, XCMPLX_1:2; take S ; ::_thesis: ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) thus Free S = {} by A8; ::_thesis: for M being non empty set holds ( M |= S iff M |= H ) let M be non empty set ; ::_thesis: ( M |= S iff M |= H ) ( M |= H iff M |= All (x,H) ) by ZF_MODEL:23; hence ( M |= S iff M |= H ) by A9; ::_thesis: verum end; A10: card (Free H) = card (Free H) ; A11: S2[ 0 ] proof let H be ZF-formula; ::_thesis: ( card (Free H) = 0 implies ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) ) assume A12: card (Free H) = 0 ; ::_thesis: ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) take H ; ::_thesis: ( Free H = {} & ( for M being non empty set holds ( M |= H iff M |= H ) ) ) thus ( Free H = {} & ( for M being non empty set holds ( M |= H iff M |= H ) ) ) by A12; ::_thesis: verum end; for i being Element of NAT holds S2[i] from NAT_1:sch_1(A11, A1); hence ex S being ZF-formula st ( Free S = {} & ( for M being non empty set holds ( M |= S iff M |= H ) ) ) by A10; ::_thesis: verum end; theorem :: ZFREFLE1:7 for M1, M2 being non empty set holds ( M1 <==> M2 iff for H being ZF-formula holds ( M1 |= H iff M2 |= H ) ) proof let M1, M2 be non empty set ; ::_thesis: ( M1 <==> M2 iff for H being ZF-formula holds ( M1 |= H iff M2 |= H ) ) thus ( M1 <==> M2 implies for H being ZF-formula holds ( M1 |= H iff M2 |= H ) ) ::_thesis: ( ( for H being ZF-formula holds ( M1 |= H iff M2 |= H ) ) implies M1 <==> M2 ) proof assume A1: for H being ZF-formula st Free H = {} holds ( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def_2 ::_thesis: for H being ZF-formula holds ( M1 |= H iff M2 |= H ) let H be ZF-formula; ::_thesis: ( M1 |= H iff M2 |= H ) consider S being ZF-formula such that A2: Free S = {} and A3: for M being non empty set holds ( M |= S iff M |= H ) by Th6; ( M1 |= S iff M2 |= S ) by A1, A2; hence ( M1 |= H iff M2 |= H ) by A3; ::_thesis: verum end; assume A4: for H being ZF-formula holds ( M1 |= H iff M2 |= H ) ; ::_thesis: M1 <==> M2 let H be ZF-formula; :: according to ZFREFLE1:def_2 ::_thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) thus ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) by A4; ::_thesis: verum end; theorem Th8: :: ZFREFLE1:8 for M1, M2 being non empty set holds ( M1 <==> M2 iff for F being Subset of WFF holds ( M1 |= F iff M2 |= F ) ) proof let M1, M2 be non empty set ; ::_thesis: ( M1 <==> M2 iff for F being Subset of WFF holds ( M1 |= F iff M2 |= F ) ) thus ( M1 <==> M2 implies for F being Subset of WFF holds ( M1 |= F iff M2 |= F ) ) ::_thesis: ( ( for F being Subset of WFF holds ( M1 |= F iff M2 |= F ) ) implies M1 <==> M2 ) proof assume A1: for H being ZF-formula st Free H = {} holds ( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def_2 ::_thesis: for F being Subset of WFF holds ( M1 |= F iff M2 |= F ) let F be Subset of WFF; ::_thesis: ( M1 |= F iff M2 |= F ) thus ( M1 |= F implies M2 |= F ) ::_thesis: ( M2 |= F implies M1 |= F ) proof assume A2: for H being ZF-formula st H in F holds M1 |= H ; :: according to ZFREFLE1:def_1 ::_thesis: M2 |= F let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F implies M2 |= H ) consider S being ZF-formula such that A3: Free S = {} and A4: for M being non empty set holds ( M |= S iff M |= H ) by Th6; assume H in F ; ::_thesis: M2 |= H then M1 |= H by A2; then M1 |= S by A4; then M2 |= S by A1, A3; hence M2 |= H by A4; ::_thesis: verum end; assume A5: for H being ZF-formula st H in F holds M2 |= H ; :: according to ZFREFLE1:def_1 ::_thesis: M1 |= F let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F implies M1 |= H ) consider S being ZF-formula such that A6: Free S = {} and A7: for M being non empty set holds ( M |= S iff M |= H ) by Th6; assume H in F ; ::_thesis: M1 |= H then M2 |= H by A5; then M2 |= S by A7; then M1 |= S by A1, A6; hence M1 |= H by A7; ::_thesis: verum end; assume A8: for F being Subset of WFF holds ( M1 |= F iff M2 |= F ) ; ::_thesis: M1 <==> M2 let H be ZF-formula; :: according to ZFREFLE1:def_2 ::_thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) assume Free H = {} ; ::_thesis: ( M1 |= H iff M2 |= H ) H in WFF by ZF_LANG:4; then reconsider F = {H} as Subset of WFF by ZFMISC_1:31; thus ( M1 |= H implies M2 |= H ) ::_thesis: ( M2 |= H implies M1 |= H ) proof assume M1 |= H ; ::_thesis: M2 |= H then for S being ZF-formula st S in F holds M1 |= S by TARSKI:def_1; then M1 |= F by Def1; then A9: M2 |= F by A8; H in F by TARSKI:def_1; hence M2 |= H by A9, Def1; ::_thesis: verum end; assume M2 |= H ; ::_thesis: M1 |= H then for S being ZF-formula st S in F holds M2 |= S by TARSKI:def_1; then M2 |= F by Def1; then A10: M1 |= F by A8; H in F by TARSKI:def_1; hence M1 |= H by A10, Def1; ::_thesis: verum end; theorem Th9: :: ZFREFLE1:9 for M1, M2 being non empty set st M1 is_elementary_subsystem_of M2 holds M1 <==> M2 proof let M1, M2 be non empty set ; ::_thesis: ( M1 is_elementary_subsystem_of M2 implies M1 <==> M2 ) assume that M1 c= M2 and A1: for H being ZF-formula for v being Function of VAR,M1 holds ( M1,v |= H iff M2,M2 ! v |= H ) ; :: according to ZFREFLE1:def_3 ::_thesis: M1 <==> M2 let H be ZF-formula; :: according to ZFREFLE1:def_2 ::_thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) assume A2: Free H = {} ; ::_thesis: ( M1 |= H iff M2 |= H ) thus ( M1 |= H implies M2 |= H ) ::_thesis: ( M2 |= H implies M1 |= H ) proof assume A3: for v1 being Function of VAR,M1 holds M1,v1 |= H ; :: according to ZF_MODEL:def_5 ::_thesis: M2 |= H set v1 = the Function of VAR,M1; M1, the Function of VAR,M1 |= H by A3; then A4: M2,M2 ! the Function of VAR,M1 |= H by A1; let v2 be Function of VAR,M2; :: according to ZF_MODEL:def_5 ::_thesis: M2,v2 |= H for x being Variable st x in Free H holds v2 . x = (M2 ! the Function of VAR,M1) . x by A2; hence M2,v2 |= H by A4, ZF_LANG1:75; ::_thesis: verum end; assume A5: for v2 being Function of VAR,M2 holds M2,v2 |= H ; :: according to ZF_MODEL:def_5 ::_thesis: M1 |= H let v1 be Function of VAR,M1; :: according to ZF_MODEL:def_5 ::_thesis: M1,v1 |= H M2,M2 ! v1 |= H by A5; hence M1,v1 |= H by A1; ::_thesis: verum end; theorem Th10: :: ZFREFLE1:10 for M1, M2 being non empty set st M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive holds M2 is being_a_model_of_ZF proof let M1, M2 be non empty set ; ::_thesis: ( M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive implies M2 is being_a_model_of_ZF ) assume that A1: M1 is being_a_model_of_ZF and A2: M1 <==> M2 ; ::_thesis: ( not M2 is epsilon-transitive or M2 is being_a_model_of_ZF ) M1 |= ZF-axioms by A1, Th4; then M2 |= ZF-axioms by A2, Th8; hence ( not M2 is epsilon-transitive or M2 is being_a_model_of_ZF ) by Th5; ::_thesis: verum end; theorem Th11: :: ZFREFLE1:11 for f being Function for W being Universe st dom f in W & rng f c= W holds rng f in W proof let f be Function; ::_thesis: for W being Universe st dom f in W & rng f c= W holds rng f in W let W be Universe; ::_thesis: ( dom f in W & rng f c= W implies rng f in W ) assume dom f in W ; ::_thesis: ( not rng f c= W or rng f in W ) then ( rng f = f .: (dom f) & card (dom f) in card W ) by CLASSES2:1, RELAT_1:113; then card (rng f) in card W by CARD_1:67, ORDINAL1:12; hence ( not rng f c= W or rng f in W ) by CLASSES1:1; ::_thesis: verum end; theorem :: ZFREFLE1:12 for X, Y being set st ( X,Y are_equipotent or card X = card Y ) holds ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) proof let X, Y be set ; ::_thesis: ( ( X,Y are_equipotent or card X = card Y ) implies ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) ) assume ( X,Y are_equipotent or card X = card Y ) ; ::_thesis: ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) then X,Y are_equipotent by CARD_1:5; then A1: card (Funcs (X,{0,1})) = card (Funcs (Y,{0,1})) by FUNCT_5:60; ( card (Funcs (X,{0,1})) = card (bool X) & card (Funcs (Y,{0,1})) = card (bool Y) ) by FUNCT_5:65; hence ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) by A1, CARD_1:5; ::_thesis: verum end; theorem Th13: :: ZFREFLE1:13 for W being Universe for D being non empty set for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) proof let W be Universe; ::_thesis: for D being non empty set for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) deffunc H1( set , T-Sequence) -> set = sup \$2; let D be non empty set ; ::_thesis: for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) let Phi be Function of D,(Funcs ((On W),(On W))); ::_thesis: ( card D in card W implies ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) ) assume A1: card D in card W ; ::_thesis: ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) deffunc H2( Ordinal, Ordinal) -> set = sup ({\$2} \/ ((uncurry Phi) .: [:D,{(succ \$1)}:])); consider L being Ordinal-Sequence such that A2: ( dom L = On W & ( {} in On W implies L . {} = {} ) ) and A3: for A being Ordinal st succ A in On W holds L . (succ A) = H2(A,L . A) and A4: for A being Ordinal st A in On W & A <> {} & A is limit_ordinal holds L . A = H1(A,L | A) from ORDINAL2:sch_11(); defpred S2[ Ordinal] means L . \$1 in On W; A5: for a being Ordinal of W st S2[a] holds S2[ succ a] proof let a be Ordinal of W; ::_thesis: ( S2[a] implies S2[ succ a] ) A6: On W c= W by ORDINAL2:7; assume L . a in On W ; ::_thesis: S2[ succ a] then reconsider b = L . a as Ordinal of W by ZF_REFLE:7; card [:D,{(succ a)}:] = card D by CARD_1:69; then card ((uncurry Phi) .: [:D,{(succ a)}:]) c= card D by CARD_1:66; then A7: card ((uncurry Phi) .: [:D,{(succ a)}:]) in card W by A1, ORDINAL1:12; rng Phi c= Funcs ((On W),(On W)) by RELAT_1:def_19; then A8: rng (uncurry Phi) c= On W by FUNCT_5:41; (uncurry Phi) .: [:D,{(succ a)}:] c= rng (uncurry Phi) by RELAT_1:111; then (uncurry Phi) .: [:D,{(succ a)}:] c= On W by A8, XBOOLE_1:1; then (uncurry Phi) .: [:D,{(succ a)}:] c= W by A6, XBOOLE_1:1; then (uncurry Phi) .: [:D,{(succ a)}:] in W by A7, CLASSES1:1; then A9: {b} \/ ((uncurry Phi) .: [:D,{(succ a)}:]) in W by CLASSES2:60; succ a in On W by ZF_REFLE:7; then L . (succ a) = sup ({b} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3; then L . (succ a) in W by A9, ZF_REFLE:19; hence S2[ succ a] by ORDINAL1:def_9; ::_thesis: verum end; A10: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds S2[b] ) holds S2[a] proof let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds S2[b] ) implies S2[a] ) assume that A11: ( a <> 0-element_of W & a is limit_ordinal ) and A12: for b being Ordinal of W st b in a holds L . b in On W ; ::_thesis: S2[a] A13: dom (L | a) c= a by RELAT_1:58; then A14: dom (L | a) in W by CLASSES1:def_1; A15: a in On W by ZF_REFLE:7; A16: rng (L | a) c= W proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (L | a) or e in W ) assume e in rng (L | a) ; ::_thesis: e in W then consider u being set such that A17: u in dom (L | a) and A18: e = (L | a) . u by FUNCT_1:def_3; reconsider u = u as Ordinal by A17; u in On W by A15, A13, A17, ORDINAL1:10; then reconsider u = u as Ordinal of W by ZF_REFLE:7; e = L . u by A17, A18, FUNCT_1:47; then e in On W by A12, A13, A17; hence e in W by ORDINAL1:def_9; ::_thesis: verum end; L . a = sup (L | a) by A4, A11, A15; then L . a in W by A14, A16, Th11, ZF_REFLE:19; hence S2[a] by ORDINAL1:def_9; ::_thesis: verum end; A19: S2[ 0-element_of W] by A2, ORDINAL1:def_9; rng L c= On W proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng L or e in On W ) assume e in rng L ; ::_thesis: e in On W then consider u being set such that A20: u in dom L and A21: e = L . u by FUNCT_1:def_3; reconsider u = u as Ordinal of W by A2, A20, ZF_REFLE:7; for a being Ordinal of W holds S2[a] from ZF_REFLE:sch_4(A19, A5, A10); then L . u in On W ; hence e in On W by A21; ::_thesis: verum end; then reconsider phi = L as Ordinal-Sequence of W by A2, FUNCT_2:def_1, RELSET_1:4; take phi ; ::_thesis: ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) thus A22: phi is increasing ::_thesis: ( phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) proof let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds ( not A in b1 or not b1 in dom phi or phi . A in phi . b1 ) let B be Ordinal; ::_thesis: ( not A in B or not B in dom phi or phi . A in phi . B ) assume that A23: A in B and A24: B in dom phi ; ::_thesis: phi . A in phi . B A in dom phi by A23, A24, ORDINAL1:10; then reconsider a = A, b = B as Ordinal of W by A2, A24, ZF_REFLE:7; defpred S3[ Ordinal] means ( a in \$1 implies phi . a in phi . \$1 ); A25: for b being Ordinal of W st S3[b] holds S3[ succ b] proof let b be Ordinal of W; ::_thesis: ( S3[b] implies S3[ succ b] ) assume A26: ( ( a in b implies phi . a in phi . b ) & a in succ b ) ; ::_thesis: phi . a in phi . (succ b) phi . b in {(phi . b)} by TARSKI:def_1; then A27: phi . b in {(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:]) by XBOOLE_0:def_3; succ b in On W by ZF_REFLE:7; then phi . (succ b) = sup ({(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:])) by A3; then phi . b in phi . (succ b) by A27, ORDINAL2:19; hence phi . a in phi . (succ b) by A26, ORDINAL1:8, ORDINAL1:10; ::_thesis: verum end; A28: for b being Ordinal of W st b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds S3[c] ) holds S3[b] proof let b be Ordinal of W; ::_thesis: ( b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds S3[c] ) implies S3[b] ) assume that A29: ( b <> 0-element_of W & b is limit_ordinal ) and for c being Ordinal of W st c in b & a in c holds phi . a in phi . c and A30: a in b ; ::_thesis: phi . a in phi . b b in On W by ZF_REFLE:7; then A31: phi . b = sup (phi | b) by A4, A29; a in On W by ZF_REFLE:7; then phi . a in rng (phi | b) by A2, A30, FUNCT_1:50; hence phi . a in phi . b by A31, ORDINAL2:19; ::_thesis: verum end; A32: S3[ 0-element_of W] ; for b being Ordinal of W holds S3[b] from ZF_REFLE:sch_4(A32, A25, A28); then phi . a in phi . b by A23; hence phi . A in phi . B ; ::_thesis: verum end; thus phi is continuous ::_thesis: ( phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) proof let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds ( not A in dom phi or A = {} or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A ) let B be Ordinal; ::_thesis: ( not A in dom phi or A = {} or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A ) assume that A33: A in dom phi and A34: ( A <> {} & A is limit_ordinal ) and A35: B = phi . A ; ::_thesis: B is_limes_of phi | A A c= dom phi by A33, ORDINAL1:def_2; then A36: dom (phi | A) = A by RELAT_1:62; A37: phi | A is increasing by A22, ORDINAL4:15; B = sup (phi | A) by A2, A4, A33, A34, A35; hence B is_limes_of phi | A by A34, A36, A37, ORDINAL4:8; ::_thesis: verum end; thus phi . (0-element_of W) = 0-element_of W by A2, ORDINAL1:def_9; ::_thesis: ( ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) ) ) thus for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ::_thesis: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) proof let a be Ordinal of W; ::_thesis: phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) succ a in On W by ZF_REFLE:7; hence phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3; ::_thesis: verum end; let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) ) a in On W by ZF_REFLE:7; hence ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) ) by A4; ::_thesis: verum end; theorem Th14: :: ZFREFLE1:14 for C being Ordinal for phi being Ordinal-Sequence st phi is increasing holds C +^ phi is increasing proof let C be Ordinal; ::_thesis: for phi being Ordinal-Sequence st phi is increasing holds C +^ phi is increasing let phi be Ordinal-Sequence; ::_thesis: ( phi is increasing implies C +^ phi is increasing ) assume A1: phi is increasing ; ::_thesis: C +^ phi is increasing let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds ( not A in b1 or not b1 in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . b1 ) let B be Ordinal; ::_thesis: ( not A in B or not B in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . B ) set xi = C +^ phi; assume that A2: A in B and A3: B in dom (C +^ phi) ; ::_thesis: (C +^ phi) . A in (C +^ phi) . B reconsider A9 = phi . A, B9 = phi . B as Ordinal ; A4: dom (C +^ phi) = dom phi by ORDINAL3:def_1; then A5: (C +^ phi) . B = C +^ B9 by A3, ORDINAL3:def_1; A in dom (C +^ phi) by A2, A3, ORDINAL1:10; then A6: (C +^ phi) . A = C +^ A9 by A4, ORDINAL3:def_1; A9 in B9 by A1, A2, A3, A4, ORDINAL2:def_12; hence (C +^ phi) . A in (C +^ phi) . B by A6, A5, ORDINAL2:32; ::_thesis: verum end; theorem Th15: :: ZFREFLE1:15 for C, A being Ordinal for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A) proof let C, A be Ordinal; ::_thesis: for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A) let xi be Ordinal-Sequence; ::_thesis: (C +^ xi) | A = C +^ (xi | A) A1: dom (xi | A) = (dom xi) /\ A by RELAT_1:61; A2: dom (C +^ xi) = dom xi by ORDINAL3:def_1; A3: dom ((C +^ xi) | A) = (dom (C +^ xi)) /\ A by RELAT_1:61; A4: now__::_thesis:_for_e_being_set_st_e_in_dom_((C_+^_xi)_|_A)_holds_ ((C_+^_xi)_|_A)_._e_=_(C_+^_(xi_|_A))_._e let e be set ; ::_thesis: ( e in dom ((C +^ xi) | A) implies ((C +^ xi) | A) . e = (C +^ (xi | A)) . e ) assume A5: e in dom ((C +^ xi) | A) ; ::_thesis: ((C +^ xi) | A) . e = (C +^ (xi | A)) . e then reconsider a = e as Ordinal ; A6: e in dom xi by A3, A2, A5, XBOOLE_0:def_4; thus ((C +^ xi) | A) . e = (C +^ xi) . a by A5, FUNCT_1:47 .= C +^ (xi . a) by A6, ORDINAL3:def_1 .= C +^ ((xi | A) . a) by A3, A1, A2, A5, FUNCT_1:47 .= (C +^ (xi | A)) . e by A3, A1, A2, A5, ORDINAL3:def_1 ; ::_thesis: verum end; dom (C +^ (xi | A)) = dom (xi | A) by ORDINAL3:def_1; hence (C +^ xi) | A = C +^ (xi | A) by A1, A2, A4, FUNCT_1:2, RELAT_1:61; ::_thesis: verum end; theorem Th16: :: ZFREFLE1:16 for C being Ordinal for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds C +^ phi is continuous proof let C be Ordinal; ::_thesis: for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds C +^ phi is continuous let phi be Ordinal-Sequence; ::_thesis: ( phi is increasing & phi is continuous implies C +^ phi is continuous ) assume A1: phi is increasing ; ::_thesis: ( not phi is continuous or C +^ phi is continuous ) assume A2: for A, B being Ordinal st A in dom phi & A <> {} & A is limit_ordinal & B = phi . A holds B is_limes_of phi | A ; :: according to ORDINAL2:def_13 ::_thesis: C +^ phi is continuous let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds ( not A in dom (C +^ phi) or A = {} or not A is limit_ordinal or not b1 = (C +^ phi) . A or b1 is_limes_of (C +^ phi) | A ) let B be Ordinal; ::_thesis: ( not A in dom (C +^ phi) or A = {} or not A is limit_ordinal or not B = (C +^ phi) . A or B is_limes_of (C +^ phi) | A ) set xi = phi | A; reconsider A9 = phi . A as Ordinal ; assume that A3: A in dom (C +^ phi) and A4: A <> {} and A5: A is limit_ordinal and A6: B = (C +^ phi) . A ; ::_thesis: B is_limes_of (C +^ phi) | A A7: dom phi = dom (C +^ phi) by ORDINAL3:def_1; then A8: B = C +^ A9 by A3, A6, ORDINAL3:def_1; A9 is_limes_of phi | A by A2, A3, A4, A5, A7; then A9: lim (phi | A) = A9 by ORDINAL2:def_10; A10: ( dom (phi | A) = dom (C +^ (phi | A)) & (C +^ phi) | A = C +^ (phi | A) ) by Th15, ORDINAL3:def_1; A11: phi | A is increasing by A1, ORDINAL4:15; then A12: C +^ (phi | A) is increasing by Th14; A c= dom (C +^ phi) by A3, ORDINAL1:def_2; then A13: dom (phi | A) = A by A7, RELAT_1:62; then A14: sup (C +^ (phi | A)) = C +^ (sup (phi | A)) by A4, ORDINAL3:43; sup (phi | A) = lim (phi | A) by A4, A5, A13, A11, ORDINAL4:8; hence B is_limes_of (C +^ phi) | A by A4, A5, A13, A10, A8, A14, A9, A12, ORDINAL4:8; ::_thesis: verum end; theorem :: ZFREFLE1:17 for e being set for psi being Ordinal-Sequence st e in rng psi holds e is Ordinal by ORDINAL2:48; theorem :: ZFREFLE1:18 for psi being Ordinal-Sequence holds rng psi c= sup psi by ORDINAL2:49; theorem :: ZFREFLE1:19 for A, B, C being Ordinal st A is_cofinal_with B & B is_cofinal_with C holds A is_cofinal_with C by ORDINAL4:37; theorem Th20: :: ZFREFLE1:20 for A, B being Ordinal st A is_cofinal_with B holds B c= A proof let A, B be Ordinal; ::_thesis: ( A is_cofinal_with B implies B c= A ) given psi being Ordinal-Sequence such that A1: dom psi = B and A2: rng psi c= A and A3: psi is increasing and A = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: B c= A let C be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not C in B or C in A ) assume C in B ; ::_thesis: C in A then ( C c= psi . C & psi . C in rng psi ) by A1, A3, FUNCT_1:def_3, ORDINAL4:10; hence C in A by A2, ORDINAL1:12; ::_thesis: verum end; theorem :: ZFREFLE1:21 for A, B being Ordinal st A is_cofinal_with B & B is_cofinal_with A holds A = B proof let A, B be Ordinal; ::_thesis: ( A is_cofinal_with B & B is_cofinal_with A implies A = B ) assume ( A is_cofinal_with B & B is_cofinal_with A ) ; ::_thesis: A = B hence ( A c= B & B c= A ) by Th20; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem :: ZFREFLE1:22 for A being Ordinal for psi being Ordinal-Sequence st dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi holds A is_cofinal_with dom psi proof let A be Ordinal; ::_thesis: for psi being Ordinal-Sequence st dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi holds A is_cofinal_with dom psi let psi be Ordinal-Sequence; ::_thesis: ( dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi implies A is_cofinal_with dom psi ) assume that A1: ( dom psi <> {} & dom psi is limit_ordinal ) and A2: psi is increasing and A3: A is_limes_of psi ; ::_thesis: A is_cofinal_with dom psi take psi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom psi = dom psi & rng psi c= A & psi is increasing & A = sup psi ) thus dom psi = dom psi ; ::_thesis: ( rng psi c= A & psi is increasing & A = sup psi ) ( sup psi = lim psi & A = lim psi ) by A1, A2, A3, ORDINAL2:def_10, ORDINAL4:8; hence ( rng psi c= A & psi is increasing & A = sup psi ) by A2, ORDINAL2:49; ::_thesis: verum end; theorem :: ZFREFLE1:23 for A being Ordinal holds succ A is_cofinal_with 1 by ORDINAL3:73; theorem :: ZFREFLE1:24 for A, B being Ordinal st A is_cofinal_with succ B holds ex C being Ordinal st A = succ C proof let A, B be Ordinal; ::_thesis: ( A is_cofinal_with succ B implies ex C being Ordinal st A = succ C ) given psi being Ordinal-Sequence such that A1: dom psi = succ B and A2: rng psi c= A and A3: psi is increasing and A4: A = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: ex C being Ordinal st A = succ C reconsider C = psi . B as Ordinal ; take C ; ::_thesis: A = succ C thus A c= succ C :: according to XBOOLE_0:def_10 ::_thesis: succ C c= A proof let a be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not a in A or a in succ C ) assume a in A ; ::_thesis: a in succ C then consider b being Ordinal such that A5: b in rng psi and A6: a c= b by A4, ORDINAL2:21; consider e being set such that A7: e in succ B and A8: b = psi . e by A1, A5, FUNCT_1:def_3; reconsider e = e as Ordinal by A7; e c= B by A7, ORDINAL1:22; then b c= C by A1, A3, A8, ORDINAL1:6, ORDINAL4:9; then b in succ C by ORDINAL1:22; hence a in succ C by A6, ORDINAL1:12; ::_thesis: verum end; B in succ B by ORDINAL1:6; then C in rng psi by A1, FUNCT_1:def_3; hence succ C c= A by A2, ORDINAL1:21; ::_thesis: verum end; theorem :: ZFREFLE1:25 for A, B being Ordinal st A is_cofinal_with B holds ( A is limit_ordinal iff B is limit_ordinal ) by ORDINAL4:38; theorem :: ZFREFLE1:26 for A being Ordinal st A is_cofinal_with {} holds A = {} by ORDINAL2:50; theorem :: ZFREFLE1:27 for W being Universe for a being Ordinal of W holds not On W is_cofinal_with a proof let W be Universe; ::_thesis: for a being Ordinal of W holds not On W is_cofinal_with a let a be Ordinal of W; ::_thesis: not On W is_cofinal_with a given psi being Ordinal-Sequence such that A1: dom psi = a and A2: rng psi c= On W and psi is increasing and A3: On W = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: contradiction On W c= W by ORDINAL2:7; then rng psi c= W by A2, XBOOLE_1:1; then sup (rng psi) in W by A1, Th11, ZF_REFLE:19; then sup psi in On W by ORDINAL1:def_9; hence contradiction by A3; ::_thesis: verum end; theorem Th28: :: ZFREFLE1:28 for W being Universe for a being Ordinal of W for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds ex b being Ordinal of W st ( a in b & phi . b = b ) proof let W be Universe; ::_thesis: for a being Ordinal of W for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds ex b being Ordinal of W st ( a in b & phi . b = b ) let a be Ordinal of W; ::_thesis: for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds ex b being Ordinal of W st ( a in b & phi . b = b ) let phi be Ordinal-Sequence of W; ::_thesis: ( omega in W & phi is increasing & phi is continuous implies ex b being Ordinal of W st ( a in b & phi . b = b ) ) assume that A1: omega in W and A2: phi is increasing and A3: phi is continuous ; ::_thesis: ex b being Ordinal of W st ( a in b & phi . b = b ) deffunc H1( Ordinal of W) -> Element of W = (succ a) +^ (phi . \$1); consider xi being Ordinal-Sequence of W such that A4: for b being Ordinal of W holds xi . b = H1(b) from ORDINAL4:sch_2(); A5: dom xi = On W by FUNCT_2:def_1; A6: dom phi = On W by FUNCT_2:def_1; for A being Ordinal st A in dom phi holds xi . A = (succ a) +^ (phi . A) proof let A be Ordinal; ::_thesis: ( A in dom phi implies xi . A = (succ a) +^ (phi . A) ) assume A in dom phi ; ::_thesis: xi . A = (succ a) +^ (phi . A) then reconsider b = A as Ordinal of W by A6, ZF_REFLE:7; xi . b = (succ a) +^ (phi . b) by A4; hence xi . A = (succ a) +^ (phi . A) ; ::_thesis: verum end; then xi = (succ a) +^ phi by A6, A5, ORDINAL3:def_1; then ( xi is increasing & xi is continuous ) by A2, A3, Th14, Th16; then consider A being Ordinal such that A7: A in dom xi and A8: xi . A = A by A1, ORDINAL4:36; reconsider b = A as Ordinal of W by A5, A7, ZF_REFLE:7; A9: b = (succ a) +^ (phi . b) by A4, A8; take b ; ::_thesis: ( a in b & phi . b = b ) A10: ( succ a c= (succ a) +^ (phi . b) & a in succ a ) by ORDINAL1:6, ORDINAL3:24; A11: phi . b c= (succ a) +^ (phi . b) by ORDINAL3:24; b c= phi . b by A2, A6, A5, A7, ORDINAL4:10; hence ( a in b & phi . b = b ) by A10, A9, A11, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th29: :: ZFREFLE1:29 for W being Universe for b being Ordinal of W for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds ex a being Ordinal of W st ( b in a & phi . a = a & a is_cofinal_with omega ) proof let W be Universe; ::_thesis: for b being Ordinal of W for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds ex a being Ordinal of W st ( b in a & phi . a = a & a is_cofinal_with omega ) let b be Ordinal of W; ::_thesis: for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds ex a being Ordinal of W st ( b in a & phi . a = a & a is_cofinal_with omega ) let phi be Ordinal-Sequence of W; ::_thesis: ( omega in W & phi is increasing & phi is continuous implies ex a being Ordinal of W st ( b in a & phi . a = a & a is_cofinal_with omega ) ) assume that A1: omega in W and A2: phi is increasing and A3: phi is continuous ; ::_thesis: ex a being Ordinal of W st ( b in a & phi . a = a & a is_cofinal_with omega ) A4: omega in On W by A1, ORDINAL1:def_9; deffunc H1( Ordinal, set ) -> Element of W = 0-element_of W; deffunc H2( Ordinal, Ordinal of W) -> Element of W = succ (phi . \$2); consider nu being Ordinal-Sequence of W such that A5: nu . (0-element_of W) = b and A6: for a being Ordinal of W holds nu . (succ a) = H2(a,nu . a) and for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds nu . a = H1(a,nu | a) from ZF_REFLE:sch_3(); set xi = nu | omega; set a = sup (nu | omega); A7: On W c= W by ORDINAL2:7; dom nu = On W by FUNCT_2:def_1; then A8: omega c= dom nu by A4; then A9: dom (nu | omega) = omega by RELAT_1:62; ( rng (nu | omega) c= rng nu & rng nu c= On W ) by RELAT_1:def_19; then rng (nu | omega) c= On W by XBOOLE_1:1; then rng (nu | omega) c= W by A7, XBOOLE_1:1; then reconsider a = sup (nu | omega) as Ordinal of W by A1, A9, Th11, ZF_REFLE:19; A10: a in dom phi by ORDINAL4:34; then A11: a c= dom phi by ORDINAL1:def_2; then A12: dom (phi | a) = a by RELAT_1:62; A13: nu | omega is increasing proof let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds ( not A in b1 or not b1 in dom (nu | omega) or (nu | omega) . A in (nu | omega) . b1 ) let B be Ordinal; ::_thesis: ( not A in B or not B in dom (nu | omega) or (nu | omega) . A in (nu | omega) . B ) assume that A14: A in B and A15: B in dom (nu | omega) ; ::_thesis: (nu | omega) . A in (nu | omega) . B defpred S2[ Ordinal] means ( A +^ \$1 in dom (nu | omega) & \$1 <> {} implies (nu | omega) . A in (nu | omega) . (A +^ \$1) ); A16: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds S2[C] ) holds S2[B] proof let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds S2[C] ) implies S2[B] ) assume that A17: B <> {} and A18: B is limit_ordinal ; ::_thesis: ( ex C being Ordinal st ( C in B & not S2[C] ) or S2[B] ) {} in B by A17, ORDINAL3:8; then A19: omega c= B by A18, ORDINAL1:def_11; B c= A +^ B by ORDINAL3:24; hence ( ex C being Ordinal st ( C in B & not S2[C] ) or S2[B] ) by A9, A19, ORDINAL1:5; ::_thesis: verum end; A20: for C being Ordinal st S2[C] holds S2[ succ C] proof let C be Ordinal; ::_thesis: ( S2[C] implies S2[ succ C] ) assume that A21: ( A +^ C in dom (nu | omega) & C <> {} implies (nu | omega) . A in (nu | omega) . (A +^ C) ) and A22: A +^ (succ C) in dom (nu | omega) and succ C <> {} ; ::_thesis: (nu | omega) . A in (nu | omega) . (A +^ (succ C)) A23: A +^ (succ C) in On W by A4, A9, A22, ORDINAL1:10; then reconsider asc = A +^ (succ C) as Ordinal of W by ZF_REFLE:7; A24: A +^ C in asc by ORDINAL1:6, ORDINAL2:32; then A +^ C in On W by A23, ORDINAL1:10; then reconsider ac = A +^ C as Ordinal of W by ZF_REFLE:7; A25: now__::_thesis:_(_C_=_{}_implies_(nu_|_omega)_._A_in_(nu_|_omega)_._(A_+^_(succ_C))_) nu . ac in dom phi by ORDINAL4:34; then A26: nu . ac c= phi . (nu . ac) by A2, ORDINAL4:10; asc = succ ac by ORDINAL2:28; then A27: nu . asc = succ (phi . (nu . ac)) by A6; assume C = {} ; ::_thesis: (nu | omega) . A in (nu | omega) . (A +^ (succ C)) then A28: ac = A by ORDINAL2:27; ( (nu | omega) . ac = nu . ac & (nu | omega) . asc = nu . asc ) by A22, A24, FUNCT_1:47, ORDINAL1:10; hence (nu | omega) . A in (nu | omega) . (A +^ (succ C)) by A28, A27, A26, ORDINAL1:6, ORDINAL1:12; ::_thesis: verum end; A29: ( succ ac = asc & nu . ac in dom phi ) by ORDINAL2:28, ORDINAL4:34; A +^ C in dom (nu | omega) by A22, A24, ORDINAL1:10; then ( ( (nu | omega) . A in (nu | omega) . ac & nu . asc = succ (phi . (nu . ac)) & nu . ac = (nu | omega) . ac & phi . (nu . ac) in succ (phi . (nu . ac)) & nu . ac c= phi . (nu . ac) ) or C = {} ) by A2, A6, A21, A29, FUNCT_1:47, ORDINAL1:6, ORDINAL4:10; then ( ( (nu | omega) . A in nu . ac & nu . ac in nu . asc & nu . asc = (nu | omega) . asc ) or C = {} ) by A22, FUNCT_1:47, ORDINAL1:12; then ( ( (nu | omega) . A in nu . ac & nu . ac c= (nu | omega) . asc ) or C = {} ) by ORDINAL1:def_2; hence (nu | omega) . A in (nu | omega) . (A +^ (succ C)) by A25; ::_thesis: verum end; A30: S2[ {} ] ; A31: for C being Ordinal holds S2[C] from ORDINAL2:sch_1(A30, A20, A16); ex C being Ordinal st ( B = A +^ C & C <> {} ) by A14, ORDINAL3:28; hence (nu | omega) . A in (nu | omega) . B by A15, A31; ::_thesis: verum end; then A32: a is limit_ordinal by A9, Lm2, ORDINAL4:16; take a ; ::_thesis: ( b in a & phi . a = a & a is_cofinal_with omega ) 0-element_of W in dom nu by ORDINAL4:34; then A33: b in rng (nu | omega) by A5, Lm1, FUNCT_1:50; hence b in a by ORDINAL2:19; ::_thesis: ( phi . a = a & a is_cofinal_with omega ) A34: a <> {} by A33, ORDINAL2:19; a in dom phi by ORDINAL4:34; then A35: phi . a is_limes_of phi | a by A3, A32, A34, ORDINAL2:def_13; phi | a is increasing by A2, ORDINAL4:15; then sup (phi | a) = lim (phi | a) by A32, A34, A12, ORDINAL4:8; then A36: phi . a = sup (rng (phi | a)) by A35, ORDINAL2:def_10; thus phi . a c= a :: according to XBOOLE_0:def_10 ::_thesis: ( a c= phi . a & a is_cofinal_with omega ) proof let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in phi . a or A in a ) assume A in phi . a ; ::_thesis: A in a then consider B being Ordinal such that A37: B in rng (phi | a) and A38: A c= B by A36, ORDINAL2:21; consider e being set such that A39: e in a and A40: B = (phi | a) . e by A12, A37, FUNCT_1:def_3; reconsider e = e as Ordinal by A39; consider C being Ordinal such that A41: C in rng (nu | omega) and A42: e c= C by A39, ORDINAL2:21; A43: ( e c< C iff ( e c= C & e <> C ) ) by XBOOLE_0:def_8; consider u being set such that A44: u in omega and A45: C = (nu | omega) . u by A9, A41, FUNCT_1:def_3; reconsider u = u as Ordinal by A44; u c= omega by A44, ORDINAL1:def_2; then reconsider u = u as Ordinal of W by A1, CLASSES1:def_1; A46: succ u in dom nu by ORDINAL4:34; C in a by A41, ORDINAL2:19; then ( e = C or ( e in C & C in dom phi ) ) by A11, A42, A43, ORDINAL1:11; then A47: ( phi . e = phi . C or phi . e in phi . C ) by A2, ORDINAL2:def_12; A48: nu . (succ u) = succ (phi . (nu . u)) by A6; succ u in omega by A44, Lm2, ORDINAL1:28; then nu . (succ u) in rng (nu | omega) by A46, FUNCT_1:50; then A49: nu . (succ u) in a by ORDINAL2:19; C = nu . u by A9, A44, A45, FUNCT_1:47; then A50: phi . e c= phi . (nu . u) by A47, ORDINAL1:def_2; phi . e = B by A12, A39, A40, FUNCT_1:47; then B in nu . (succ u) by A48, A50, ORDINAL1:6, ORDINAL1:12; then B in a by A49, ORDINAL1:10; hence A in a by A38, ORDINAL1:12; ::_thesis: verum end; thus a c= phi . a by A2, A10, ORDINAL4:10; ::_thesis: a is_cofinal_with omega take nu | omega ; :: according to ORDINAL2:def_17 ::_thesis: ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) ) rng (nu | omega) c= a proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (nu | omega) or e in a ) assume A51: e in rng (nu | omega) ; ::_thesis: e in a then consider u being set such that A52: u in dom (nu | omega) and A53: e = (nu | omega) . u by FUNCT_1:def_3; thus e in a by A51, A52, A53, ORDINAL2:19; ::_thesis: verum end; hence ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) ) by A8, A13, RELAT_1:62; ::_thesis: verum end; theorem Th30: :: ZFREFLE1:30 for W being Universe for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L ) ) proof let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L ) ) let L be DOMAIN-Sequence of W; ::_thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L ) ) ) assume that A1: omega in W and A2: ( ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) ) ; ::_thesis: ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L ) ) set M = Union L; defpred S2[ set , set ] means ex H being ZF-formula ex phi being Ordinal-Sequence of W st ( \$1 = H & \$2 = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for va being Function of VAR,(L . a) holds ( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) ); A3: for e being set st e in WFF holds ex u being set st ( u in Funcs ((On W),(On W)) & S2[e,u] ) proof let e be set ; ::_thesis: ( e in WFF implies ex u being set st ( u in Funcs ((On W),(On W)) & S2[e,u] ) ) assume e in WFF ; ::_thesis: ex u being set st ( u in Funcs ((On W),(On W)) & S2[e,u] ) then reconsider H = e as ZF-formula by ZF_LANG:4; consider phi being Ordinal-Sequence of W such that A4: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for va being Function of VAR,(L . a) holds ( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A1, A2, ZF_REFLE:20; reconsider u = phi as set ; take u ; ::_thesis: ( u in Funcs ((On W),(On W)) & S2[e,u] ) ( dom phi = On W & rng phi c= On W ) by FUNCT_2:def_1, RELAT_1:def_19; hence u in Funcs ((On W),(On W)) by FUNCT_2:def_2; ::_thesis: S2[e,u] take H ; ::_thesis: ex phi being Ordinal-Sequence of W st ( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for va being Function of VAR,(L . a) holds ( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) ) take phi ; ::_thesis: ( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for va being Function of VAR,(L . a) holds ( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) ) thus ( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for va being Function of VAR,(L . a) holds ( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A4; ::_thesis: verum end; consider Phi being Function such that A5: ( dom Phi = WFF & rng Phi c= Funcs ((On W),(On W)) ) and A6: for e being set st e in WFF holds S2[e,Phi . e] from FUNCT_1:sch_5(A3); reconsider Phi = Phi as Function of WFF,(Funcs ((On W),(On W))) by A5, FUNCT_2:def_1, RELSET_1:4; [:omega,omega:] in W by A1, CLASSES2:61; then bool [:omega,omega:] in W by CLASSES2:59; then ( card WFF c= card (bool [:omega,omega:]) & card (bool [:omega,omega:]) in card W ) by CARD_1:11, CLASSES2:1, ZF_LANG1:134; then consider phi being Ordinal-Sequence of W such that A7: ( phi is increasing & phi is continuous ) and phi . (0-element_of W) = 0-element_of W and A8: for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) and A9: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds phi . a = sup (phi | a) by Th13, ORDINAL1:12; take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L ) ) thus ( phi is increasing & phi is continuous ) by A7; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies L . a is_elementary_subsystem_of Union L ) assume that A10: phi . a = a and A11: {} <> a ; ::_thesis: L . a is_elementary_subsystem_of Union L thus L . a c= Union L by ZF_REFLE:16; :: according to ZFREFLE1:def_3 ::_thesis: for H being ZF-formula for v being Function of VAR,(L . a) holds ( L . a,v |= H iff Union L,(Union L) ! v |= H ) let H be ZF-formula; ::_thesis: for v being Function of VAR,(L . a) holds ( L . a,v |= H iff Union L,(Union L) ! v |= H ) let va be Function of VAR,(L . a); ::_thesis: ( L . a,va |= H iff Union L,(Union L) ! va |= H ) A12: H in WFF by ZF_LANG:4; then consider H1 being ZF-formula, xi being Ordinal-Sequence of W such that A13: H = H1 and A14: Phi . H = xi and A15: xi is increasing and A16: xi is continuous and A17: for a being Ordinal of W st xi . a = a & {} <> a holds for va being Function of VAR,(L . a) holds ( Union L,(Union L) ! va |= H1 iff L . a,va |= H1 ) by A6; defpred S3[ Ordinal] means ( \$1 <> {} implies xi . \$1 c= phi . \$1 ); a in dom xi by ORDINAL4:34; then A18: a c= xi . a by A15, ORDINAL4:10; A19: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds S3[b] ) holds S3[a] proof let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds S3[b] ) implies S3[a] ) assume that A20: a <> 0-element_of W and A21: a is limit_ordinal and A22: for b being Ordinal of W st b in a & b <> {} holds xi . b c= phi . b and a <> {} ; ::_thesis: xi . a c= phi . a A23: a in dom xi by ORDINAL4:34; then xi . a is_limes_of xi | a by A16, A20, A21, ORDINAL2:def_13; then A24: xi . a = lim (xi | a) by ORDINAL2:def_10; let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in xi . a or A in phi . a ) assume A25: A in xi . a ; ::_thesis: A in phi . a a c= dom xi by A23, ORDINAL1:def_2; then A26: dom (xi | a) = a by RELAT_1:62; xi | a is increasing by A15, ORDINAL4:15; then xi . a = sup (xi | a) by A20, A21, A26, A24, ORDINAL4:8 .= sup (rng (xi | a)) ; then consider B being Ordinal such that A27: B in rng (xi | a) and A28: A c= B by A25, ORDINAL2:21; consider e being set such that A29: e in dom (xi | a) and A30: B = (xi | a) . e by A27, FUNCT_1:def_3; reconsider e = e as Ordinal by A29; a in On W by ZF_REFLE:7; then e in On W by A26, A29, ORDINAL1:10; then reconsider e = e as Ordinal of W by ZF_REFLE:7; A31: succ e in a by A21, A26, A29, ORDINAL1:28; ( e in succ e & succ e in dom xi ) by ORDINAL1:6, ORDINAL4:34; then A32: xi . e in xi . (succ e) by A15, ORDINAL2:def_12; B = xi . e by A29, A30, FUNCT_1:47; then A33: A in xi . (succ e) by A28, A32, ORDINAL1:12; succ e in dom phi by ORDINAL4:34; then A34: phi . (succ e) in rng (phi | a) by A31, FUNCT_1:50; phi . a = sup (phi | a) by A9, A20, A21 .= sup (rng (phi | a)) ; then A35: phi . (succ e) in phi . a by A34, ORDINAL2:19; xi . (succ e) c= phi . (succ e) by A22, A31; hence A in phi . a by A35, A33, ORDINAL1:10; ::_thesis: verum end; A36: for a being Ordinal of W st S3[a] holds S3[ succ a] proof let a be Ordinal of W; ::_thesis: ( S3[a] implies S3[ succ a] ) succ a in {(succ a)} by TARSKI:def_1; then A37: [H,(succ a)] in [:WFF,{(succ a)}:] by A12, ZFMISC_1:87; succ a in dom xi by ORDINAL4:34; then ( [H,(succ a)] in dom (uncurry Phi) & (uncurry Phi) . (H,(succ a)) = xi . (succ a) ) by A5, A12, A14, FUNCT_5:38; then xi . (succ a) in (uncurry Phi) .: [:WFF,{(succ a)}:] by A37, FUNCT_1:def_6; then xi . (succ a) in {(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:]) by XBOOLE_0:def_3; then A38: xi . (succ a) in sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) by ORDINAL2:19; phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) by A8; hence ( S3[a] implies S3[ succ a] ) by A38, ORDINAL1:def_2; ::_thesis: verum end; A39: S3[ 0-element_of W] ; for a being Ordinal of W holds S3[a] from ZF_REFLE:sch_4(A39, A36, A19); then xi . a c= a by A10, A11; then xi . a = a by A18, XBOOLE_0:def_10; hence ( L . a,va |= H iff Union L,(Union L) ! va |= H ) by A11, A13, A17; ::_thesis: verum end; theorem Th31: :: ZFREFLE1:31 for W being Universe for a being Ordinal of W holds Rank a in W proof let W be Universe; ::_thesis: for a being Ordinal of W holds Rank a in W let a be Ordinal of W; ::_thesis: Rank a in W ( W = Rank (On W) & a in On W ) by CLASSES2:50, ZF_REFLE:7; hence Rank a in W by CLASSES1:36; ::_thesis: verum end; theorem Th32: :: ZFREFLE1:32 for W being Universe for a being Ordinal of W st a <> {} holds Rank a is non empty Element of W proof let W be Universe; ::_thesis: for a being Ordinal of W st a <> {} holds Rank a is non empty Element of W let a be Ordinal of W; ::_thesis: ( a <> {} implies Rank a is non empty Element of W ) assume a <> {} ; ::_thesis: Rank a is non empty Element of W then {} in a by ORDINAL3:8; then reconsider D = Rank a as non empty set by CLASSES1:36; D in W by Th31; hence Rank a is non empty Element of W ; ::_thesis: verum end; theorem Th33: :: ZFREFLE1:33 for W being Universe st omega in W holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W ) ) proof let W be Universe; ::_thesis: ( omega in W implies ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W ) ) ) deffunc H1( Ordinal, set ) -> set = Rank \$1; deffunc H2( Ordinal, set ) -> set = Rank (succ \$1); consider L being T-Sequence such that A1: ( dom L = On W & ( {} in On W implies L . {} = Rank (1-element_of W) ) ) and A2: for A being Ordinal st succ A in On W holds L . (succ A) = H2(A,L . A) and A3: for A being Ordinal st A in On W & A <> {} & A is limit_ordinal holds L . A = H1(A,L | A) from ORDINAL2:sch_5(); A4: for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Rank a proof let a be Ordinal of W; ::_thesis: ( a <> {} & a is limit_ordinal implies L . a = Rank a ) a in On W by ZF_REFLE:7; hence ( a <> {} & a is limit_ordinal implies L . a = Rank a ) by A3; ::_thesis: verum end; A5: for a being Ordinal of W holds L . (succ a) = Rank (succ a) proof let a be Ordinal of W; ::_thesis: L . (succ a) = Rank (succ a) succ a in On W by ZF_REFLE:7; hence L . (succ a) = Rank (succ a) by A2; ::_thesis: verum end; A6: for a being Ordinal of W st a <> {} holds L . a = Rank a proof let a be Ordinal of W; ::_thesis: ( a <> {} implies L . a = Rank a ) A7: now__::_thesis:_(_ex_A_being_Ordinal_st_a_=_succ_A_&_a_<>_{}_implies_L_._a_=_Rank_a_) A8: a in On W by ZF_REFLE:7; given A being Ordinal such that A9: a = succ A ; ::_thesis: ( a <> {} implies L . a = Rank a ) A in a by A9, ORDINAL1:6; then A in On W by A8, ORDINAL1:10; then reconsider A = A as Ordinal of W by ZF_REFLE:7; L . (succ A) = Rank (succ A) by A5; hence ( a <> {} implies L . a = Rank a ) by A9; ::_thesis: verum end; ( a is limit_ordinal or ex A being Ordinal st a = succ A ) by ORDINAL1:29; hence ( a <> {} implies L . a = Rank a ) by A4, A7; ::_thesis: verum end; rng L c= W proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng L or e in W ) assume e in rng L ; ::_thesis: e in W then consider u being set such that A10: u in On W and A11: e = L . u by A1, FUNCT_1:def_3; reconsider u = u as Ordinal of W by A10, ZF_REFLE:7; ( Rank (1-element_of W) in W & Rank u in W ) by Th31; hence e in W by A1, A6, A10, A11; ::_thesis: verum end; then reconsider L = L as T-Sequence of W by RELAT_1:def_19; now__::_thesis:_not_{}_in_rng_L assume {} in rng L ; ::_thesis: contradiction then consider e being set such that A12: e in On W and A13: {} = L . e by A1, FUNCT_1:def_3; reconsider e = e as Ordinal of W by A12, ZF_REFLE:7; ( ( e = {} & 1-element_of W = {{}} ) or e <> {} ) by ORDINAL3:15; then ( ( L . e = Rank (1-element_of W) & 1-element_of W <> {} ) or ( e <> {} & L . e = Rank e ) ) by A1, A6, ZF_REFLE:7; hence contradiction by A13, Th32; ::_thesis: verum end; then reconsider L = L as DOMAIN-Sequence of W by A1, RELAT_1:def_9, ZF_REFLE:def_2; A14: Union L = W proof thus Union L c= W ; :: according to XBOOLE_0:def_10 ::_thesis: W c= Union L let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in W or e in Union L ) A15: Union L = union (rng L) by CARD_3:def_4; assume e in W ; ::_thesis: e in Union L then A16: e in Rank (On W) by CLASSES2:50; On W is limit_ordinal by CLASSES2:51; then consider A being Ordinal such that A17: A in On W and A18: e in Rank A by A16, CLASSES1:31; reconsider A = A as Ordinal of W by A17, ZF_REFLE:7; ( L . A = Rank A & L . A in rng L ) by A1, A6, A17, A18, CLASSES1:29, FUNCT_1:def_3; then Rank A c= Union L by A15, ZFMISC_1:74; hence e in Union L by A18; ::_thesis: verum end; A19: 0-element_of W in On W by ZF_REFLE:7; A20: for a, b being Ordinal of W st a in b holds L . a c= L . b proof let a, b be Ordinal of W; ::_thesis: ( a in b implies L . a c= L . b ) assume A21: a in b ; ::_thesis: L . a c= L . b then A22: ( Rank a in Rank b & succ a c= b ) by CLASSES1:36, ORDINAL1:21; A23: L . b = Rank b by A6, A21; ( L . a = Rank a or ( a = 0-element_of W & L . a = Rank (1-element_of W) & 1-element_of W = succ (0-element_of W) ) ) by A1, A19, A6; hence L . a c= L . b by A22, A23, CLASSES1:37, ORDINAL1:def_2; ::_thesis: verum end; A24: for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) proof let a be Ordinal of W; ::_thesis: ( a <> {} & a is limit_ordinal implies L . a = Union (L | a) ) assume that A25: a <> {} and A26: a is limit_ordinal ; ::_thesis: L . a = Union (L | a) A27: a in On W by ZF_REFLE:7; A28: L . a = Rank a by A4, A25, A26; thus L . a c= Union (L | a) :: according to XBOOLE_0:def_10 ::_thesis: Union (L | a) c= L . a proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in L . a or e in Union (L | a) ) assume e in L . a ; ::_thesis: e in Union (L | a) then consider B being Ordinal such that A29: B in a and A30: e in Rank B by A25, A26, A28, CLASSES1:31; B in On W by A27, A29, ORDINAL1:10; then reconsider B = B as Ordinal of W by ZF_REFLE:7; A31: ( succ B in On W & Union (L | a) = union (rng (L | a)) ) by CARD_3:def_4, ZF_REFLE:7; L . (succ B) = Rank (succ B) by A5; then A32: Rank B c= L . (succ B) by CLASSES1:33; succ B in a by A26, A29, ORDINAL1:28; then L . (succ B) c= Union (L | a) by A1, A31, FUNCT_1:50, ZFMISC_1:74; then Rank B c= Union (L | a) by A32, XBOOLE_1:1; hence e in Union (L | a) by A30; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Union (L | a) or e in L . a ) assume e in Union (L | a) ; ::_thesis: e in L . a then e in union (rng (L | a)) by CARD_3:def_4; then consider X being set such that A33: e in X and A34: X in rng (L | a) by TARSKI:def_4; consider u being set such that A35: u in dom (L | a) and A36: X = (L | a) . u by A34, FUNCT_1:def_3; reconsider u = u as Ordinal by A35; A37: X = L . u by A35, A36, FUNCT_1:47; A38: dom (L | a) c= a by RELAT_1:58; then u in On W by A27, A35, ORDINAL1:10; then reconsider u = u as Ordinal of W by ZF_REFLE:7; L . u c= L . a by A20, A35, A38; hence e in L . a by A33, A37; ::_thesis: verum end; assume omega in W ; ::_thesis: ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W ) ) then consider phi being Ordinal-Sequence of W such that A39: ( phi is increasing & phi is continuous ) and A40: for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L by A20, A24, Th30; take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W ) ) thus ( phi is increasing & phi is continuous ) by A39; ::_thesis: for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W let a be Ordinal of W; ::_thesis: for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W let M be non empty set ; ::_thesis: ( phi . a = a & {} <> a & M = Rank a implies M is_elementary_subsystem_of W ) assume that A41: phi . a = a and A42: {} <> a and A43: M = Rank a ; ::_thesis: M is_elementary_subsystem_of W M = L . a by A6, A42, A43; hence M is_elementary_subsystem_of W by A40, A14, A41, A42; ::_thesis: verum end; theorem Th34: :: ZFREFLE1:34 for W being Universe for a being Ordinal of W st omega in W holds ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M is_elementary_subsystem_of W ) proof let W be Universe; ::_thesis: for a being Ordinal of W st omega in W holds ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M is_elementary_subsystem_of W ) let a be Ordinal of W; ::_thesis: ( omega in W implies ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M is_elementary_subsystem_of W ) ) assume A1: omega in W ; ::_thesis: ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M is_elementary_subsystem_of W ) then consider phi being Ordinal-Sequence of W such that A2: ( phi is increasing & phi is continuous ) and A3: for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W by Th33; consider b being Ordinal of W such that A4: a in b and A5: phi . b = b by A1, A2, Th28; reconsider M = Rank b as non empty set by A4, CLASSES1:36; take b ; ::_thesis: ex M being non empty set st ( a in b & M = Rank b & M is_elementary_subsystem_of W ) take M ; ::_thesis: ( a in b & M = Rank b & M is_elementary_subsystem_of W ) thus ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by A3, A4, A5; ::_thesis: verum end; theorem Th35: :: ZFREFLE1:35 for W being Universe st omega in W holds ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W ) proof let W be Universe; ::_thesis: ( omega in W implies ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W ) ) set a = the Ordinal of W; assume A1: omega in W ; ::_thesis: ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W ) then consider phi being Ordinal-Sequence of W such that A2: ( phi is increasing & phi is continuous ) and A3: for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W by Th33; consider b being Ordinal of W such that A4: the Ordinal of W in b and A5: ( phi . b = b & b is_cofinal_with omega ) by A1, A2, Th29; reconsider M = Rank b as non empty set by A4, CLASSES1:36; take b ; ::_thesis: ex M being non empty set st ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W ) take M ; ::_thesis: ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W ) thus ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W ) by A3, A4, A5; ::_thesis: verum end; theorem :: ZFREFLE1:36 for W being Universe for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a <==> Union L ) ) proof let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a <==> Union L ) ) let L be DOMAIN-Sequence of W; ::_thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a <==> Union L ) ) ) assume ( omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) ) ; ::_thesis: ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a <==> Union L ) ) then consider phi being Ordinal-Sequence of W such that A1: ( phi is increasing & phi is continuous ) and A2: for a being Ordinal of W st phi . a = a & {} <> a holds L . a is_elementary_subsystem_of Union L by Th30; take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds L . a <==> Union L ) ) thus ( phi is increasing & phi is continuous ) by A1; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds L . a <==> Union L let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies L . a <==> Union L ) assume ( phi . a = a & {} <> a ) ; ::_thesis: L . a <==> Union L hence L . a <==> Union L by A2, Th9; ::_thesis: verum end; theorem :: ZFREFLE1:37 for W being Universe st omega in W holds ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M <==> W ) ) proof let W be Universe; ::_thesis: ( omega in W implies ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M <==> W ) ) ) assume omega in W ; ::_thesis: ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M <==> W ) ) then consider phi being Ordinal-Sequence of W such that A1: ( phi is increasing & phi is continuous ) and A2: for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M is_elementary_subsystem_of W by Th33; take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M <==> W ) ) thus ( phi is increasing & phi is continuous ) by A1; ::_thesis: for a being Ordinal of W for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M <==> W let a be Ordinal of W; ::_thesis: for M being non empty set st phi . a = a & {} <> a & M = Rank a holds M <==> W let M be non empty set ; ::_thesis: ( phi . a = a & {} <> a & M = Rank a implies M <==> W ) assume ( phi . a = a & {} <> a & M = Rank a ) ; ::_thesis: M <==> W hence M <==> W by A2, Th9; ::_thesis: verum end; theorem Th38: :: ZFREFLE1:38 for W being Universe for a being Ordinal of W st omega in W holds ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M <==> W ) proof let W be Universe; ::_thesis: for a being Ordinal of W st omega in W holds ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M <==> W ) let a be Ordinal of W; ::_thesis: ( omega in W implies ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M <==> W ) ) assume omega in W ; ::_thesis: ex b being Ordinal of W ex M being non empty set st ( a in b & M = Rank b & M <==> W ) then consider b being Ordinal of W, M being non empty set such that A1: ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by Th34; take b ; ::_thesis: ex M being non empty set st ( a in b & M = Rank b & M <==> W ) take M ; ::_thesis: ( a in b & M = Rank b & M <==> W ) thus ( a in b & M = Rank b & M <==> W ) by A1, Th9; ::_thesis: verum end; theorem Th39: :: ZFREFLE1:39 for W being Universe st omega in W holds ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M <==> W ) proof let W be Universe; ::_thesis: ( omega in W implies ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M <==> W ) ) assume omega in W ; ::_thesis: ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M <==> W ) then consider b being Ordinal of W, M being non empty set such that A1: ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W ) by Th35; take b ; ::_thesis: ex M being non empty set st ( b is_cofinal_with omega & M = Rank b & M <==> W ) take M ; ::_thesis: ( b is_cofinal_with omega & M = Rank b & M <==> W ) thus ( b is_cofinal_with omega & M = Rank b & M <==> W ) by A1, Th9; ::_thesis: verum end; theorem :: ZFREFLE1:40 for W being Universe st omega in W holds ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) proof let W be Universe; ::_thesis: ( omega in W implies ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) ) assume A1: omega in W ; ::_thesis: ex a being Ordinal of W ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) then consider a being Ordinal of W, M being non empty set such that A2: ( a is_cofinal_with omega & M = Rank a & M <==> W ) by Th39; take a ; ::_thesis: ex M being non empty set st ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) take M ; ::_thesis: ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) W is being_a_model_of_ZF by A1, ZF_REFLE:6; hence ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) by A2, Th10; ::_thesis: verum end; theorem :: ZFREFLE1:41 for X being set for W being Universe st omega in W & X in W holds ex M being non empty set st ( X in M & M in W & M is being_a_model_of_ZF ) proof let X be set ; ::_thesis: for W being Universe st omega in W & X in W holds ex M being non empty set st ( X in M & M in W & M is being_a_model_of_ZF ) let W be Universe; ::_thesis: ( omega in W & X in W implies ex M being non empty set st ( X in M & M in W & M is being_a_model_of_ZF ) ) assume A1: omega in W ; ::_thesis: ( not X in W or ex M being non empty set st ( X in M & M in W & M is being_a_model_of_ZF ) ) A2: W = Rank (On W) by CLASSES2:50; assume X in W ; ::_thesis: ex M being non empty set st ( X in M & M in W & M is being_a_model_of_ZF ) then the_rank_of X in the_rank_of W by CLASSES1:68; then the_rank_of X in On W by A2, CLASSES1:64; then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:7; consider b being Ordinal of W, M being non empty set such that A3: a in b and A4: M = Rank b and A5: M <==> W by A1, Th38; take M ; ::_thesis: ( X in M & M in W & M is being_a_model_of_ZF ) X c= Rank a by CLASSES1:def_8; then A6: X in Rank (succ a) by CLASSES1:32; succ a c= b by A3, ORDINAL1:21; then Rank (succ a) c= M by A4, CLASSES1:37; hence X in M by A6; ::_thesis: ( M in W & M is being_a_model_of_ZF ) b in On W by ZF_REFLE:7; hence M in W by A2, A4, CLASSES1:36; ::_thesis: M is being_a_model_of_ZF W is being_a_model_of_ZF by A1, ZF_REFLE:6; then W |= ZF-axioms by Th4; then M |= ZF-axioms by A5, Th8; hence M is being_a_model_of_ZF by A4, Th5; ::_thesis: verum end;