zfrefle1.miz



    begin

    

     Lm1: {} in omega by ORDINAL1:def 11;

    

     Lm2: omega is limit_ordinal by ORDINAL1:def 11;

    reserve H,S for ZF-formula,

x for Variable,

X,Y for set,

i for Element of NAT ,

e,u for set;

    definition

      let M be non empty set, F be Subset of WFF ;

      :: ZFREFLE1:def1

      pred M |= F means for H st H in F holds M |= H;

    end

    definition

      let M1,M2 be non empty set;

      :: ZFREFLE1:def2

      pred M1 <==> M2 means for H st ( Free H) = {} holds M1 |= H iff M2 |= H;

      reflexivity ;

      symmetry ;

      :: ZFREFLE1:def3

      pred M1 is_elementary_subsystem_of M2 means M1 c= M2 & for H holds for v be Function of VAR , M1 holds (M1,v) |= H iff (M2,(M2 ! v)) |= H;

      reflexivity by ZF_LANG1:def 1;

    end

    defpred ZFAx[ object] 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 st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & $1 = ( the_axiom_of_substitution_for H);

    definition

      :: ZFREFLE1:def4

      func ZF-axioms -> set means

      : Def4: for e be object 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 st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & e = ( the_axiom_of_substitution_for H));

      existence

      proof

        thus ex X st for e be object holds e in X iff e in WFF & ZFAx[e] from XBOOLE_0:sch 1;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 in WFF & ZFAx[$1];

        let X1,X2 be set such that

         A1: for e be object holds e in X1 iff P[e] and

         A2: for e be object holds e in X2 iff P[e];

        thus thesis from XBOOLE_0:sch 2( A1, A2);

      end;

    end

    definition

      :: original: ZF-axioms

      redefine

      func ZF-axioms -> Subset of WFF ;

      coherence

      proof

         ZF-axioms c= WFF by Def4;

        hence thesis;

      end;

    end

    reserve M,M1,M2 for non empty set,

f for Function,

v1 for Function of VAR , M1,

v2 for Function of VAR , M2,

F,F1,F2 for Subset of WFF ,

W for Universe,

a,b,c for Ordinal of W,

A,B,C for Ordinal,

L for DOMAIN-Sequence of W,

va for Function of VAR , (L . a),

