zf_refle.miz



    begin

    reserve W for Universe,

H for ZF-formula,

x,y,z,X for set,

k for Variable,

f for Function of VAR , W,

u,v for Element of W;

    theorem :: ZF_REFLE:1

    

     Th1: W |= the_axiom_of_pairs

    proof

      for u, v holds {u, v} in W;

      hence thesis by ZFMODEL1: 2;

    end;

    theorem :: ZF_REFLE:2

    

     Th2: W |= the_axiom_of_unions

    proof

      for u holds ( union u) in W;

      hence thesis by ZFMODEL1: 4;

    end;

    theorem :: ZF_REFLE:3

    

     Th3: omega in W implies W |= the_axiom_of_infinity

    proof

      assume omega in W;

      then

      reconsider u = omega as Element of W;

      now

        take u;

        thus u <> {} ;

        let v;

        assume

         A1: v in u;

        then

        reconsider A = v as Ordinal;

        ( succ A) in omega by A1, ORDINAL1: 28;

        then ( succ A) c= u by ORDINAL1:def 2;

        then

        reconsider w = ( succ A) as Element of W by CLASSES1:def 1;

        take w;

        A in ( succ A) by ORDINAL1: 6;

        then v c= w & v <> w by ORDINAL1:def 2;

        hence v c< w & w in u by A1, ORDINAL1: 28;

      end;

      hence thesis by ZFMODEL1: 6;

    end;

    theorem :: ZF_REFLE:4

    

     Th4: W |= the_axiom_of_power_sets

    proof

      for u holds (W /\ ( bool u)) in W by CLASSES1:def 1, XBOOLE_1: 17;

      hence thesis by ZFMODEL1: 8;

    end;

    theorem :: ZF_REFLE:5

    

     Th5: for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds W |= ( the_axiom_of_substitution_for H)

    proof

      for H, f st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (W,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) holds for u holds (( def_func' (H,f)) .: u) in W

      proof

        let H, f such that {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) and (W,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

        let u;

        ( card u) in ( card W) by CLASSES2: 1;

        then ( card (( def_func' (H,f)) .: u)) in ( card W) by CARD_1: 67, ORDINAL1: 12;

        hence thesis by CLASSES1: 1;

      end;

      hence thesis by ZFMODEL1: 15;

    end;

    theorem :: ZF_REFLE:6

    

     Th6: omega in W implies W is being_a_model_of_ZF

    proof

      assume omega in W;

      hence W is epsilon-transitive & W |= the_axiom_of_pairs & W |= the_axiom_of_unions & W |= the_axiom_of_infinity & W |= the_axiom_of_power_sets & for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds W |= ( the_axiom_of_substitution_for H) by Th1, Th2, Th3, Th4, Th5;

    end;

    reserve F for Function,

A,B,C for Ordinal,

a,b,b1,b2,c for Ordinal of W,

fi for Ordinal-Sequence,

phi for Ordinal-Sequence of W,

H for ZF-formula;

    scheme :: ZF_REFLE:sch1

    ALFA9Universe { W() -> Universe , D() -> non empty set , P[ set, set] } :

ex F st ( dom F) = D() & for d be Element of D() holds ex a be Ordinal of W() st a = (F . d) & P[d, a] & for b be Ordinal of W() st P[d, b] holds a c= b

      provided

       A1: for d be Element of D() holds ex a be Ordinal of W() st P[d, a];

      

       A2: for d be Element of D() holds ex A st P[d, A]

      proof

        let d be Element of D();

        consider a be Ordinal of W() such that

         A3: P[d, a] by A1;

        reconsider a as Ordinal;

        take a;

        thus thesis by A3;

      end;

      consider F such that

       A4: ( dom F) = D() and

       A5: for d be Element of D() holds ex A st A = (F . d) & P[d, A] & for B st P[d, B] holds A c= B from ORDINAL1:sch 6( A2);

      take F;

      thus ( dom F) = D() by A4;

      let d be Element of D();

      consider A such that

       A6: A = (F . d) & P[d, A] and

       A7: for B st P[d, B] holds A c= B by A5;

      consider a be Ordinal of W() such that

       A8: P[d, a] by A1;

      A c= a by A7, A8;

      then

      reconsider a = A as Ordinal of W() by CLASSES1:def 1;

      take a;

      thus thesis by A6, A7;

    end;

    theorem :: ZF_REFLE:7

    x is Ordinal of W iff x in ( On W) by ORDINAL1:def 9;

    reserve psi for Ordinal-Sequence;

    scheme :: ZF_REFLE:sch2

    OrdSeqOfUnivEx { W() -> Universe , P[ object, object] } :

ex phi be Ordinal-Sequence of W() st for a be Ordinal of W() holds P[a, (phi . a)]

      provided

       A1: for a be Ordinal of W() holds ex b be Ordinal of W() st P[a, b];

      defpred Q[ object, object] means P[$1, $2] & $2 is Ordinal of W();

      

       A2: for x be object st x in ( On W()) holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in ( On W());

        then

        reconsider a = x as Ordinal of W() by ORDINAL1:def 9;

        consider b be Ordinal of W() such that

         A3: P[a, b] by A1;

        reconsider y = b as set;

        take y;

        thus thesis by A3;

      end;

      consider f be Function such that

       A4: ( dom f) = ( On W()) & for x be object st x in ( On W()) holds Q[x, (f . x)] from CLASSES1:sch 1( A2);

      reconsider phi = f as Sequence by A4, ORDINAL1:def 7;

      

       A5: ( rng phi) c= ( On W())

      proof

        let x be object;

        assume x in ( rng phi);

        then ex y be object st y in ( dom phi) & x = (phi . y) by FUNCT_1:def 3;

        then

        reconsider x as Ordinal of W() by A4;

        x in W();

        hence thesis by ORDINAL1:def 9;

      end;

      then

      reconsider phi as Ordinal-Sequence by ORDINAL2:def 4;

      reconsider phi as Ordinal-Sequence of W() by A4, A5, FUNCT_2:def 1, RELSET_1: 4;

      take phi;

      let a be Ordinal of W();

      a in ( On W()) by ORDINAL1:def 9;

      hence thesis by A4;

    end;

    scheme :: ZF_REFLE:sch3

    UOSExist { W() -> Universe , a() -> Ordinal of W() , C( Ordinal, Ordinal) -> Ordinal of W() , D( Ordinal, Sequence) -> Ordinal of W() } :

ex phi be Ordinal-Sequence of W() st (phi . ( 0-element_of W())) = a() & (for a be Ordinal of W() holds (phi . ( succ a)) = C(a,.)) & for a be Ordinal of W() st a <> ( 0-element_of W()) & a is limit_ordinal holds (phi . a) = D(a,|);

      consider phi be Ordinal-Sequence such that

       A1: ( dom phi) = ( On W()) and

       A2: 0 in ( On W()) implies (phi . 0 ) = a() and

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

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

      ( rng phi) c= ( On W())

      proof

        let x be object;

        assume x in ( rng phi);

        then

        consider y be object such that

         A5: y in ( dom phi) and

         A6: x = (phi . y) by FUNCT_1:def 3;

        reconsider y as Ordinal of W() by A1, A5, ORDINAL1:def 9;

         A7:

        now

          assume not ex A st y = ( succ A);

          then

           A8: y is limit_ordinal by ORDINAL1: 29;

          assume y <> {} ;

          then x = D(y,|) by A1, A4, A5, A6, A8;

          hence thesis by ORDINAL1:def 9;

        end;

        now

          given A such that

           A9: y = ( succ A);

          reconsider B = (phi . A) as Ordinal;

          x = C(A,B) by A1, A3, A5, A6, A9;

          hence thesis by ORDINAL1:def 9;

        end;

        hence thesis by A2, A6, A7, ORDINAL1:def 9;

      end;

      then

      reconsider phi as Ordinal-Sequence of W() by A1, FUNCT_2:def 1, RELSET_1: 4;

      take phi;

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

      hence (phi . ( 0-element_of W())) = a() by A1, A2, ORDINAL4: 33;

      thus for a be Ordinal of W() holds (phi . ( succ a)) = C(a,.) by A1, A3, ORDINAL4: 34;

      let a be Ordinal of W();

      a in ( dom phi) & {} = ( 0-element_of W()) by ORDINAL4: 33, ORDINAL4: 34;

      hence thesis by A4;

    end;

    scheme :: ZF_REFLE:sch4

    UniverseInd { W() -> Universe , P[ Ordinal] } :

for a be Ordinal of W() holds P[a]

      provided

       A1: P[( 0-element_of W())]

       and

       A2: for a be Ordinal of W() st P[a] holds P[( succ a)]

       and

       A3: for a be Ordinal of W() st a <> ( 0-element_of W()) & a is limit_ordinal & for b be Ordinal of W() st b in a holds P[b] holds P[a];

      defpred Q[ Ordinal] means $1 is Ordinal of W() implies P[$1];

      

       A4: for A st A <> 0 & A is limit_ordinal & for B st B in A holds Q[B] holds Q[A]

      proof

        let A such that

         A5: A <> 0 & A is limit_ordinal and

         A6: for B st B in A holds B is Ordinal of W() implies P[B];

        assume A is Ordinal of W();

        then

        reconsider a = A as Ordinal of W();

         {} = ( 0-element_of W()) & for b be Ordinal of W() st b in a holds P[b] by A6, ORDINAL4: 33;

        hence thesis by A3, A5;

      end;

      

       A7: for A st Q[A] holds Q[( succ A)]

      proof

        let A such that

         A8: A is Ordinal of W() implies P[A] and

         A9: ( succ A) is Ordinal of W();

        A in ( succ A) & ( succ A) in ( On W()) by A9, ORDINAL1: 6, ORDINAL1:def 9;

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

        then

        reconsider a = A as Ordinal of W() by ORDINAL1:def 9;

        P[( succ a)] by A2, A8;

        hence thesis;

      end;

      

       A10: Q[ 0 ] by A1, ORDINAL4: 33;

       Q[A] from ORDINAL2:sch 1( A10, A7, A4);

      hence thesis;

    end;

    definition

      let f be Function, W be Universe, a be Ordinal of W;

      :: ZF_REFLE:def1

      func union (f,a) -> set equals ( Union (W |` (f | ( Rank a))));

      correctness ;

    end

    theorem :: ZF_REFLE:8

    

     Th8: for L be Sequence, A holds (L | ( Rank A)) is Sequence

    proof

      let L be Sequence, A;

      

       A1: ( dom (L | ( Rank A))) = (( dom L) /\ ( Rank A)) by RELAT_1: 61;

      now

        let X;

        assume

         A2: X in ( dom (L | ( Rank A)));

        then

         A3: X in ( dom L) by A1, XBOOLE_0:def 4;

        hence X is Ordinal;

        X in ( Rank A) by A1, A2, XBOOLE_0:def 4;

        then

         A4: X c= ( Rank A) by ORDINAL1:def 2;

        X c= ( dom L) by A3, ORDINAL1:def 2;

        hence X c= ( dom (L | ( Rank A))) by A1, A4, XBOOLE_1: 19;

      end;

      then ( dom (L | ( Rank A))) is epsilon-transitive epsilon-connected set by ORDINAL1: 19;

      hence thesis by ORDINAL1: 31;

    end;

    theorem :: ZF_REFLE:9

    

     Th9: for L be Ordinal-Sequence, A holds (L | ( Rank A)) is Ordinal-Sequence

    proof

      let L be Ordinal-Sequence, A;

      reconsider K = (L | ( Rank A)) as Sequence by Th8;

      consider B such that

       A1: ( rng L) c= B by ORDINAL2:def 4;

      ( rng K) c= ( rng L) by RELAT_1: 70;

      then ( rng K) c= B by A1;

      hence thesis by ORDINAL2:def 4;

    end;

    theorem :: ZF_REFLE:10

    ( Union psi) is Ordinal;

    theorem :: ZF_REFLE:11

    

     Th11: ( Union (X |` psi)) is epsilon-transitive epsilon-connected set

    proof

      consider A such that

       A1: ( rng psi) c= A by ORDINAL2:def 4;

      

       A2: ( rng (X |` psi)) c= ( rng psi) by RELAT_1: 87;

       A3:

      now

        let x be object;

        assume x in ( rng (X |` psi));

        then x in A by A1, A2;

        hence x is Ordinal;

      end;

      ( Union (X |` psi)) = ( union ( rng (X |` psi))) by CARD_3:def 4;

      hence thesis by A3, ORDINAL1: 23;

    end;

    theorem :: ZF_REFLE:12

    

     Th12: ( On ( Rank A)) = A

    proof

      thus ( On ( Rank A)) c= A

      proof

        let x be object;

        assume

         A1: x in ( On ( Rank A));

        then

        reconsider B = x as Ordinal by ORDINAL1:def 9;

        x in ( Rank A) by A1, ORDINAL1:def 9;

        then ( the_rank_of B) in A by CLASSES1: 66;

        hence thesis by CLASSES1: 73;

      end;

      ( On A) c= ( On ( Rank A)) by CLASSES1: 38, ORDINAL2: 9;

      hence thesis by ORDINAL2: 8;

    end;

    theorem :: ZF_REFLE:13

    

     Th13: (psi | ( Rank A)) = (psi | A)

    proof

      ( dom (psi | ( Rank A))) c= ( dom psi) by RELAT_1: 60;

      then ( On ( dom (psi | ( Rank A)))) c= ( On ( Rank A)) & ( On ( dom (psi | ( Rank A)))) = ( dom (psi | ( Rank A))) by ORDINAL2: 9, ORDINAL3: 6, RELAT_1: 58;

      then

       A1: ( dom (psi | ( Rank A))) c= A by Th12;

      A c= ( Rank A) by CLASSES1: 38;

      then ((psi | ( Rank A)) | A) = (psi | A) by FUNCT_1: 51;

      hence thesis by A1, RELAT_1: 68;

    end;

    definition

      let phi be Ordinal-Sequence, W be Universe, a be Ordinal of W;

      :: original: union

      redefine

      func union (phi,a) -> Ordinal of W ;

      coherence

      proof

        reconsider K = (phi | ( Rank a)) as Ordinal-Sequence by Th9;

        reconsider A = ( Union (W |` K)) as Ordinal by Th11;

        a in ( On W) by ORDINAL1:def 9;

        then ( dom K) c= ( Rank a) & ( Rank a) in W by CLASSES2: 25, RELAT_1: 58;

        then ( dom (W |` K)) c= ( dom K) & ( dom K) in W by CLASSES1:def 1, FUNCT_1: 56;

        then ( dom (W |` K)) in W by CLASSES1:def 1;

        then

         A1: ( card ( dom (W |` K))) in ( card W) by CLASSES2: 1;

        ((W |` K) .: ( dom (W |` K))) = ( rng (W |` K)) by RELAT_1: 113;

        then ( rng (W |` K)) c= W & ( card ( rng (W |` K))) in ( card W) by A1, CARD_1: 67, ORDINAL1: 12, RELAT_1: 85;

        then

         A2: ( rng (W |` K)) in W by CLASSES1: 1;

        ( union ( rng (W |` K))) = ( Union (W |` K)) by CARD_3:def 4;

        then A in W by A2, CLASSES2: 59;

        hence thesis;

      end;

    end

    theorem :: ZF_REFLE:14

    

     Th14: for phi be Ordinal-Sequence of W holds ( union (phi,a)) = ( Union (phi | a)) & ( union ((phi | a),a)) = ( Union (phi | a))

    proof

      let phi be Ordinal-Sequence of W;

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

      then ( rng (phi | a)) c= ( rng phi) & ( rng phi) c= W by RELAT_1: 70;

      then a c= ( Rank a) & (phi | a) = (W |` (phi | a)) by CLASSES1: 38, RELAT_1: 94, XBOOLE_1: 1;

      hence thesis by Th13, FUNCT_1: 51;

    end;

    definition

      let W be Universe, a,b be Ordinal of W;

      :: original: \/

      redefine

      func a \/ b -> Ordinal of W ;

      coherence

      proof

        a c= b or b c= a;

        hence thesis by XBOOLE_1: 12;

      end;

    end

    registration

      let W;

      cluster non empty for Element of W;

      existence

      proof

        set u = the Element of W;

         {u} is non empty Element of W;

        hence thesis;

      end;

    end

    definition

      let W;

      mode Subclass of W is non empty Subset of W;

    end

    definition

      let W;

      let IT be Sequence of W;

      :: ZF_REFLE:def2

      attr IT is DOMAIN-yielding means

      : Def2: ( dom IT) = ( On W);

    end

    registration

      let W;

      cluster DOMAIN-yielding non-empty for Sequence of W;

      existence

      proof

        set D = the non empty Element of W;

        deffunc F( set) = D;

        consider L be Sequence such that

         A1: ( dom L) = ( On W) & for A holds for L1 be Sequence st A in ( On W) & L1 = (L | A) holds (L . A) = F(L1) from ORDINAL1:sch 4;

        ( rng L) c= W

        proof

          let x be object;

          assume x in ( rng L);

          then

          consider y be object such that

           A2: y in ( dom L) and

           A3: x = (L . y) by FUNCT_1:def 3;

          reconsider y as Ordinal by A2;

          (L | y) = (L | y);

          then x = D by A1, A2, A3;

          hence thesis;

        end;

        then

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

        take L;

        thus ( dom L) = ( On W) by A1;

        assume {} in ( rng L);

        then

        consider x be object such that

         A4: x in ( dom L) and

         A5: {} = (L . x) by FUNCT_1:def 3;

        reconsider x as Ordinal by A4;

        (L | x) = (L | x);

        hence contradiction by A1, A4, A5;

      end;

    end

    definition

      let W;

      mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding Sequence of W;

    end

    definition

      let W;

      let L be DOMAIN-Sequence of W;

      :: original: Union

      redefine

      func Union L -> Subclass of W ;

      coherence

      proof

        set a = the Ordinal of W;

        a in ( On W) by ORDINAL1:def 9;

        then a in ( dom L) by Def2;

        then (L . a) in ( rng L) by FUNCT_1:def 3;

        then (L . a) c= ( union ( rng L)) & (L . a) <> {} by ZFMISC_1: 74;

        then ( union ( rng L)) <> {} ;

        then

        reconsider S = ( Union L) as non empty set by CARD_3:def 4;

        ( rng L) c= W & ( Union L) = ( union ( rng L)) by CARD_3:def 4;

        then

         A1: ( Union L) c= ( union W) by ZFMISC_1: 77;

        S c= W

        proof

          let x be object;

          assume x in S;

          then

          consider X such that

           A2: x in X and

           A3: X in W by A1, TARSKI:def 4;

          X c= W by A3, ORDINAL1:def 2;

          hence thesis by A2;

        end;

        hence thesis;

      end;

      let a;

      :: original: .

      redefine

      func L . a -> non empty Element of W ;

      coherence

      proof

        a in ( On W) by ORDINAL1:def 9;

        then a in ( dom L) by Def2;

        then

         A4: (L . a) in ( rng L) by FUNCT_1:def 3;

        thus thesis by A4, RELAT_1:def 9;

      end;

    end

    reserve L for DOMAIN-Sequence of W,

n for Element of NAT ,

f for Function of VAR , (L . a);

    theorem :: ZF_REFLE:15

    

     Th15: a in ( dom L)

    proof

      a in ( On W) by ORDINAL1:def 9;

      hence thesis by Def2;

    end;

    theorem :: ZF_REFLE:16

    

     Th16: (L . a) c= ( Union L)

    proof

      a in ( dom L) by Th15;

      then

       A1: (L . a) in ( rng L) by FUNCT_1:def 3;

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

      hence thesis by A1, ZFMISC_1: 74;

    end;

    theorem :: ZF_REFLE:17

    

     Th17: ( NAT , VAR ) are_equipotent

    proof

      deffunc F( Nat, set) = (5 + ($1 + 1));

      consider f be sequence of NAT such that

       A1: (f . 0 ) = (5 + 0 ) & for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 12;

       A2:

      now

        let n;

        (ex j be Nat st n = (j + 1)) implies (f . n) = (5 + n) by A1;

        then n = 0 or (f . n) = (5 + n) by NAT_1: 6;

        hence (f . n) = (5 + n) by A1;

      end;

      

       A3: ( dom f) = NAT by FUNCT_2:def 1;

      thus ( NAT , VAR ) are_equipotent

      proof

        reconsider g = f as Function;

        take g;

        thus g is one-to-one

        proof

          let x,y be object;

          assume x in ( dom g) & y in ( dom g);

          then

          reconsider n1 = x, n2 = y as Element of NAT by FUNCT_2:def 1;

          (f . n1) = (5 + n1) & (f . n2) = (5 + n2) by A2;

          hence thesis by XCMPLX_1: 2;

        end;

        thus ( dom g) = NAT by FUNCT_2:def 1;

        thus ( rng g) c= VAR

        proof

          let x be object;

          assume x in ( rng g);

          then

          consider y be object such that

           A4: y in ( dom f) and

           A5: x = (f . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A4;

          

           A6: (5 + y) >= 5 by NAT_1: 11;

          x = (5 + y) by A2, A5;

          hence thesis by A6;

        end;

        let x be object;

        assume x in VAR ;

        then ex n st x = n & 5 <= n;

        then

        consider n be Nat such that

         A7: x = (5 + n) by NAT_1: 10;

        

         A8: n in NAT by ORDINAL1:def 12;

        then (f . n) = x by A2, A7;

        hence thesis by A3, A8, FUNCT_1:def 3;

      end;

    end;

    theorem :: ZF_REFLE:18

    ( sup X) c= ( succ ( union ( On X))) by ORDINAL3: 72;

    theorem :: ZF_REFLE:19

    

     Th19: X in W implies ( sup X) in W

    proof

      reconsider a = ( union ( On X)) as Ordinal by ORDINAL3: 5;

      

       A1: ( On X) c= X by ORDINAL2: 7;

      assume X in W;

      then ( On X) in W by A1, CLASSES1:def 1;

      then

      reconsider a as Ordinal of W by CLASSES2: 59;

      ( sup X) c= ( succ a) by ORDINAL3: 72;

      hence thesis by CLASSES1:def 1;

    end;

    reserve x1 for Variable;

    ::$Notion-Name

    theorem :: ZF_REFLE:20

     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 for H holds ex phi st phi is increasing & phi is continuous & for a st (phi . a) = a & {} <> a holds for f holds (( Union L),(( Union L) ! f)) |= H iff ((L . a),f) |= H

    proof

      assume that

       A1: omega in W and

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

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

      set M = ( Union L);

      

       A4: ( union ( rng L)) = M by CARD_3:def 4;

      defpred RT[ ZF-formula] means ex phi st phi is increasing & phi is continuous & for a st (phi . a) = a & {} <> a holds for f holds (M,(M ! f)) |= $1 iff ((L . a),f) |= $1;

      

       A5: ( dom L) = ( On W) by Def2;

      

       A6: for H st H is universal & RT[( the_scope_of H)] holds RT[H]

      proof

        deffunc D( Ordinal of W, Ordinal-Sequence) = ( union ($2,$1));

        let H;

        set x0 = ( bound_in H);

        set H9 = ( the_scope_of H);

        defpred P[ set, set] means ex f be Function of VAR , M st $1 = f & ((ex m be Element of M st m in (L . $2) & (M,(f / (x0,m))) |= ( 'not' H9)) or $2 = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9));

        assume H is universal;

        then

         A7: H = ( All (( bound_in H),( the_scope_of H))) by ZF_LANG: 44;

        

         A8: for h be Element of ( Funcs ( VAR ,M)) qua non empty set holds ex a st P[h, a]

        proof

          let h be Element of ( Funcs ( VAR ,M)) qua non empty set;

          reconsider f = h as Element of ( Funcs ( VAR ,M));

          reconsider f as Function of VAR , M;

          now

            per cases ;

              suppose for m be Element of M holds not (M,(f / (x0,m))) |= ( 'not' H9);

              hence thesis;

            end;

              suppose

               A9: not for m be Element of M holds not (M,(f / (x0,m))) |= ( 'not' H9);

              thus thesis

              proof

                consider m be Element of M such that

                 A10: (M,(f / (x0,m))) |= ( 'not' H9) by A9;

                consider X be set such that

                 A11: m in X and

                 A12: X in ( rng L) by A4, TARSKI:def 4;

                consider x be object such that

                 A13: x in ( dom L) and

                 A14: X = (L . x) by A12, FUNCT_1:def 3;

                reconsider x as Ordinal by A13;

                reconsider b = x as Ordinal of W by A5, A13, ORDINAL1:def 9;

                take b, f;

                thus thesis by A10, A11, A14;

              end;

            end;

          end;

          hence thesis;

        end;

        consider rho be Function such that

         A15: ( dom rho) = ( Funcs ( VAR ,M)) qua non empty set and

         A16: for h be Element of ( Funcs ( VAR ,M)) qua non empty set holds ex a st a = (rho . h) & P[h, a] & for b st P[h, b] holds a c= b from ALFA9Universe( A8);

        defpred SI[ Ordinal of W, Ordinal of W] means $2 = ( sup (rho .: ( Funcs ( VAR ,(L . $1)))));

        

         A17: for a holds ex b st SI[a, b]

        proof

          let a;

          set X = (rho .: ( Funcs ( VAR ,(L . a))));

          

           A18: X c= W

          proof

            let x be object;

            assume x in X;

            then

            consider h be object such that h in ( dom rho) and

             A19: h in ( Funcs ( VAR ,(L . a))) and

             A20: x = (rho . h) by FUNCT_1:def 6;

            ( Funcs ( VAR ,(L . a))) c= ( Funcs ( VAR ,M)) by Th16, FUNCT_5: 56;

            then

            reconsider h as Element of ( Funcs ( VAR ,M)) qua non empty set by A19;

            ex a st a = (rho . h) & (ex f be Function of VAR , M st h = f & ((ex m be Element of M st m in (L . a) & (M,(f / (x0,m))) |= ( 'not' H9)) or a = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9))) & for b st ex f be Function of VAR , M st h = f & ((ex m be Element of M st m in (L . b) & (M,(f / (x0,m))) |= ( 'not' H9)) or b = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9)) holds a c= b by A16;

            hence thesis by A20;

          end;

          ( Funcs ( omega ,(L . a))) in W by A1, CLASSES2: 61;

          then

           A21: ( card ( Funcs ( omega ,(L . a)))) in ( card W) by CLASSES2: 1;

          ( card VAR ) = ( card omega ) & ( card (L . a)) = ( card (L . a)) by Th17, CARD_1: 5;

          then ( card ( Funcs ( VAR ,(L . a)))) = ( card ( Funcs ( omega ,(L . a)))) by FUNCT_5: 61;

          then ( card X) in ( card W) by A21, CARD_1: 67, ORDINAL1: 12;

          then X in W by A18, CLASSES1: 1;

          then

          reconsider b = ( sup X) as Ordinal of W by Th19;

          take b;

          thus thesis;

        end;

        consider si be Ordinal-Sequence of W such that

         A22: for a holds SI[a, (si . a)] from OrdSeqOfUnivEx( A17);

        deffunc C( Ordinal of W, Ordinal of W) = ( succ ((si . ( succ $1)) \/ $2));

        consider ksi be Ordinal-Sequence of W such that

         A23: (ksi . ( 0-element_of W)) = (si . ( 0-element_of W)) and

         A24: for a holds (ksi . ( succ a)) = C(a,.) and

         A25: for a st a <> ( 0-element_of W) & a is limit_ordinal holds (ksi . a) = D(a,|) from UOSExist;

        defpred P[ Ordinal] means (si . $1) c= (ksi . $1);

        given phi such that

         A26: phi is increasing and

         A27: phi is continuous and

         A28: for a st (phi . a) = a & {} <> a holds for f holds (M,(M ! f)) |= ( the_scope_of H) iff ((L . a),f) |= ( the_scope_of H);

        

         A29: ksi is increasing

        proof

          let A, B;

          assume that

           A30: A in B and

           A31: B in ( dom ksi);

          A in ( dom ksi) by A30, A31, ORDINAL1: 10;

          then

          reconsider a = A, b = B as Ordinal of W by A31, ORDINAL1:def 9;

          defpred Theta[ Ordinal of W] means a in $1 implies (ksi . a) in (ksi . $1);

          

           A32: Theta[c] implies Theta[( succ c)]

          proof

            assume that

             A33: a in c implies (ksi . a) in (ksi . c) and

             A34: a in ( succ c);

            

             A35: a c= c by A34, ORDINAL1: 22;

            

             A36: (ksi . a) in (ksi . c) or (ksi . a) = (ksi . c)

            proof

              per cases ;

                suppose a <> c;

                then a c< c by A35;

                hence thesis by A33, ORDINAL1: 11;

              end;

                suppose a = c;

                hence thesis;

              end;

            end;

            

             A37: (ksi . c) c= ((si . ( succ c)) \/ (ksi . c)) by XBOOLE_1: 7;

            (ksi . ( succ c)) = ( succ ((si . ( succ c)) \/ (ksi . c))) & ((si . ( succ c)) \/ (ksi . c)) in ( succ ((si . ( succ c)) \/ (ksi . c))) by A24, ORDINAL1: 22;

            hence thesis by A37, A36, ORDINAL1: 10, ORDINAL1: 12;

          end;

          

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

          proof

            (ksi . ( succ a)) = ( succ ((si . ( succ a)) \/ (ksi . a))) by A24;

            then ((si . ( succ a)) \/ (ksi . a)) in (ksi . ( succ a)) by ORDINAL1: 6;

            then

             A39: (ksi . a) in (ksi . ( succ a)) by ORDINAL1: 12, XBOOLE_1: 7;

            let b such that

             A40: b <> ( 0-element_of W) and

             A41: b is limit_ordinal and for c st c in b holds Theta[c] and

             A42: a in b;

            ( succ a) in ( dom ksi) & ( succ a) in b by A41, A42, ORDINAL1: 28, ORDINAL4: 34;

            then

             A43: (ksi . ( succ a)) in ( rng (ksi | b)) by FUNCT_1: 50;

            (ksi . b) = ( union ((ksi | b),b)) by A25, A40, A41

            .= ( Union (ksi | b)) by Th14

            .= ( union ( rng (ksi | b))) by CARD_3:def 4;

            hence thesis by A43, A39, TARSKI:def 4;

          end;

          

           A44: Theta[( 0-element_of W)] by ORDINAL4: 33;

           Theta[c] from UniverseInd( A44, A32, A38);

          then (ksi . a) in (ksi . b) by A30;

          hence thesis;

        end;

        

         A45: ( 0-element_of W) = {} by ORDINAL4: 33;

        

         A46: ksi is continuous

        proof

          let A, B;

          assume that

           A47: A in ( dom ksi) and

           A48: A <> 0 and

           A49: A is limit_ordinal and

           A50: B = (ksi . A);

          A c= ( dom ksi) by A47, ORDINAL1:def 2;

          then

           A51: ( dom (ksi | A)) = A by RELAT_1: 62;

          reconsider a = A as Ordinal of W by A47, ORDINAL1:def 9;

          

           A52: B = ( union ((ksi | a),a)) by A25, A45, A48, A49, A50

          .= ( Union (ksi | a)) by Th14

          .= ( union ( rng (ksi | a))) by CARD_3:def 4;

          

           A53: B c= ( sup (ksi | A))

          proof

            let C;

            assume C in B;

            then

            consider X such that

             A54: C in X and

             A55: X in ( rng (ksi | A)) by A52, TARSKI:def 4;

            ( rng (ksi | A)) c= ( rng ksi) by RELAT_1: 70;

            then X in ( rng ksi) by A55;

            then

            reconsider X as Ordinal;

            X in ( sup (ksi | A)) by A55, ORDINAL2: 19;

            hence thesis by A54, ORDINAL1: 10;

          end;

          

           A56: (ksi | A) is increasing by A29, ORDINAL4: 15;

          

           A57: ( sup (ksi | A)) c= B

          proof

            let C;

            assume C in ( sup (ksi | A));

            then

            consider D be Ordinal such that

             A58: D in ( rng (ksi | A)) and

             A59: C c= D by ORDINAL2: 21;

            consider x be object such that

             A60: x in ( dom (ksi | A)) and

             A61: D = ((ksi | A) . x) by A58, FUNCT_1:def 3;

            reconsider x as Ordinal by A60;

            

             A62: ( succ x) in A by A49, A60, ORDINAL1: 28;

            then

             A63: ((ksi | A) . ( succ x)) in ( rng (ksi | A)) by A51, FUNCT_1:def 3;

            x in ( succ x) by ORDINAL1: 6;

            then D in ((ksi | A) . ( succ x)) by A51, A56, A61, A62;

            then D in B by A52, A63, TARSKI:def 4;

            hence thesis by A59, ORDINAL1: 12;

          end;

          ( sup (ksi | A)) is_limes_of (ksi | A) by A48, A49, A51, A56, ORDINAL4: 8;

          hence thesis by A53, A57, XBOOLE_0:def 10;

        end;

        

         A64: a <> ( 0-element_of W) & a is limit_ordinal implies (si . a) c= ( sup (si | a))

        proof

          defpred C[ object] means $1 in ( Free ( 'not' H9));

          assume that

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

           A66: a is limit_ordinal;

          

           A67: (si . a) = ( sup (rho .: ( Funcs ( VAR ,(L . a))))) by A22;

          let A;

          assume A in (si . a);

          then

          consider B such that

           A68: B in (rho .: ( Funcs ( VAR ,(L . a)))) and

           A69: A c= B by A67, ORDINAL2: 21;

          consider x be object such that

           A70: x in ( dom rho) and

           A71: x in ( Funcs ( VAR ,(L . a))) and

           A72: B = (rho . x) by A68, FUNCT_1:def 6;

          reconsider h = x as Element of ( Funcs ( VAR ,M)) qua non empty set by A15, A70;

          consider a1 be Ordinal of W such that

           A73: a1 = (rho . h) and

           A74: ex f be Function of VAR , M st h = f & ((ex m be Element of M st m in (L . a1) & (M,(f / (x0,m))) |= ( 'not' H9)) or a1 = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9)) and

           A75: for b st ex f be Function of VAR , M st h = f & ((ex m be Element of M st m in (L . b) & (M,(f / (x0,m))) |= ( 'not' H9)) or b = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9)) holds a1 c= b by A16;

          consider f be Function of VAR , M such that

           A76: h = f and

           A77: (ex m be Element of M st m in (L . a1) & (M,(f / (x0,m))) |= ( 'not' H9)) or a1 = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9) by A74;

          defpred P[ object, object] means for a st (f . $1) in (L . a) holds (f . $2) in (L . a);

           A78:

          now

            

             A79: for x,y be object holds P[x, y] or P[y, x]

            proof

              let x,y be object;

              given a such that

               A80: (f . x) in (L . a) & not (f . y) in (L . a);

              let b such that

               A81: (f . y) in (L . b);

              a in b or a = b or b in a by ORDINAL1: 14;

              then (L . a) c= (L . b) or (L . b) c= (L . a) by A2;

              hence thesis by A80, A81;

            end;

            assume ( Free ( 'not' H9)) <> {} ;

            then

             A82: ( Free ( 'not' H9)) <> {} ;

            

             A83: (L . a) = ( Union (L | a)) & ( Union (L | a)) = ( union ( rng (L | a))) by A3, A45, A65, A66, CARD_3:def 4;

            

             A84: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z];

            consider z be object such that

             A85: z in ( Free ( 'not' H9)) & for y be object st y in ( Free ( 'not' H9)) holds P[z, y] from CARD_2:sch 2( A82, A79, A84);

            reconsider z as Variable by A85;

            

             A86: ( dom (L | a)) c= a by RELAT_1: 58;

            

             A87: ex s be Function st f = s & ( dom s) = VAR & ( rng s) c= (L . a) by A71, A76, FUNCT_2:def 2;

            then (f . z) in ( rng f) by FUNCT_1:def 3;

            then

            consider X such that

             A88: (f . z) in X and

             A89: X in ( rng (L | a)) by A87, A83, TARSKI:def 4;

            consider x be object such that

             A90: x in ( dom (L | a)) and

             A91: X = ((L | a) . x) by A89, FUNCT_1:def 3;

            

             A92: ((L | a) . x) = (L . x) by A90, FUNCT_1: 47;

            reconsider x as Ordinal by A90;

            a in ( On W) by ORDINAL1:def 9;

            then x in ( On W) by A90, A86, ORDINAL1: 10;

            then

            reconsider x as Ordinal of W by ORDINAL1:def 9;

            take x;

            thus x in a by A90, A86;

            let y be Variable;

            assume y in ( Free ( 'not' H9));

            hence (f . y) in (L . x) by A85, A88, A91, A92;

          end;

          now

            assume

             A93: ( Free ( 'not' H9)) = {} ;

            take b = ( 0-element_of W);

            thus b in a by A45, A65, ORDINAL3: 8;

            thus for x1 st x1 in ( Free ( 'not' H9)) holds (f . x1) in (L . b) by A93;

          end;

          then

          consider c such that

           A94: c in a and

           A95: for x1 st x1 in ( Free ( 'not' H9)) holds (f . x1) in (L . c) by A78;

          

           A96: (si . c) = ( sup (rho .: ( Funcs ( VAR ,(L . c))))) by A22;

          c in ( dom si) & ( dom (si | a)) = (( dom si) /\ a) by ORDINAL4: 34, RELAT_1: 61;

          then

           A97: c in ( dom (si | a)) by A94, XBOOLE_0:def 4;

          (si . c) = ((si | a) . c) by A94, FUNCT_1: 49;

          then (si . c) in ( rng (si | a)) by A97, FUNCT_1:def 3;

          then

           A98: (si . c) in ( sup (si | a)) by ORDINAL2: 19;

          deffunc F( object) = (f . $1);

          set e = the Element of (L . c);

          deffunc G( object) = e;

          consider v be Function such that

           A99: ( dom v) = VAR & for x be object st x in VAR holds ( C[x] implies (v . x) = F(x)) & ( not C[x] implies (v . x) = G(x)) from PARTFUN1:sch 1;

          

           A100: ( rng v) c= (L . c)

          proof

            let x be object;

            assume x in ( rng v);

            then

            consider y be object such that

             A101: y in ( dom v) and

             A102: x = (v . y) by FUNCT_1:def 3;

            reconsider y as Variable by A99, A101;

            y in ( Free ( 'not' H9)) or not y in ( Free ( 'not' H9));

            then x = (f . y) & (f . y) in (L . c) or x = e by A95, A99, A102;

            hence thesis;

          end;

          then

          reconsider v as Function of VAR , (L . c) by A99, FUNCT_2:def 1, RELSET_1: 4;

          

           A103: v in ( Funcs ( VAR ,(L . c))) by A99, A100, FUNCT_2:def 2;

          ( Funcs ( VAR ,(L . c))) c= ( Funcs ( VAR ,M)) by Th16, FUNCT_5: 56;

          then

          reconsider v9 = v as Element of ( Funcs ( VAR ,M)) qua non empty set by A103;

          consider a2 be Ordinal of W such that

           A104: a2 = (rho . v9) and

           A105: ex f be Function of VAR , M st v9 = f & ((ex m be Element of M st m in (L . a2) & (M,(f / (x0,m))) |= ( 'not' H9)) or a2 = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9)) and

           A106: for b st ex f be Function of VAR , M st v9 = f & ((ex m be Element of M st m in (L . b) & (M,(f / (x0,m))) |= ( 'not' H9)) or b = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9)) holds a2 c= b by A16;

          consider f9 be Function of VAR , M such that

           A107: v9 = f9 and

           A108: (ex m be Element of M st m in (L . a2) & (M,(f9 / (x0,m))) |= ( 'not' H9)) or a2 = ( 0-element_of W) & not ex m be Element of M st (M,(f9 / (x0,m))) |= ( 'not' H9) by A105;

          

           A109: v = (M ! v) by Th16, ZF_LANG1:def 1;

           A110:

          now

            given m be Element of M such that

             A111: m in (L . a1) and

             A112: (M,(f / (x0,m))) |= ( 'not' H9);

             A113:

            now

              let x1;

              

               A114: ((f / (x0,m)) . x0) = m by FUNCT_7: 128;

              

               A115: x1 <> x0 implies ((f / (x0,m)) . x1) = (f . x1) & (((M ! v) / (x0,m)) . x1) = ((M ! v) . x1) by FUNCT_7: 32;

              assume x1 in ( Free ( 'not' H9));

              hence ((f / (x0,m)) . x1) = (((M ! v) / (x0,m)) . x1) by A99, A109, A114, A115, FUNCT_7: 128;

            end;

            then (M,((M ! v) / (x0,m))) |= ( 'not' H9) by A112, ZF_LANG1: 75;

            then

            consider m9 be Element of M such that

             A116: m9 in (L . a2) & (M,(f9 / (x0,m9))) |= ( 'not' H9) by A109, A107, A108;

            now

              let x1;

              

               A117: ((f / (x0,m9)) . x0) = m9 by FUNCT_7: 128;

              

               A118: x1 <> x0 implies ((f / (x0,m9)) . x1) = (f . x1) & (((M ! v) / (x0,m9)) . x1) = ((M ! v) . x1) by FUNCT_7: 32;

              assume x1 in ( Free ( 'not' H9));

              hence ((f / (x0,m9)) . x1) = ((f9 / (x0,m9)) . x1) by A99, A109, A107, A117, A118, FUNCT_7: 128;

            end;

            then

             A119: a1 c= a2 by A75, A76, A116, ZF_LANG1: 75;

            a2 c= a1 by A109, A106, A111, A112, A113, ZF_LANG1: 75;

            hence a1 = a2 by A119;

          end;

          now

            assume

             A120: not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9);

            now

              let m be Element of M;

              now

                let x1;

                

                 A121: ((f / (x0,m)) . x0) = m by FUNCT_7: 128;

                

                 A122: x1 <> x0 implies ((f / (x0,m)) . x1) = (f . x1) & (((M ! v) / (x0,m)) . x1) = ((M ! v) . x1) by FUNCT_7: 32;

                assume x1 in ( Free ( 'not' H9));

                hence ((f / (x0,m)) . x1) = (((M ! v) / (x0,m)) . x1) by A99, A109, A121, A122, FUNCT_7: 128;

              end;

              hence not (M,((M ! v) / (x0,m))) |= ( 'not' H9) by A120, ZF_LANG1: 75;

            end;

            hence a1 = a2 by A77, A109, A107, A108, A120;

          end;

          then B in (rho .: ( Funcs ( VAR ,(L . c)))) by A15, A72, A73, A74, A76, A103, A104, A110, FUNCT_1:def 6;

          then B in (si . c) by A96, ORDINAL2: 19;

          then B in ( sup (si | a)) by A98, ORDINAL1: 10;

          hence thesis by A69, ORDINAL1: 12;

        end;

        

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

        proof

          assume that

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

           A125: for b st b in a holds (si . b) c= (ksi . b);

          thus (si . a) c= (ksi . a)

          proof

            

             A126: (si . a) c= ( sup (si | a)) by A64, A124;

            let A;

            assume A in (si . a);

            then

            consider B such that

             A127: B in ( rng (si | a)) and

             A128: A c= B by A126, ORDINAL2: 21;

            consider x be object such that

             A129: x in ( dom (si | a)) and

             A130: B = ((si | a) . x) by A127, FUNCT_1:def 3;

            reconsider x as Ordinal by A129;

            

             A131: a in ( On W) by ORDINAL1:def 9;

            x in ( dom si) by A129, RELAT_1: 57;

            then x in ( On W);

            then

            reconsider x as Ordinal of W by ORDINAL1:def 9;

            

             A132: (si . x) = B by A129, A130, FUNCT_1: 47;

            

             A133: (si . x) c= (ksi . x) by A125, A129;

            ( dom ksi) = ( On W) by FUNCT_2:def 1;

            then (ksi . x) in (ksi . a) by A29, A129, A131;

            hence thesis by A128, A132, A133, ORDINAL1: 12, XBOOLE_1: 1;

          end;

        end;

        

         A134: P[a] implies P[( succ a)]

        proof

          assume (si . a) c= (ksi . a);

          (ksi . ( succ a)) = ( succ ((si . ( succ a)) \/ (ksi . a))) & ((si . ( succ a)) \/ (ksi . a)) in ( succ ((si . ( succ a)) \/ (ksi . a))) by A24, ORDINAL1: 6;

          then (si . ( succ a)) in (ksi . ( succ a)) by ORDINAL1: 12, XBOOLE_1: 7;

          hence (si . ( succ a)) c= (ksi . ( succ a)) by ORDINAL1:def 2;

        end;

        

         A135: P[( 0-element_of W)] by A23;

        

         A136: P[a] from UniverseInd( A135, A134, A123);

         A137:

        now

          assume x0 in ( Free H9);

          thus thesis

          proof

            take gamma = (phi * ksi);

            ex f be Ordinal-Sequence st f = (phi * ksi) & f is increasing by A26, A29, ORDINAL4: 13;

            hence gamma is increasing & gamma is continuous by A27, A29, A46, ORDINAL4: 17;

            let a such that

             A138: (gamma . a) = a and

             A139: {} <> a;

            let f;

            a in ( dom gamma) by ORDINAL4: 34;

            then

             A140: (phi . (ksi . a)) = (gamma . a) by FUNCT_1: 12;

            a in ( dom ksi) by ORDINAL4: 34;

            then

             A141: a c= (ksi . a) by A29, ORDINAL4: 10;

            (ksi . a) in ( dom phi) by ORDINAL4: 34;

            then

             A142: (ksi . a) c= (phi . (ksi . a)) by A26, ORDINAL4: 10;

            then

             A143: (ksi . a) = a by A138, A141, A140;

            

             A144: (phi . a) = a by A138, A142, A141, A140, XBOOLE_0:def 10;

            thus (M,(M ! f)) |= H implies ((L . a),f) |= H

            proof

              assume

               A145: (M,(M ! f)) |= H;

              now

                let g be Function of VAR , (L . a) such that

                 A146: for k st (g . k) <> (f . k) holds x0 = k;

                now

                  let k;

                  (M ! f) = f & (M ! g) = g by Th16, ZF_LANG1:def 1;

                  hence ((M ! g) . k) <> ((M ! f) . k) implies x0 = k by A146;

                end;

                then (M,(M ! g)) |= H9 by A7, A145, ZF_MODEL: 16;

                hence ((L . a),g) |= H9 by A28, A139, A144;

              end;

              hence thesis by A7, ZF_MODEL: 16;

            end;

            assume that

             A147: ((L . a),f) |= H and

             A148: not (M,(M ! f)) |= H;

            consider m be Element of M such that

             A149: not (M,((M ! f) / (x0,m))) |= H9 by A7, A148, ZF_LANG1: 71;

            

             A150: (si . a) c= (ksi . a) by A136;

            

             A151: (si . a) = ( sup (rho .: ( Funcs ( VAR ,(L . a))))) by A22;

            reconsider h = (M ! f) as Element of ( Funcs ( VAR ,M)) qua non empty set by FUNCT_2: 8;

            consider a1 be Ordinal of W such that

             A152: a1 = (rho . h) and

             A153: ex f be Function of VAR , M st h = f & ((ex m be Element of M st m in (L . a1) & (M,(f / (x0,m))) |= ( 'not' H9)) or a1 = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9)) and for b st ex f be Function of VAR , M st h = f & ((ex m be Element of M st m in (L . b) & (M,(f / (x0,m))) |= ( 'not' H9)) or b = ( 0-element_of W) & not ex m be Element of M st (M,(f / (x0,m))) |= ( 'not' H9)) holds a1 c= b by A16;

            

             A154: (M ! f) = f by Th16, ZF_LANG1:def 1;

            (M,((M ! f) / (x0,m))) |= ( 'not' H9) by A149, ZF_MODEL: 14;

            then

            consider m be Element of M such that

             A155: m in (L . a1) and

             A156: (M,((M ! f) / (x0,m))) |= ( 'not' H9) by A153;

            f in ( Funcs ( VAR ,(L . a))) by FUNCT_2: 8;

            then a1 in (rho .: ( Funcs ( VAR ,(L . a)))) by A15, A152, A154, FUNCT_1:def 6;

            then a1 in (si . a) by A151, ORDINAL2: 19;

            then (L . a1) c= (L . a) by A2, A143, A150;

            then

            reconsider m9 = m as Element of (L . a) by A155;

            ((M ! f) / (x0,m)) = (M ! (f / (x0,m9))) by A154, Th16, ZF_LANG1:def 1;

            then not (M,(M ! (f / (x0,m9)))) |= H9 by A156, ZF_MODEL: 14;

            then not ((L . a),(f / (x0,m9))) |= H9 by A28, A139, A144;

            hence contradiction by A7, A147, ZF_LANG1: 71;

          end;

        end;

        now

          assume

           A157: not x0 in ( Free H9);

          thus thesis

          proof

            take phi;

            thus phi is increasing & phi is continuous by A26, A27;

            let a such that

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

            let f;

            thus (M,(M ! f)) |= H implies ((L . a),f) |= H

            proof

              

               A159: for k st ((M ! f) . k) <> ((M ! f) . k) holds x0 = k;

              assume (M,(M ! f)) |= H;

              then (M,(M ! f)) |= H9 by A7, A159, ZF_MODEL: 16;

              then ((L . a),f) |= H9 by A28, A158;

              hence thesis by A7, A157, ZFMODEL1: 10;

            end;

            

             A160: for k st (f . k) <> (f . k) holds x0 = k;

            assume ((L . a),f) |= H;

            then ((L . a),f) |= H9 by A7, A160, ZF_MODEL: 16;

            then (M,(M ! f)) |= H9 by A28, A158;

            hence thesis by A7, A157, ZFMODEL1: 10;

          end;

        end;

        hence thesis by A137;

      end;

      

       A161: for H st H is conjunctive & RT[( the_left_argument_of H)] & RT[( the_right_argument_of H)] holds RT[H]

      proof

        let H;

        assume H is conjunctive;

        then

         A162: H = (( the_left_argument_of H) '&' ( the_right_argument_of H)) by ZF_LANG: 40;

        given fi1 be Ordinal-Sequence of W such that

         A163: fi1 is increasing and

         A164: fi1 is continuous and

         A165: for a st (fi1 . a) = a & {} <> a holds for f holds (M,(M ! f)) |= ( the_left_argument_of H) iff ((L . a),f) |= ( the_left_argument_of H);

        given fi2 be Ordinal-Sequence of W such that

         A166: fi2 is increasing and

         A167: fi2 is continuous and

         A168: for a st (fi2 . a) = a & {} <> a holds for f holds (M,(M ! f)) |= ( the_right_argument_of H) iff ((L . a),f) |= ( the_right_argument_of H);

        take phi = (fi2 * fi1);

        ex fi st fi = (fi2 * fi1) & fi is increasing by A163, A166, ORDINAL4: 13;

        hence phi is increasing & phi is continuous by A163, A164, A167, ORDINAL4: 17;

        let a such that

         A169: (phi . a) = a and

         A170: {} <> a;

        a in ( dom fi1) by ORDINAL4: 34;

        then

         A171: a c= (fi1 . a) by A163, ORDINAL4: 10;

        let f;

        

         A172: a in ( dom phi) by ORDINAL4: 34;

        

         A173: a in ( dom fi2) by ORDINAL4: 34;

         A174:

        now

          assume (fi1 . a) <> a;

          then a c< (fi1 . a) by A171;

          then

           A175: a in (fi1 . a) by ORDINAL1: 11;

          

           A176: (phi . a) = (fi2 . (fi1 . a)) by A172, FUNCT_1: 12;

          (fi1 . a) in ( dom fi2) by ORDINAL4: 34;

          then (fi2 . a) in (fi2 . (fi1 . a)) by A166, A175;

          hence contradiction by A166, A169, A173, A176, ORDINAL1: 5, ORDINAL4: 10;

        end;

        then

         A177: (fi2 . a) = a by A169, A172, FUNCT_1: 12;

        thus (M,(M ! f)) |= H implies ((L . a),f) |= H

        proof

          assume

           A178: (M,(M ! f)) |= H;

          then (M,(M ! f)) |= ( the_right_argument_of H) by A162, ZF_MODEL: 15;

          then

           A179: ((L . a),f) |= ( the_right_argument_of H) by A168, A170, A177;

          (M,(M ! f)) |= ( the_left_argument_of H) by A162, A178, ZF_MODEL: 15;

          then ((L . a),f) |= ( the_left_argument_of H) by A165, A170, A174;

          hence thesis by A162, A179, ZF_MODEL: 15;

        end;

        assume

         A180: ((L . a),f) |= H;

        then ((L . a),f) |= ( the_right_argument_of H) by A162, ZF_MODEL: 15;

        then

         A181: (M,(M ! f)) |= ( the_right_argument_of H) by A168, A170, A177;

        ((L . a),f) |= ( the_left_argument_of H) by A162, A180, ZF_MODEL: 15;

        then (M,(M ! f)) |= ( the_left_argument_of H) by A165, A170, A174;

        hence thesis by A162, A181, ZF_MODEL: 15;

      end;

      

       A182: for H st H is atomic holds RT[H]

      proof

        

         A183: ( dom ( id ( On W))) = ( On W);

        then

        reconsider phi = ( id ( On W)) as Sequence by ORDINAL1:def 7;

        

         A184: ( rng ( id ( On W))) = ( On W);

        reconsider phi as Ordinal-Sequence;

        reconsider phi as Ordinal-Sequence of W by A183, A184, FUNCT_2:def 1, RELSET_1: 4;

        let H such that

         A185: H is being_equality or H is being_membership;

        take phi;

        thus

         A186: phi is increasing

        proof

          let A, B;

          assume

           A187: A in B & B in ( dom phi);

          then (phi . A) = A by FUNCT_1: 18, ORDINAL1: 10;

          hence thesis by A187, FUNCT_1: 18;

        end;

        thus phi is continuous

        proof

          let A, B;

          assume that

           A188: A in ( dom phi) and

           A189: A <> 0 & A is limit_ordinal and

           A190: B = (phi . A);

          

           A191: A c= ( dom phi) by A188, ORDINAL1:def 2;

          (phi | A) = (phi * ( id A)) by RELAT_1: 65

          .= ( id (( dom phi) /\ A)) by FUNCT_1: 22

          .= ( id A) by A191, XBOOLE_1: 28;

          then

           A192: ( rng (phi | A)) = A;

          (phi . A) = A by A188, FUNCT_1: 18;

          then

           A193: ( sup (phi | A)) = B by A190, A192, ORDINAL2: 18;

          

           A194: (phi | A) is increasing by A186, ORDINAL4: 15;

          ( dom (phi | A)) = A by A191, RELAT_1: 62;

          hence thesis by A189, A193, A194, ORDINAL4: 8;

        end;

        let a such that (phi . a) = a and {} <> a;

        let f;

        thus (M,(M ! f)) |= H implies ((L . a),f) |= H

        proof

          assume

           A195: (M,(M ! f)) |= H;

          

           A196: (M ! f) = f by Th16, ZF_LANG1:def 1;

           A197:

          now

            assume H is being_membership;

            then

             A198: H = (( Var1 H) 'in' ( Var2 H)) by ZF_LANG: 37;

            then ((M ! f) . ( Var1 H)) in ((M ! f) . ( Var2 H)) by A195, ZF_MODEL: 13;

            hence thesis by A196, A198, ZF_MODEL: 13;

          end;

          now

            assume H is being_equality;

            then

             A199: H = (( Var1 H) '=' ( Var2 H)) by ZF_LANG: 36;

            then ((M ! f) . ( Var1 H)) = ((M ! f) . ( Var2 H)) by A195, ZF_MODEL: 12;

            hence thesis by A196, A199, ZF_MODEL: 12;

          end;

          hence thesis by A185, A197;

        end;

        assume

         A200: ((L . a),f) |= H;

        

         A201: (M ! f) = f by Th16, ZF_LANG1:def 1;

         A202:

        now

          assume H is being_membership;

          then

           A203: H = (( Var1 H) 'in' ( Var2 H)) by ZF_LANG: 37;

          then (f . ( Var1 H)) in (f . ( Var2 H)) by A200, ZF_MODEL: 13;

          hence thesis by A201, A203, ZF_MODEL: 13;

        end;

        now

          assume H is being_equality;

          then

           A204: H = (( Var1 H) '=' ( Var2 H)) by ZF_LANG: 36;

          then (f . ( Var1 H)) = (f . ( Var2 H)) by A200, ZF_MODEL: 12;

          hence thesis by A201, A204, ZF_MODEL: 12;

        end;

        hence thesis by A185, A202;

      end;

      

       A205: for H st H is negative & RT[( the_argument_of H)] holds RT[H]

      proof

        let H;

        assume H is negative;

        then

         A206: H = ( 'not' ( the_argument_of H)) by ZF_LANG:def 30;

        given phi such that

         A207: phi is increasing & phi is continuous and

         A208: for a st (phi . a) = a & {} <> a holds for f holds (M,(M ! f)) |= ( the_argument_of H) iff ((L . a),f) |= ( the_argument_of H);

        take phi;

        thus phi is increasing & phi is continuous by A207;

        let a such that

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

        let f;

        thus (M,(M ! f)) |= H implies ((L . a),f) |= H

        proof

          assume (M,(M ! f)) |= H;

          then not (M,(M ! f)) |= ( the_argument_of H) by A206, ZF_MODEL: 14;

          then not ((L . a),f) |= ( the_argument_of H) by A208, A209;

          hence thesis by A206, ZF_MODEL: 14;

        end;

        assume ((L . a),f) |= H;

        then not ((L . a),f) |= ( the_argument_of H) by A206, ZF_MODEL: 14;

        then not (M,(M ! f)) |= ( the_argument_of H) by A208, A209;

        hence thesis by A206, ZF_MODEL: 14;

      end;

      thus RT[H] from ZF_LANG:sch 1( A182, A205, A161, A6);

    end;

    begin

    reserve M for non countable Aleph;

    theorem :: ZF_REFLE:21

    M is strongly_inaccessible implies ( Rank M) is being_a_model_of_ZF

    proof

      assume M is strongly_inaccessible;

      then

       A1: ( Rank M) is Universe by CARD_LAR: 38;

       omega c= M;

      then omega c< M;

      then

       A2: omega in M by ORDINAL1: 11;

      M c= ( Rank M) by CLASSES1: 38;

      hence thesis by A1, A2, Th6;

    end;