phi,xi for Ordinal-Sequence of W;

    theorem :: ZFREFLE1:1

    M |= ( {} WFF );

    theorem :: ZFREFLE1:2

    F1 c= F2 & M |= F2 implies M |= F1;

    theorem :: ZFREFLE1:3

    M |= F1 & M |= F2 implies M |= (F1 \/ F2)

    proof

      assume

       A1: M |= F1 & M |= F2;

      let H;

      assume H in (F1 \/ F2);

      then H in F1 or H in F2 by XBOOLE_0:def 3;

      hence thesis by A1;

    end;

    theorem :: ZFREFLE1:4

    

     Th4: M is being_a_model_of_ZF implies M |= ZF-axioms

    proof

      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 st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds M |= ( the_axiom_of_substitution_for H));

      let H;

      assume H in ZF-axioms ;

      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 be ZF-formula st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H1) & H = ( the_axiom_of_substitution_for H1) by Def4;

      hence thesis by A1, ZFMODEL1: 1;

    end;

    theorem :: ZFREFLE1:5

    

     Th5: M |= ZF-axioms & M is epsilon-transitive implies M is being_a_model_of_ZF

    proof

       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 st H in ZF-axioms holds M |= H and

       A5: M is epsilon-transitive;

       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;

      let H;

      assume

       A6: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free 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 thesis by A4;

    end;

    theorem :: ZFREFLE1:6

    

     Th6: ex S st ( Free S) = {} & for M holds M |= S iff M |= H

    proof

      defpred P[ Nat] means for H st ( card ( Free H)) = $1 holds ex S st ( Free S) = {} & for M holds M |= S iff M |= H;

      

       A1: for i be Nat holds P[i] implies P[(i + 1)]

      proof

        let i be Nat;

        assume

         A2: P[i];

        let H;

        set e = the Element of ( Free H);

        assume

         A3: ( card ( Free H)) = (i + 1);

        then

         A4: ( Free H) <> {} ;

        then

        reconsider x = e 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 such that

         A8: ( Free S) = {} and

         A9: for M holds M |= S iff M |= ( All (x,H)) by A2, A3, XCMPLX_1: 2;

        take S;

        thus ( Free S) = {} by A8;

        let M;

        M |= H iff M |= ( All (x,H)) by ZF_MODEL: 23;

        hence thesis by A9;

      end;

      

       A10: ( card ( Free H)) = ( card ( Free H));

      

       A11: P[ 0 ]

      proof

        let H;

        assume

         A12: ( card ( Free H)) = 0 ;

        take H;

        thus thesis by A12;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A11, A1);

      hence thesis by A10;

    end;

    theorem :: ZFREFLE1:7

    M1 <==> M2 iff for H holds M1 |= H iff M2 |= H

    proof

      thus M1 <==> M2 implies for H holds M1 |= H iff M2 |= H

      proof

        assume

         A1: for H st ( Free H) = {} holds M1 |= H iff M2 |= H;

        let H;

        consider S such that

         A2: ( Free S) = {} and

         A3: for M holds M |= S iff M |= H by Th6;

        M1 |= S iff M2 |= S by A1, A2;

        hence thesis by A3;

      end;

      assume

       A4: for H holds M1 |= H iff M2 |= H;

      let H;

      thus thesis by A4;

    end;

    theorem :: ZFREFLE1:8

    

     Th8: M1 <==> M2 iff for F holds M1 |= F iff M2 |= F

    proof

      thus M1 <==> M2 implies for F holds M1 |= F iff M2 |= F

      proof

        assume

         A1: for H st ( Free H) = {} holds M1 |= H iff M2 |= H;

        let F;

        thus M1 |= F implies M2 |= F

        proof

          assume

           A2: H in F implies M1 |= H;

          let H;

          consider S such that

           A3: ( Free S) = {} and

           A4: for M holds M |= S iff M |= H by Th6;

          assume H in F;

          then M1 |= H by A2;

          then M1 |= S by A4;

          then M2 |= S by A1, A3;

          hence thesis by A4;

        end;

        assume

         A5: H in F implies M2 |= H;

        let H;

        consider S such that

         A6: ( Free S) = {} and

         A7: for M holds M |= S iff M |= H by Th6;

        assume H in F;

        then M2 |= H by A5;

        then M2 |= S by A7;

        then M1 |= S by A1, A6;

        hence thesis by A7;

      end;

      assume

       A8: M1 |= F iff M2 |= F;

      let H such that ( Free 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

      proof

        assume M1 |= H;

        then S in F implies M1 |= S by TARSKI:def 1;

        then M1 |= F;

        then

         A9: M2 |= F by A8;

        H in F by TARSKI:def 1;

        hence thesis by A9;

      end;

      assume M2 |= H;

      then S in F implies M2 |= S by TARSKI:def 1;

      then M2 |= F;

      then

       A10: M1 |= F by A8;

      H in F by TARSKI:def 1;

      hence thesis by A10;

    end;

    theorem :: ZFREFLE1:9

    

     Th9: M1 is_elementary_subsystem_of M2 implies M1 <==> M2

    proof

      assume that M1 c= M2 and

       A1: for H holds for v be Function of VAR , M1 holds (M1,v) |= H iff (M2,(M2 ! v)) |= H;

      let H such that

       A2: ( Free H) = {} ;

      thus M1 |= H implies M2 |= H

      proof

        assume

         A3: (M1,v1) |= H;

        set v1 = the Function of VAR , M1;

        (M1,v1) |= H by A3;

        then

         A4: (M2,(M2 ! v1)) |= H by A1;

        let v2;

        for x st x in ( Free H) holds (v2 . x) = ((M2 ! v1) . x) by A2;

        hence thesis by A4, ZF_LANG1: 75;

      end;

      assume

       A5: (M2,v2) |= H;

      let v1;

      (M2,(M2 ! v1)) |= H by A5;

      hence thesis by A1;

    end;

    theorem :: ZFREFLE1:10

    

     Th10: M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive implies M2 is being_a_model_of_ZF

    proof

      assume that

       A1: M1 is being_a_model_of_ZF and

       A2: M1 <==> M2;

      M1 |= ZF-axioms by A1, Th4;

      then M2 |= ZF-axioms by A2, Th8;

      hence thesis by Th5;

    end;

    theorem :: ZFREFLE1:11

    

     Th11: ( dom f) in W & ( rng f) c= W implies ( rng f) in W

    proof

      assume ( dom 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 thesis by CLASSES1: 1;

    end;

    theorem :: ZFREFLE1:12

    (X,Y) are_equipotent or ( card X) = ( card Y) implies (( bool X),( bool Y)) are_equipotent & ( card ( bool X)) = ( card ( bool Y))

    proof

      assume (X,Y) are_equipotent or ( card X) = ( card 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 thesis by A1, CARD_1: 5;

    end;

    theorem :: ZFREFLE1:13

    

     Th13: for D be non empty set, Phi be Function of D, ( Funcs (( On W),( On W))) st ( card D) in ( card W) holds ex phi st phi is increasing & phi is continuous & (phi . ( 0-element_of W)) = ( 0-element_of W) & (for a holds (phi . ( succ a)) = ( sup ( {(phi . a)} \/ (( uncurry Phi) .: [:D, {( succ a)}:])))) & for a st a <> ( 0-element_of W) & a is limit_ordinal holds (phi . a) = ( sup (phi | a))

    proof

      deffunc D( set, Sequence) = ( sup $2);

      let D be non empty set, Phi be Function of D, ( Funcs (( On W),( On W))) such that

       A1: ( card D) in ( card W);

      deffunc C( Ordinal, Ordinal) = ( sup ( {$2} \/ (( uncurry Phi) .: [:D, {( succ $1)}:])));

      consider L be Ordinal-Sequence such that

       A2: ( dom L) = ( On W) & ( 0 in ( On W) implies (L . 0 ) = 0 ) and

       A3: for A st ( succ A) in ( On W) holds (L . ( succ A)) = C(A,.) and

       A4: for A st A in ( On W) & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|) from ORDINAL2:sch 11;

      defpred P[ Ordinal] means (L . $1) in ( On W);

      

       A5: for a st P[a] holds P[( succ a)]

      proof

        let a;

        

         A6: ( On W) c= W by ORDINAL2: 7;

        assume (L . a) in ( On W);

        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;

        then (( uncurry Phi) .: [:D, {( succ a)}:]) c= W by A6;

        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 thesis by ORDINAL1:def 9;

      end;

      

       A10: for a st a <> ( 0-element_of W) & a is limit_ordinal & for b st b in a holds P[b] holds P[a]

      proof

        let a such that

         A11: a <> ( 0-element_of W) & a is limit_ordinal and

         A12: for b st b in a holds (L . b) in ( On W);

        

         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 object;

          assume e in ( rng (L | a));

          then

          consider u be object such that

           A17: u in ( dom (L | a)) and

           A18: e = ((L | a) . u) by FUNCT_1:def 3;

          reconsider u as Ordinal by A17;

          u in ( On W) by A15, A13, A17, ORDINAL1: 10;

          then

          reconsider 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 thesis by ORDINAL1:def 9;

        end;

        (L . a) = ( sup (L | a)) by A4, A11, A15;

        then (L . a) in W by A14, A16, Th11, ZF_REFLE: 19;

        hence thesis by ORDINAL1:def 9;

      end;

      

       A19: P[( 0-element_of W)] by A2, ORDINAL1:def 9;

      ( rng L) c= ( On W)

      proof

        let e be object;

        assume e in ( rng L);

        then

        consider u be object such that

         A20: u in ( dom L) and

         A21: e = (L . u) by FUNCT_1:def 3;

        reconsider u as Ordinal of W by A2, A20, ZF_REFLE: 7;

         P[a] from ZF_REFLE:sch 4( A19, A5, A10);

        then (L . u) in ( On W);

        hence thesis by A21;

      end;

      then

      reconsider phi = L as Ordinal-Sequence of W by A2, FUNCT_2:def 1, RELSET_1: 4;

      take phi;

      thus

       A22: phi is increasing

      proof

        let A, B;

        assume that

         A23: A in B and

         A24: B in ( dom phi);

        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 Q[ Ordinal] means a in $1 implies (phi . a) in (phi . $1);

        

         A25: for b st Q[b] holds Q[( succ b)]

        proof

          let b such that

           A26: (a in b implies (phi . a) in (phi . b)) & a in ( 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 thesis by A26, ORDINAL1: 8, ORDINAL1: 10;

        end;

        

         A28: for b st b <> ( 0-element_of W) & b is limit_ordinal & for c st c in b holds Q[c] holds Q[b]

        proof

          let b such that

           A29: b <> ( 0-element_of W) & b is limit_ordinal and for c st c in b holds a in c implies (phi . a) in (phi . c) and

           A30: a in 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;

        end;

        

         A32: Q[( 0-element_of W)];

        for b holds Q[b] from ZF_REFLE:sch 4( A32, A25, A28);

        then (phi . a) in (phi . b) by A23;

        hence thesis;

      end;

      thus phi is continuous

      proof

        let A, B;

        assume that

         A33: A in ( dom phi) and

         A34: A <> 0 & A is limit_ordinal and

         A35: B = (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 thesis by A34, A36, A37, ORDINAL4: 8;

      end;

      thus (phi . ( 0-element_of W)) = ( 0-element_of W) by A2, ORDINAL1:def 9;

      thus for a holds (phi . ( succ a)) = ( sup ( {(phi . a)} \/ (( uncurry Phi) .: [:D, {( succ a)}:]))) by A3, ZF_REFLE: 7;

      let a;

      a in ( On W) by ZF_REFLE: 7;

      hence thesis by A4;

    end;

    theorem :: ZFREFLE1:14

    

     Th14: for phi be Ordinal-Sequence st phi is increasing holds (C +^ phi) is increasing

    proof

      let phi be Ordinal-Sequence such that

       A1: phi is increasing;

      let A, B;

      set xi = (C +^ phi);

      assume that

       A2: A in B and

       A3: B in ( dom xi);

      reconsider A9 = (phi . A), B9 = (phi . B) as Ordinal;

      

       A4: ( dom xi) = ( dom phi) by ORDINAL3:def 1;

      then

       A5: (xi . B) = (C +^ B9) by A3, ORDINAL3:def 1;

      A in ( dom xi) by A2, A3, ORDINAL1: 10;

      then

       A6: (xi . A) = (C +^ A9) by A4, ORDINAL3:def 1;

      A9 in B9 by A1, A2, A3, A4;

      hence thesis by A6, A5, ORDINAL2: 32;

    end;

    theorem :: ZFREFLE1:15

    

     Th15: for xi be Ordinal-Sequence holds ((C +^ xi) | A) = (C +^ (xi | A))

    proof

      let xi be Ordinal-Sequence;

      

       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

        let e be object;

        assume

         A5: e in ( dom ((C +^ xi) | A));

        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;

      end;

      ( dom (C +^ (xi | A))) = ( dom (xi | A)) by ORDINAL3:def 1;

      hence thesis by A1, A2, A4, FUNCT_1: 2, RELAT_1: 61;

    end;

    theorem :: ZFREFLE1:16

    

     Th16: for phi be Ordinal-Sequence st phi is increasing & phi is continuous holds (C +^ phi) is continuous

    proof

      let phi be Ordinal-Sequence such that

       A1: phi is increasing;

      assume

       A2: for A, B st A in ( dom phi) & A <> 0 & A is limit_ordinal & B = (phi . A) holds B is_limes_of (phi | A);

      let A, B;

      set xi = (phi | A);

      reconsider A9 = (phi . A) as Ordinal;

      assume that

       A3: A in ( dom (C +^ phi)) and

       A4: A <> 0 and

       A5: A is limit_ordinal and

       A6: B = ((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 xi by A2, A3, A4, A5, A7;

      then

       A9: ( lim xi) = A9 by ORDINAL2:def 10;

      

       A10: ( dom xi) = ( dom (C +^ xi)) & ((C +^ phi) | A) = (C +^ xi) by Th15, ORDINAL3:def 1;

      

       A11: xi is increasing by A1, ORDINAL4: 15;

      then

       A12: (C +^ xi) is increasing by Th14;

      A c= ( dom (C +^ phi)) by A3, ORDINAL1:def 2;

      then

       A13: ( dom xi) = A by A7, RELAT_1: 62;

      then

       A14: ( sup (C +^ xi)) = (C +^ ( sup xi)) by A4, ORDINAL3: 43;

      ( sup xi) = ( lim xi) by A4, A5, A13, A11, ORDINAL4: 8;

      hence thesis by A4, A5, A13, A10, A8, A14, A9, A12, ORDINAL4: 8;

    end;

    reserve psi for Ordinal-Sequence;

    theorem :: ZFREFLE1:17

    e in ( rng psi) implies e is Ordinal by ORDINAL2: 48;

    theorem :: ZFREFLE1:18

    ( rng psi) c= ( sup psi) by ORDINAL2: 49;

    theorem :: ZFREFLE1:19

    A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C by ORDINAL4: 37;

    theorem :: ZFREFLE1:20

    

     Th20: A is_cofinal_with B implies B c= A

    proof

      given psi such that

       A1: ( dom psi) = B and

       A2: ( rng psi) c= A and

       A3: psi is increasing and A = ( sup psi);

      let C;

      assume C in B;

      then C c= (psi . C) & (psi . C) in ( rng psi) by A1, A3, FUNCT_1:def 3, ORDINAL4: 10;

      hence thesis by A2, ORDINAL1: 12;

    end;

    theorem :: ZFREFLE1:21

    A is_cofinal_with B & B is_cofinal_with A implies A = B by Th20;

    theorem :: ZFREFLE1:22

    ( dom psi) <> {} & ( dom psi) is limit_ordinal & psi is increasing & A is_limes_of psi implies A is_cofinal_with ( dom psi)

    proof

      assume that

       A1: ( dom psi) <> {} & ( dom psi) is limit_ordinal and

       A2: psi is increasing and

       A3: A is_limes_of psi;

      take psi;

      thus ( dom psi) = ( dom psi);

      ( sup psi) = ( lim psi) & A = ( lim psi) by A1, A2, A3, ORDINAL2:def 10, ORDINAL4: 8;

      hence thesis by A2, ORDINAL2: 49;

    end;

    theorem :: ZFREFLE1:23

    ( succ A) is_cofinal_with 1 by ORDINAL3: 73;

    theorem :: ZFREFLE1:24

    A is_cofinal_with ( succ B) implies ex C st A = ( succ C)

    proof

      given psi such that

       A1: ( dom psi) = ( succ B) and

       A2: ( rng psi) c= A and

       A3: psi is increasing and

       A4: A = ( sup psi);

      reconsider C = (psi . B) as Ordinal;

      take C;

      thus A c= ( succ C)

      proof

        let a be Ordinal;

        assume a in A;

        then

        consider b be Ordinal such that

         A5: b in ( rng psi) and

         A6: a c= b by A4, ORDINAL2: 21;

        consider e be object such that

         A7: e in ( succ B) and

         A8: b = (psi . e) by A1, A5, FUNCT_1:def 3;

        reconsider 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 thesis by A6, ORDINAL1: 12;

      end;

      B in ( succ B) by ORDINAL1: 6;

      then C in ( rng psi) by A1, FUNCT_1:def 3;

      hence thesis by A2, ORDINAL1: 21;

    end;

    theorem :: ZFREFLE1:25

    A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal) by ORDINAL4: 38;

    theorem :: ZFREFLE1:26

    A is_cofinal_with {} implies A = {} by ORDINAL2: 50;

    theorem :: ZFREFLE1:27

     not ( On W) is_cofinal_with a

    proof

      given psi such that

       A1: ( dom psi) = a and

       A2: ( rng psi) c= ( On W) and psi is increasing and

       A3: ( On W) = ( sup psi);

      ( On W) c= W by ORDINAL2: 7;

      then ( rng psi) c= W by A2;

      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;

    end;

    theorem :: ZFREFLE1:28

    

     Th28: omega in W & phi is increasing & phi is continuous implies ex b st a in b & (phi . b) = b

    proof

      assume that

       A1: omega in W and

       A2: phi is increasing and

       A3: phi is continuous;

      deffunc F( Ordinal of W) = (( succ a) +^ (phi . $1));

      consider xi such that

       A4: (xi . b) = F(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 st A in ( dom phi) holds (xi . A) = (( succ a) +^ (phi . A))

      proof

        let A;

        assume A in ( dom phi);

        then

        reconsider b = A as Ordinal of W by A6, ZF_REFLE: 7;

        (xi . b) = (( succ a) +^ (phi . b)) by A4;

        hence thesis;

      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 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;

      

       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 thesis by A10, A9, A11;

    end;

    theorem :: ZFREFLE1:29

    

     Th29: omega in W & phi is increasing & phi is continuous implies ex a st b in a & (phi . a) = a & a is_cofinal_with omega

    proof

      assume that

       A1: omega in W and

       A2: phi is increasing and

       A3: phi is continuous;

      

       A4: omega in ( On W) by A1, ORDINAL1:def 9;

      deffunc D( Ordinal, set) = ( 0-element_of W);

      deffunc C( Ordinal, Ordinal of W) = ( succ (phi . $2));

      consider nu be Ordinal-Sequence of W such that

       A5: (nu . ( 0-element_of W)) = b and

       A6: for a holds (nu . ( succ a)) = C(a,.) and for a st a <> ( 0-element_of W) & a is limit_ordinal holds (nu . a) = D(a,|) from ZF_REFLE:sch 3;

      set xi = (nu | omega );

      set a = ( sup xi);

      

       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 xi) = omega by RELAT_1: 62;

      ( rng xi) c= ( rng nu) & ( rng nu) c= ( On W) by RELAT_1:def 19;

      then ( rng xi) c= ( On W);

      then ( rng xi) c= W by A7;

      then

      reconsider a 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: xi is increasing

      proof

        let A, B;

        assume that

         A14: A in B and

         A15: B in ( dom xi);

        defpred P[ Ordinal] means (A +^ $1) in ( dom xi) & $1 <> {} implies (xi . A) in (xi . (A +^ $1));

        

         A16: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C] holds P[B]

        proof

          let B;

          assume that

           A17: B <> 0 and

           A18: B is limit_ordinal;

           {} in B by A17, ORDINAL3: 8;

          then

           A19: omega c= B by A18, ORDINAL1:def 11;

          B c= (A +^ B) by ORDINAL3: 24;

          hence thesis by A9, A19, ORDINAL1: 5;

        end;

        

         A20: for C st P[C] holds P[( succ C)]

        proof

          let C such that

           A21: (A +^ C) in ( dom xi) & C <> {} implies (xi . A) in (xi . (A +^ C)) and

           A22: (A +^ ( succ C)) in ( dom xi) and ( 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

            (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 = {} ;

            then

             A28: ac = A by ORDINAL2: 27;

            (xi . ac) = (nu . ac) & (xi . asc) = (nu . asc) by A22, A24, FUNCT_1: 47, ORDINAL1: 10;

            hence thesis by A28, A27, A26, ORDINAL1: 6, ORDINAL1: 12;

          end;

          

           A29: ( succ ac) = asc & (nu . ac) in ( dom phi) by ORDINAL2: 28, ORDINAL4: 34;

          (A +^ C) in ( dom xi) by A22, A24, ORDINAL1: 10;

          then (xi . A) in (xi . ac) & (nu . asc) = ( succ (phi . (nu . ac))) & (nu . ac) = (xi . 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 (xi . A) in (nu . ac) & (nu . ac) in (nu . asc) & (nu . asc) = (xi . asc) or C = {} by A22, FUNCT_1: 47, ORDINAL1: 12;

          then (xi . A) in (nu . ac) & (nu . ac) c= (xi . asc) or C = {} by ORDINAL1:def 2;

          hence thesis by A25;

        end;

        

         A30: P[ 0 ];

        

         A31: P[C] from ORDINAL2:sch 1( A30, A20, A16);

        ex C st B = (A +^ C) & C <> {} by A14, ORDINAL3: 28;

        hence thesis by A15, A31;

      end;

      then

       A32: a is limit_ordinal by A9, Lm2, ORDINAL4: 16;

      take a;

      ( 0-element_of W) in ( dom nu) by ORDINAL4: 34;

      then

       A33: b in ( rng xi) by A5, Lm1, FUNCT_1: 50;

      hence b in a by ORDINAL2: 19;

      

       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;

      (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

      proof

        let A;

        assume A in (phi . a);

        then

        consider B such that

         A37: B in ( rng (phi | a)) and

         A38: A c= B by A36, ORDINAL2: 21;

        consider e be object such that

         A39: e in a and

         A40: B = ((phi | a) . e) by A12, A37, FUNCT_1:def 3;

        reconsider e as Ordinal by A39;

        consider C such that

         A41: C in ( rng xi) and

         A42: e c= C by A39, ORDINAL2: 21;

        

         A43: e c< C iff e c= C & e <> C;

        consider u be object such that

         A44: u in omega and

         A45: C = (xi . u) by A9, A41, FUNCT_1:def 3;

        reconsider u as Ordinal by A44;

        u c= omega by A44, ORDINAL1:def 2;

        then

        reconsider 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;

        

         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 xi) 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 thesis by A38, ORDINAL1: 12;

      end;

      thus a c= (phi . a) by A2, A10, ORDINAL4: 10;

      take xi;

      ( rng xi) c= a

      proof

        let e be object;

        assume

         A51: e in ( rng xi);

        then

        consider u be object such that u in ( dom xi) and

         A52: e = (xi . u) by FUNCT_1:def 3;

        thus thesis by A51, A52, ORDINAL2: 19;

      end;

      hence thesis by A8, A13, RELAT_1: 62;

    end;

    theorem :: ZFREFLE1:30

    

     Th30: omega in W & (for a, b st a in b holds (L . a) c= (L . b)) & (for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a))) implies ex phi st phi is increasing & phi is continuous & for a st (phi . a) = a & {} <> a holds (L . a) is_elementary_subsystem_of ( Union L)

    proof

      assume that

       A1: omega in W and

       A2: (for a, b st a in b holds (L . a) c= (L . b)) & for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a));

      set M = ( Union L);

      defpred P[ object, object] means ex H, phi st $1 = H & $2 = phi & phi is increasing & phi is continuous & for a st (phi . a) = a & {} <> a holds for va holds (( Union L),(( Union L) ! va)) |= H iff ((L . a),va) |= H;

      

       A3: for e be object st e in WFF holds ex u be object st u in ( Funcs (( On W),( On W))) & P[e, u]

      proof

        let e be object;

        assume e in WFF ;

        then

        reconsider H = e as ZF-formula by ZF_LANG: 4;

        consider phi such that

         A4: phi is increasing & phi is continuous & for a st (phi . a) = a & {} <> a holds for va 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;

        ( 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;

        take H, phi;

        thus thesis by A4;

      end;

      consider Phi be Function such that

       A5: ( dom Phi) = WFF & ( rng Phi) c= ( Funcs (( On W),( On W))) and

       A6: for e be object st e in WFF holds P[e, (Phi . e)] from FUNCT_1:sch 6( A3);

      reconsider 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 such that

       A7: phi is increasing & phi is continuous and (phi . ( 0-element_of W)) = ( 0-element_of W) and

       A8: for a holds (phi . ( succ a)) = ( sup ( {(phi . a)} \/ (( uncurry Phi) .: [: WFF , {( succ a)}:]))) and

       A9: for a st a <> ( 0-element_of W) & a is limit_ordinal holds (phi . a) = ( sup (phi | a)) by Th13, ORDINAL1: 12;

      take phi;

      thus phi is increasing & phi is continuous by A7;

      let a such that

       A10: (phi . a) = a and

       A11: {} <> a;

      thus (L . a) c= ( Union L) by ZF_REFLE: 16;

      let H, va;

      

       A12: H in WFF by ZF_LANG: 4;

      then

      consider H1 be ZF-formula, xi such that

       A13: H = H1 and

       A14: (Phi . H) = xi and

       A15: xi is increasing and

       A16: xi is continuous and

       A17: for a st (xi . a) = a & {} <> a holds for va holds (M,(M ! va)) |= H1 iff ((L . a),va) |= H1 by A6;

      defpred P[ 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 st a <> ( 0-element_of W) & a is limit_ordinal & for b st b in a holds P[b] holds P[a]

      proof

        let a such that

         A20: a <> ( 0-element_of W) and

         A21: a is limit_ordinal and

         A22: for b st b in a holds b <> {} implies (xi . b) c= (phi . b) and a <> {} ;

        

         A23: a in ( dom xi) by ORDINAL4: 34;

        then (xi . a) is_limes_of (xi | a) by A16, A20, A21;

        then

         A24: (xi . a) = ( lim (xi | a)) by ORDINAL2:def 10;

        let A such that

         A25: A in (xi . 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 such that

         A27: B in ( rng (xi | a)) and

         A28: A c= B by A25, ORDINAL2: 21;

        consider e be object such that

         A29: e in ( dom (xi | a)) and

         A30: B = ((xi | a) . e) by A27, FUNCT_1:def 3;

        reconsider 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 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;

        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;

      end;

      

       A36: for a st P[a] holds P[( succ a)]

      proof

        let 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 thesis by A38, ORDINAL1:def 2;

      end;

      

       A39: P[( 0-element_of W)];

      for a holds P[a] from ZF_REFLE:sch 4( A39, A36, A19);

      then (xi . a) c= a by A10, A11;

      then (xi . a) = a by A18;

      hence thesis by A11, A13, A17;

    end;

    theorem :: ZFREFLE1:31

    

     Th31: ( Rank a) in W

    proof

      W = ( Rank ( On W)) & a in ( On W) by CLASSES2: 50, ZF_REFLE: 7;

      hence thesis by CLASSES1: 36;

    end;

    theorem :: ZFREFLE1:32

    

     Th32: a <> {} implies ( Rank a) is non empty Element of W by Th31, CLASSES1: 36, ORDINAL3: 8;

    theorem :: ZFREFLE1:33

    

     Th33: omega in W implies ex phi st phi is increasing & phi is continuous & for a, M st (phi . a) = a & {} <> a & M = ( Rank a) holds M is_elementary_subsystem_of W

    proof

      deffunc D( Ordinal, set) = ( Rank $1);

      deffunc C( Ordinal, set) = ( Rank ( succ $1));

      consider L be Sequence such that

       A1: ( dom L) = ( On W) & ( 0 in ( On W) implies (L . 0 ) = ( Rank ( 1-element_of W))) and

       A2: for A st ( succ A) in ( On W) holds (L . ( succ A)) = C(A,.) and

       A3: for A st A in ( On W) & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|) from ORDINAL2:sch 5;

      

       A4: a <> {} & a is limit_ordinal implies (L . a) = ( Rank a) by A3, ZF_REFLE: 7;

      

       A5: (L . ( succ a)) = ( Rank ( succ a)) by A2, ZF_REFLE: 7;

      

       A6: a <> {} implies (L . a) = ( Rank a)

      proof

         A7:

        now

          

           A8: a in ( On W) by ZF_REFLE: 7;

          given A such that

           A9: a = ( succ A);

          A in a by A9, ORDINAL1: 6;

          then A in ( On W) by A8, ORDINAL1: 10;

          then

          reconsider A as Ordinal of W by ZF_REFLE: 7;

          (L . ( succ A)) = ( Rank ( succ A)) by A5;

          hence thesis by A9;

        end;

        a is limit_ordinal or ex A st a = ( succ A) by ORDINAL1: 29;

        hence thesis by A4, A7;

      end;

      ( rng L) c= W

      proof

        let e be object;

        assume e in ( rng L);

        then

        consider u be object such that

         A10: u in ( On W) and

         A11: e = (L . u) by A1, FUNCT_1:def 3;

        reconsider u as Ordinal of W by A10, ZF_REFLE: 7;

        ( Rank ( 1-element_of W)) in W & ( Rank u) in W by Th31;

        hence thesis by A1, A6, A10, A11;

      end;

      then

      reconsider L as Sequence of W by RELAT_1:def 19;

      now

        assume {} in ( rng L);

        then

        consider e be object such that

         A12: e in ( On W) and

         A13: {} = (L . e) by A1, FUNCT_1:def 3;

        reconsider 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;

      end;

      then

      reconsider 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;

        let e be object;

        

         A15: ( Union L) = ( union ( rng L)) by CARD_3:def 4;

        assume e in W;

        then

         A16: e in ( Rank ( On W)) by CLASSES2: 50;

        ( On W) is limit_ordinal by CLASSES2: 51;

        then

        consider A such that

         A17: A in ( On W) and

         A18: e in ( Rank A) by A16, CLASSES1: 31;

        reconsider 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 thesis by A18;

      end;

      

       A19: ( 0-element_of W) in ( On W) by ZF_REFLE: 7;

      

       A20: for a, b st a in b holds (L . a) c= (L . b)

      proof

        let a, b;

        assume

         A21: a in 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 thesis by A22, A23, CLASSES1: 37, ORDINAL1:def 2;

      end;

      

       A24: for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a))

      proof

        let a;

        assume that

         A25: a <> {} and

         A26: a is limit_ordinal;

        

         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))

        proof

          let e be object;

          assume e in (L . a);

          then

          consider B 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 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;

          hence thesis by A30;

        end;

        let e be object;

        assume e in ( Union (L | a));

        then e in ( union ( rng (L | a))) by CARD_3:def 4;

        then

        consider X such that

         A33: e in X and

         A34: X in ( rng (L | a)) by TARSKI:def 4;

        consider u be object such that

         A35: u in ( dom (L | a)) and

         A36: X = ((L | a) . u) by A34, FUNCT_1:def 3;

        reconsider 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 as Ordinal of W by ZF_REFLE: 7;

        (L . u) c= (L . a) by A20, A35, A38;

        hence thesis by A33, A37;

      end;

      assume omega in W;

      then

      consider phi such that

       A39: phi is increasing & phi is continuous and

       A40: for a st (phi . a) = a & {} <> a holds (L . a) is_elementary_subsystem_of ( Union L) by A20, A24, Th30;

      take phi;

      thus phi is increasing & phi is continuous by A39;

      let a, M;

      assume that

       A41: (phi . a) = a and

       A42: {} <> a and

       A43: M = ( Rank a);

      M = (L . a) by A6, A42, A43;

      hence thesis by A40, A14, A41, A42;

    end;

    theorem :: ZFREFLE1:34

    

     Th34: omega in W implies ex b, M st a in b & M = ( Rank b) & M is_elementary_subsystem_of W

    proof

      assume

       A1: omega in W;

      then

      consider phi such that

       A2: phi is increasing & phi is continuous and

       A3: for a, M st (phi . a) = a & {} <> a & M = ( Rank a) holds M is_elementary_subsystem_of W by Th33;

      consider b 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, M;

      thus thesis by A3, A4, A5;

    end;

    theorem :: ZFREFLE1:35

    

     Th35: omega in W implies ex a, M st a is_cofinal_with omega & M = ( Rank a) & M is_elementary_subsystem_of W

    proof

      set a = the Ordinal of W;

      assume

       A1: omega in W;

      then

      consider phi such that

       A2: phi is increasing & phi is continuous and

       A3: for a, M st (phi . a) = a & {} <> a & M = ( Rank a) holds M is_elementary_subsystem_of W by Th33;

      consider b such that

       A4: a 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, M;

      thus thesis by A3, A4, A5;

    end;

    theorem :: ZFREFLE1:36

     omega in W & (for a, b st a in b holds (L . a) c= (L . b)) & (for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a))) implies ex phi st phi is increasing & phi is continuous & for a st (phi . a) = a & {} <> a holds (L . a) <==> ( Union L)

    proof

      assume ( omega in W & for a, b st a in b holds (L . a) c= (L . b)) & for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a));

      then

      consider phi such that

       A1: phi is increasing & phi is continuous and

       A2: for a st (phi . a) = a & {} <> a holds (L . a) is_elementary_subsystem_of ( Union L) by Th30;

      take phi;

      thus phi is increasing & phi is continuous by A1;

      let a;

      assume (phi . a) = a & {} <> a;

      hence thesis by A2, Th9;

    end;

    theorem :: ZFREFLE1:37

     omega in W implies ex phi st phi is increasing & phi is continuous & for a, M st (phi . a) = a & {} <> a & M = ( Rank a) holds M <==> W

    proof

      assume omega in W;

      then

      consider phi such that

       A1: phi is increasing & phi is continuous and

       A2: for a, M st (phi . a) = a & {} <> a & M = ( Rank a) holds M is_elementary_subsystem_of W by Th33;

      take phi;

      thus phi is increasing & phi is continuous by A1;

      let a, M;

      assume (phi . a) = a & {} <> a & M = ( Rank a);

      hence thesis by A2, Th9;

    end;

    theorem :: ZFREFLE1:38

    

     Th38: omega in W implies ex b, M st a in b & M = ( Rank b) & M <==> W

    proof

      assume omega in W;

      then

      consider b, M such that

       A1: a in b & M = ( Rank b) & M is_elementary_subsystem_of W by Th34;

      take b, M;

      thus thesis by A1, Th9;

    end;

    theorem :: ZFREFLE1:39

    

     Th39: omega in W implies ex a, M st a is_cofinal_with omega & M = ( Rank a) & M <==> W

    proof

      assume omega in W;

      then

      consider b, M such that

       A1: b is_cofinal_with omega & M = ( Rank b) & M is_elementary_subsystem_of W by Th35;

      take b, M;

      thus thesis by A1, Th9;

    end;

    theorem :: ZFREFLE1:40

     omega in W implies ex a, M st a is_cofinal_with omega & M = ( Rank a) & M is being_a_model_of_ZF

    proof

      assume

       A1: omega in W;

      then

      consider a, M such that

       A2: a is_cofinal_with omega & M = ( Rank a) & M <==> W by Th39;

      take a, M;

      W is being_a_model_of_ZF by A1, ZF_REFLE: 6;

      hence thesis by A2, Th10;

    end;

    theorem :: ZFREFLE1:41

     omega in W & X in W implies ex M st X in M & M in W & M is being_a_model_of_ZF

    proof

      assume

       A1: omega in W;

      

       A2: W = ( Rank ( On W)) by CLASSES2: 50;

      assume X in W;

      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, M such that

       A3: a in b and

       A4: M = ( Rank b) and

       A5: M <==> W by A1, Th38;

      take M;

      X c= ( Rank a) by CLASSES1:def 9;

      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;

      b in ( On W) by ZF_REFLE: 7;

      hence M in W by A2, A4, CLASSES1: 36;

      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 thesis by A4, Th5;

    end;