classes2.miz



    begin

    reserve m for Cardinal,

A,B,C for Ordinal,

x,y,z,X,Y,Z,W for set,

f for Function;

    

     Lm1: ( Tarski-Class X) is Tarski

    proof

      ( Tarski-Class X) is_Tarski-Class_of X by CLASSES1:def 4;

      hence thesis;

    end;

    registration

      cluster Tarski -> subset-closed for set;

      coherence ;

    end

    registration

      let X be set;

      cluster ( Tarski-Class X) -> Tarski;

      coherence by Lm1;

    end

    theorem :: CLASSES2:1

    

     Th1: W is subset-closed & X in W implies not (X,W) are_equipotent & ( card X) in ( card W)

    proof

      assume

       A1: W is subset-closed;

      assume

       A2: X in W;

      ( bool X) c= W by A1, A2;

      then

       A3: ( card ( bool X)) c= ( card W) by CARD_1: 11;

      

       A4: ( card X) in ( card ( bool X)) by CARD_1: 14;

      then ( card X) in ( card W) by A3;

      then ( card X) <> ( card W);

      hence thesis by A4, A3, CARD_1: 5;

    end;

    theorem :: CLASSES2:2

    

     Th2: W is Tarski & x in W & y in W implies {x} in W & {x, y} in W

    proof

      defpred C[ object] means $1 = {} ;

      assume that

       A1: W is Tarski and

       A2: x in W and

       A3: y in W;

      

       A4: {x} c= ( bool x) by ZFMISC_1: 68;

      ( bool x) in W by A1, A2;

      hence {x} in W by A1, A4, CLASSES1:def 1;

      then

       A5: ( bool {x}) in W by A1;

      deffunc g( object) = x;

      deffunc f( object) = y;

      consider f such that

       A6: ( dom f) = { {} , {x}} & for z be object st z in { {} , {x}} holds ( C[z] implies (f . z) = f(z)) & ( not C[z] implies (f . z) = g(z)) from PARTFUN1:sch 1;

       {x, y} c= ( rng f)

      proof

        let z be object;

        

         A7: {} in { {} , {x}} by TARSKI:def 2;

        

         A8: {x} in { {} , {x}} by TARSKI:def 2;

        assume z in {x, y};

        then z = x or z = y by TARSKI:def 2;

        then (f . {} ) = z or (f . {x}) = z by A6, A7, A8;

        hence thesis by A6, A7, A8, FUNCT_1:def 3;

      end;

      then

       A9: ( card {x, y}) c= ( card { {} , {x}}) by A6, CARD_1: 12;

      

       A10: {x, y} c= W by A2, A3, TARSKI:def 2;

      ( bool {x}) = { {} , {x}} by ZFMISC_1: 24;

      then ( card { {} , {x}}) in ( card W) by A1, A5, Th1;

      then ( card {x, y}) in ( card W) by A9, ORDINAL1: 12;

      hence thesis by A1, A10, CLASSES1: 1;

    end;

    theorem :: CLASSES2:3

    

     Th3: W is Tarski & x in W & y in W implies [x, y] in W

    proof

      assume

       A1: W is Tarski;

      assume that

       A2: x in W and

       A3: y in W;

      

       A4: {x} in W by A1, A2, Th2;

       {x, y} in W by A1, A2, A3, Th2;

      hence thesis by A1, A4, Th2;

    end;

    theorem :: CLASSES2:4

    

     Th4: W is Tarski & X in W implies ( Tarski-Class X) c= W

    proof

      assume that

       A1: W is Tarski and

       A2: X in W;

      reconsider D = W as non empty set by A2;

      D is_Tarski-Class_of X by A1, A2;

      hence thesis by CLASSES1:def 4;

    end;

    theorem :: CLASSES2:5

    

     Th5: W is Tarski & A in W implies ( succ A) in W & A c= W

    proof

      assume that

       A1: for X, Y st X in W & Y c= X holds Y in W and

       A2: for X st X in W holds ( bool X) in W and for X st X c= W holds (X,W) are_equipotent or X in W and

       A3: A in W;

      ( bool A) in W by A2, A3;

      hence ( succ A) in W by A1, ORDINAL2: 3;

      let x be object;

      assume

       A4: x in A;

      then

      reconsider B = x as Ordinal;

      B c= A by A4, ORDINAL1:def 2;

      hence thesis by A1, A3;

    end;

    theorem :: CLASSES2:6

    A in ( Tarski-Class W) implies ( succ A) in ( Tarski-Class W) & A c= ( Tarski-Class W) by Th5;

    theorem :: CLASSES2:7

    

     Th7: W is subset-closed & X is epsilon-transitive & X in W implies X c= W;

    theorem :: CLASSES2:8

    X is epsilon-transitive & X in ( Tarski-Class W) implies X c= ( Tarski-Class W) by Th7;

    theorem :: CLASSES2:9

    

     Th9: W is Tarski implies ( On W) = ( card W)

    proof

      assume

       A1: W is Tarski;

      now

        let X;

        assume

         A2: X in ( On W);

        hence X is Ordinal by ORDINAL1:def 9;

        reconsider A = X as Ordinal by A2, ORDINAL1:def 9;

        

         A3: X in W by A2, ORDINAL1:def 9;

        thus X c= ( On W)

        proof

          let x be object;

          assume

           A4: x in X;

          then x in A;

          then

          reconsider B = x as Ordinal;

          B c= A by A4, ORDINAL1:def 2;

          then B in W by A1, A3, CLASSES1:def 1;

          hence thesis by ORDINAL1:def 9;

        end;

      end;

      then

      reconsider ON = ( On W) as epsilon-transitive epsilon-connected set by ORDINAL1: 19;

       A5:

      now

        assume ON in W;

        then ON in ON by ORDINAL1:def 9;

        hence contradiction;

      end;

      ON c= W by ORDINAL2: 7;

      then

       A6: (ON,W) are_equipotent or ON in W by A1;

      now

        let A;

        assume that

         A7: (A,ON) are_equipotent and

         A8: not ON c= A;

        A in ON by A8, ORDINAL1: 16;

        then A in W by ORDINAL1:def 9;

        hence contradiction by A1, A6, A5, A7, Th1, WELLORD2: 15;

      end;

      then

      reconsider ON as Cardinal by CARD_1:def 1;

      ON = ( card ON);

      hence thesis by A6, A5, CARD_1: 5;

    end;

    theorem :: CLASSES2:10

    ( On ( Tarski-Class W)) = ( card ( Tarski-Class W)) by Th9;

    theorem :: CLASSES2:11

    

     Th11: W is Tarski & X in W implies ( card X) in W

    proof

      assume that

       A1: W is Tarski and

       A2: X in W;

      

       A3: ( card W) = ( On W) by A1, Th9;

      ( card X) in ( card W) by A1, A2, Th1;

      hence thesis by A3, ORDINAL1:def 9;

    end;

    theorem :: CLASSES2:12

    X in ( Tarski-Class W) implies ( card X) in ( Tarski-Class W) by Th11;

    theorem :: CLASSES2:13

    

     Th13: W is Tarski & x in ( card W) implies x in W

    proof

      assume

       A1: W is Tarski;

      assume x in ( card W);

      then x in ( On W) by A1, Th9;

      hence thesis by ORDINAL1:def 9;

    end;

    theorem :: CLASSES2:14

    x in ( card ( Tarski-Class W)) implies x in ( Tarski-Class W) by Th13;

    theorem :: CLASSES2:15

    W is Tarski & m in ( card W) implies m in W

    proof

      assume

       A1: W is Tarski;

      assume m in ( card W);

      then m in ( On W) by A1, Th9;

      hence thesis by ORDINAL1:def 9;

    end;

    theorem :: CLASSES2:16

    m in ( card ( Tarski-Class W)) implies m in ( Tarski-Class W)

    proof

      assume m in ( card ( Tarski-Class W));

      then m in ( On ( Tarski-Class W)) by Th9;

      hence thesis by ORDINAL1:def 9;

    end;

    theorem :: CLASSES2:17

    W is Tarski & m in W implies m c= W by Th5;

    theorem :: CLASSES2:18

    m in ( Tarski-Class W) implies m c= ( Tarski-Class W) by Th5;

    theorem :: CLASSES2:19

    

     Th19: W is Tarski implies ( card W) is limit_ordinal

    proof

      assume

       A1: W is Tarski;

      now

        let A;

        assume A in ( card W);

        then A in W by A1, Th13;

        then ( succ A) in W by A1, Th5;

        then ( succ A) in ( On W) by ORDINAL1:def 9;

        hence ( succ A) in ( card W) by A1, Th9;

      end;

      hence thesis by ORDINAL1: 28;

    end;

    theorem :: CLASSES2:20

    W is Tarski & W <> {} implies ( card W) <> 0 & ( card W) <> {} & ( card W) is limit_ordinal by Th19;

    theorem :: CLASSES2:21

    

     Th21: ( card ( Tarski-Class W)) <> 0 & ( card ( Tarski-Class W)) <> {} & ( card ( Tarski-Class W)) is limit_ordinal

    proof

      thus ( card ( Tarski-Class W)) <> 0 ;

      thus ( card ( Tarski-Class W)) <> {} ;

      now

        let A;

        assume A in ( card ( Tarski-Class W));

        then A in ( Tarski-Class W) by Th13;

        then ( succ A) in ( Tarski-Class W) by Th5;

        then ( succ A) in ( On ( Tarski-Class W)) by ORDINAL1:def 9;

        hence ( succ A) in ( card ( Tarski-Class W)) by Th9;

      end;

      hence thesis by ORDINAL1: 28;

    end;

    reserve f,g for Function,

L for Sequence,

F for Cardinal-Function;

    theorem :: CLASSES2:22

    

     Th22: W is Tarski & (X in W & W is epsilon-transitive or X in W & X c= W or ( card X) in ( card W) & X c= W) implies ( Funcs (X,W)) c= W

    proof

      assume

       A1: W is Tarski;

      assume that

       A2: X in W & W is epsilon-transitive or X in W & X c= W or ( card X) in ( card W) & X c= W;

      

       A3: ( card X) in ( card W) by A1, A2, Th1;

      let x be object;

      assume

       A4: x in ( Funcs (X,W));

      then

      consider f such that

       A5: x = f and

       A6: ( dom f) = X and

       A7: ( rng f) c= W by FUNCT_2:def 2;

      

       A8: X c= W by A2;

      

       A9: f c= W

      proof

        let y be object;

        assume

         A10: y in f;

        then

        consider y1,y2 be object such that

         A11: [y1, y2] = y by RELAT_1:def 1;

        

         A12: y1 in ( dom f) by A10, A11, FUNCT_1: 1;

        y2 = (f . y1) by A10, A11, FUNCT_1: 1;

        then y2 in ( rng f) by A12, FUNCT_1:def 3;

        hence thesis by A1, A8, A6, A7, A11, A12, Th3;

      end;

      ( card f) = ( card X) by A4, A5, CARD_2: 3;

      hence thesis by A1, A3, A5, A9, CLASSES1: 1;

    end;

    theorem :: CLASSES2:23

    X in ( Tarski-Class W) & W is epsilon-transitive or X in ( Tarski-Class W) & X c= ( Tarski-Class W) or ( card X) in ( card ( Tarski-Class W)) & X c= ( Tarski-Class W) implies ( Funcs (X,( Tarski-Class W))) c= ( Tarski-Class W)

    proof

      assume that

       A1: X in ( Tarski-Class W) & W is epsilon-transitive or X in ( Tarski-Class W) & X c= ( Tarski-Class W) or ( card X) in ( card ( Tarski-Class W)) & X c= ( Tarski-Class W);

      

       A2: ( card X) in ( card ( Tarski-Class W)) by A1, CLASSES1: 24;

      let x be object;

      assume

       A3: x in ( Funcs (X,( Tarski-Class W)));

      then

      consider f such that

       A4: x = f and

       A5: ( dom f) = X and

       A6: ( rng f) c= ( Tarski-Class W) by FUNCT_2:def 2;

      W is epsilon-transitive implies ( Tarski-Class W) is epsilon-transitive by CLASSES1: 23;

      then

       A7: X c= ( Tarski-Class W) by A1;

      

       A8: f c= ( Tarski-Class W)

      proof

        let y be object;

        assume

         A9: y in f;

        then

        consider y1,y2 be object such that

         A10: [y1, y2] = y by RELAT_1:def 1;

        

         A11: y1 in ( dom f) by A9, A10, FUNCT_1: 1;

        y2 = (f . y1) by A9, A10, FUNCT_1: 1;

        then y2 in ( rng f) by A11, FUNCT_1:def 3;

        hence thesis by A7, A5, A6, A10, A11, CLASSES1: 27;

      end;

      ( card f) = ( card X) by A3, A4, CARD_2: 3;

      hence thesis by A2, A4, A8, CLASSES1: 6;

    end;

    theorem :: CLASSES2:24

    

     Th24: ( dom L) is limit_ordinal & (for A st A in ( dom L) holds (L . A) = ( Rank A)) implies ( Rank ( dom L)) = ( Union L)

    proof

      assume that

       A1: ( dom L) is limit_ordinal and

       A2: for A st A in ( dom L) holds (L . A) = ( Rank A);

      

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

      now

        assume

         A4: ( dom L) <> {} ;

        thus ( Rank ( dom L)) c= ( Union L)

        proof

          let x be object;

          assume x in ( Rank ( dom L));

          then

          consider A such that

           A5: A in ( dom L) and

           A6: x in ( Rank A) by A1, A4, CLASSES1: 31;

          (L . A) = ( Rank A) by A2, A5;

          then ( Rank A) in ( rng L) by A5, FUNCT_1:def 3;

          hence thesis by A3, A6, TARSKI:def 4;

        end;

        thus ( Union L) c= ( Rank ( dom L))

        proof

          let x be object;

          assume x in ( Union L);

          then

          consider X such that

           A7: x in X and

           A8: X in ( rng L) by A3, TARSKI:def 4;

          consider y be object such that

           A9: y in ( dom L) and

           A10: X = (L . y) by A8, FUNCT_1:def 3;

          reconsider y as Ordinal by A9;

          X = ( Rank y) by A2, A9, A10;

          hence thesis by A1, A7, A9, CLASSES1: 31;

        end;

      end;

      hence thesis by A3, CLASSES1: 29, RELAT_1: 42, ZFMISC_1: 2;

    end;

    defpred PQ[ Ordinal] means W is Tarski & $1 in ( On W) implies ( card ( Rank $1)) in ( card W) & ( Rank $1) in W;

    

     Lm2: PQ[ 0 ] by Th9, CLASSES1: 29, ORDINAL1:def 9;

    

     Lm3: PQ[A] implies PQ[( succ A)]

    proof

      assume

       A1: PQ[A];

      

       A2: A in ( succ A) by ORDINAL1: 6;

      let W;

      assume that

       A3: W is Tarski and

       A4: ( succ A) in ( On W);

      ( card W) = ( On W) by A3, Th9;

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

      then ( Rank A) in W by A1, A3;

      then

       A5: ( bool ( Rank A)) in W by A3;

      ( Rank ( succ A)) = ( bool ( Rank A)) by CLASSES1: 30;

      hence thesis by A3, A5, Th1;

    end;

    

     Lm4: A <> 0 & A is limit_ordinal & (for B st B in A holds PQ[B]) implies PQ[A]

    proof

      deffunc f( Ordinal) = ( Rank $1);

      assume that

       A1: A <> 0 and

       A2: A is limit_ordinal and

       A3: for B st B in A holds PQ[B];

      let W;

      assume that

       A4: W is Tarski and

       A5: A in ( On W);

      consider L such that

       A6: ( dom L) = A & for B st B in A holds (L . B) = f(B) from ORDINAL2:sch 2;

      deffunc g( object) = ( card ( bool (L . $1)));

      consider F such that

       A7: ( dom F) = A & for x be set st x in A holds (F . x) = g(x) from CARD_3:sch 1;

      

       A8: ( product F) c= ( Funcs (A,W))

      proof

        let x be object;

        assume x in ( product F);

        then

        consider f such that

         A9: x = f and

         A10: ( dom f) = ( dom F) and

         A11: for x be object st x in ( dom F) holds (f . x) in (F . x) by CARD_3:def 5;

        ( rng f) c= W

        proof

          

           A12: A in W by A5, ORDINAL1:def 9;

          let z be object;

          assume z in ( rng f);

          then

          consider y be object such that

           A13: y in ( dom f) and

           A14: z = (f . y) by FUNCT_1:def 3;

          reconsider y as Ordinal by A7, A10, A13;

          

           A15: (f . y) in (F . y) by A10, A11, A13;

          y c= A by A7, A10, A13, ORDINAL1:def 2;

          then y in W by A4, A12, CLASSES1:def 1;

          then

           A16: y in ( On W) by ORDINAL1:def 9;

          (L . y) = ( Rank y) by A6, A7, A10, A13;

          then (L . y) in W by A3, A4, A7, A10, A13, A16;

          then ( bool (L . y)) in W by A4;

          then

           A17: ( card ( bool (L . y))) in W by A4, Th11;

          (F . y) = ( card ( bool (L . y))) by A7, A10, A13;

          then (F . y) c= W by A4, A17, Th5;

          hence thesis by A14, A15;

        end;

        hence thesis by A7, A9, A10, FUNCT_2:def 2;

      end;

      

       A18: ( Product F) = ( card ( product F)) by CARD_3:def 8;

      

       A19: A in W by A5, ORDINAL1:def 9;

      then A c= W by A4, Th5;

      then ( Funcs (A,W)) c= W by A4, A19, Th22;

      then ( product F) c= W by A8;

      then

       A20: ( Product F) c= ( card W) by A18, CARD_1: 11;

      

       A21: for x be object st x in ( dom ( Card L)) holds (( Card L) . x) in (F . x)

      proof

        let x be object;

        

         A22: ( card (L . x)) in ( card ( bool (L . x))) by CARD_1: 14;

        assume x in ( dom ( Card L));

        then

         A23: x in ( dom L) by CARD_3:def 2;

        then (F . x) = ( card ( bool (L . x))) by A6, A7;

        hence thesis by A23, A22, CARD_3:def 2;

      end;

      ( dom ( Card L)) = ( dom L) by CARD_3:def 2;

      then

       A24: ( Sum ( Card L)) in ( Product F) by A6, A7, A21, CARD_3: 41;

      

       A25: ( Rank A) c= W

      proof

        let x be object;

        assume x in ( Rank A);

        then

        consider B such that

         A26: B in A and

         A27: x in ( Rank B) by A1, A2, CLASSES1: 31;

        B c= A by A26, ORDINAL1:def 2;

        then B in W by A4, A19, CLASSES1:def 1;

        then B in ( On W) by ORDINAL1:def 9;

        then ( Rank B) c= W by A3, A4, A26, Th7;

        hence thesis by A27;

      end;

      

       A28: ( Rank A) = ( Union L) by A2, A6, Th24;

      hence ( card ( Rank A)) in ( card W) by A24, A20, CARD_3: 39, ORDINAL1: 12;

      ( card ( Rank A)) in ( Product F) by A28, A24, CARD_3: 39, ORDINAL1: 12;

      hence thesis by A4, A20, A25, CLASSES1: 1;

    end;

    theorem :: CLASSES2:25

    

     Th25: W is Tarski & A in ( On W) implies ( card ( Rank A)) in ( card W) & ( Rank A) in W

    proof

       PQ[B] from ORDINAL2:sch 1( Lm2, Lm3, Lm4);

      hence thesis;

    end;

    theorem :: CLASSES2:26

    A in ( On ( Tarski-Class W)) implies ( card ( Rank A)) in ( card ( Tarski-Class W)) & ( Rank A) in ( Tarski-Class W) by Th25;

    theorem :: CLASSES2:27

    

     Th27: W is Tarski implies ( Rank ( card W)) c= W

    proof

      assume

       A1: W is Tarski;

      now

        assume

         A2: W <> {} ;

        thus thesis

        proof

          

           A3: ( card W) is limit_ordinal by A1, Th19;

          let x be object;

          assume x in ( Rank ( card W));

          then

          consider A such that

           A4: A in ( card W) and

           A5: x in ( Rank A) by A2, A3, CLASSES1: 31;

          A in ( On W) by A1, A4, Th9;

          then ( Rank A) c= W by A1, Th7, Th25;

          hence thesis by A5;

        end;

      end;

      hence thesis by CLASSES1: 29;

    end;

    theorem :: CLASSES2:28

    

     Th28: ( Rank ( card ( Tarski-Class W))) c= ( Tarski-Class W)

    proof

      

       A1: ( card ( Tarski-Class W)) is limit_ordinal by Th21;

      let x be object;

      assume x in ( Rank ( card ( Tarski-Class W)));

      then

      consider A such that

       A2: A in ( card ( Tarski-Class W)) and

       A3: x in ( Rank A) by A1, CLASSES1: 31;

      A in ( On ( Tarski-Class W)) by A2, Th9;

      then ( Rank A) c= ( Tarski-Class W) by Th7, Th25;

      hence thesis by A3;

    end;

    deffunc f( object) = ( the_rank_of $1);

    deffunc g( set) = ( card ( bool $1));

    theorem :: CLASSES2:29

    

     Th29: W is Tarski & W is epsilon-transitive & X in W implies ( the_rank_of X) in W

    proof

      assume that

       A1: W is Tarski and

       A2: W is epsilon-transitive;

      

       A3: ( On W) = ( card W) by A1, Th9;

      defpred P[ Ordinal] means ex X st $1 = ( the_rank_of X) & X in W & not $1 in W;

      assume that

       A4: X in W and

       A5: not ( the_rank_of X) in W;

      

       A6: ex A st P[A] by A4, A5;

      consider A such that

       A7: P[A] and

       A8: for B st P[B] holds A c= B from ORDINAL1:sch 1( A6);

      consider X such that

       A9: A = ( the_rank_of X) and

       A10: X in W and

       A11: not A in W by A7;

      defpred P[ object] means ex Y st Y in X & $1 = ( the_rank_of Y);

      consider LL be set such that

       A12: for x be object holds x in LL iff x in ( On W) & P[x] from XBOOLE_0:sch 1;

      consider ff be Cardinal-Function such that

       A13: ( dom ff) = LL & for x st x in LL holds (ff . x) = g(x) from CARD_3:sch 1;

      

       A14: LL c= ( On W) by A12;

      

       A15: ( product ff) c= ( Funcs (LL,W))

      proof

        let x be object;

        assume x in ( product ff);

        then

        consider g such that

         A16: x = g and

         A17: ( dom g) = ( dom ff) and

         A18: for x be object st x in ( dom ff) holds (g . x) in (ff . x) by CARD_3:def 5;

        ( rng g) c= W

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A19: x in ( dom g) and

           A20: y = (g . x) by FUNCT_1:def 3;

          reconsider x as set by TARSKI: 1;

          

           A21: (ff . x) = ( card ( bool x)) by A13, A17, A19;

          x in W by A14, A13, A17, A19, ORDINAL1:def 9;

          then ( bool x) in W by A1;

          then ( card ( bool x)) in W by A1, Th11;

          then

           A22: ( card ( bool x)) c= W by A1, Th5;

          y in (ff . x) by A17, A18, A19, A20;

          hence thesis by A21, A22;

        end;

        hence thesis by A13, A16, A17, FUNCT_2:def 2;

      end;

      now

        let Z;

        assume Z in ( union LL);

        then

        consider Y such that

         A23: Z in Y and

         A24: Y in LL by TARSKI:def 4;

        Y in ( On W) by A12, A24;

        then

        reconsider Y as Ordinal by ORDINAL1:def 9;

        

         A25: Y c= ( union LL) by A24, ZFMISC_1: 74;

        

         A26: Z in Y by A23;

        hence Z is Ordinal;

        reconsider A = Z as Ordinal by A26;

        A c= Y by A23, ORDINAL1:def 2;

        hence Z c= ( union LL) by A25;

      end;

      then

      reconsider ULL = ( union LL) as epsilon-transitive epsilon-connected set by ORDINAL1: 19;

      

       A27: ( dom ( Card ( id LL))) = ( dom ( id LL)) by CARD_3:def 2;

      

       A28: ( dom ( id LL)) = LL by RELAT_1: 45;

      now

        let x be object;

        assume

         A29: x in ( dom ( Card ( id LL)));

        then

         A30: (( Card ( id LL)) . x) = ( card (( id LL) . x)) by A27, CARD_3:def 2;

        

         A31: (( id LL) . x) = x by A28, A27, A29, FUNCT_1: 18;

        reconsider xx = x as set by TARSKI: 1;

        (ff . x) = ( card ( bool xx)) by A13, A28, A27, A29;

        hence (( Card ( id LL)) . x) in (ff . x) by A31, A30, CARD_1: 14;

      end;

      then

       A32: ( Sum ( Card ( id LL))) in ( Product ff) by A13, A28, A27, CARD_3: 41;

      ( Union ( id LL)) = ( union ( rng ( id LL))) by CARD_3:def 4

      .= ULL by RELAT_1: 45;

      then

       A33: ( card ULL) in ( Product ff) by A32, CARD_3: 39, ORDINAL1: 12;

      consider f such that

       A34: ( dom f) = X & for x be object st x in X holds (f . x) = f(x) from FUNCT_1:sch 3;

      LL c= ( rng f)

      proof

        let x be object;

        assume x in LL;

        then

        consider Y such that

         A35: Y in X and

         A36: x = ( the_rank_of Y) by A12;

        (f . Y) = x by A34, A35, A36;

        hence thesis by A34, A35, FUNCT_1:def 3;

      end;

      then

       A37: ( card LL) c= ( card X) by A34, CARD_1: 12;

      ( card X) in ( card W) by A1, A10, Th1;

      then ( card LL) <> ( card W) by A37, ORDINAL1: 12;

      then

       A38: not (LL,W) are_equipotent by CARD_1: 5;

      

       A39: ( card ( product ff)) = ( Product ff) by CARD_3:def 8;

      

       A40: X c= W by A2, A10;

      X c= ( Rank ( card W))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A41: x in X;

        then not A c= ( the_rank_of xx) by A9, CLASSES1: 68, ORDINAL1: 5;

        then ( the_rank_of xx) in W by A8, A40, A41;

        then ( the_rank_of xx) in ( card W) by A3, ORDINAL1:def 9;

        then

         A42: ( Rank ( the_rank_of xx)) in ( Rank ( card W)) by CLASSES1: 36;

        xx c= ( Rank ( the_rank_of xx)) by CLASSES1:def 9;

        hence thesis by A42, CLASSES1: 41;

      end;

      then

       A43: A c= ( On W) by A9, A3, CLASSES1: 65;

      ( On W) c= ULL

      proof

        let x be object;

        assume

         A44: x in ( On W);

        then

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

        now

          assume

           A45: for Y st Y in X holds ( the_rank_of Y) c= B;

          X c= ( Rank ( succ B))

          proof

            let y be object;

            reconsider yy = y as set by TARSKI: 1;

            assume y in X;

            then ( the_rank_of yy) c= B by A45;

            then ( the_rank_of yy) in ( succ B) by ORDINAL1: 22;

            hence thesis by CLASSES1: 66;

          end;

          then

           A46: A c= ( succ B) by A9, CLASSES1: 65;

          B in W by A44, ORDINAL1:def 9;

          then ( succ B) in W by A1, Th5;

          hence contradiction by A1, A11, A46, CLASSES1:def 1;

        end;

        then

        consider Y such that

         A47: Y in X and

         A48: not ( the_rank_of Y) c= B;

        ( the_rank_of Y) in A by A9, A47, CLASSES1: 68;

        then ( the_rank_of Y) in LL by A43, A12, A47;

        then

         A49: ( the_rank_of Y) c= ULL by ZFMISC_1: 74;

        B in ( the_rank_of Y) by A48, ORDINAL1: 16;

        hence thesis by A49;

      end;

      then

       A50: ( card ( On W)) c= ( card ULL) by CARD_1: 11;

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

      then LL c= W by A14;

      then LL in W by A1, A38;

      then ( Funcs (LL,W)) c= W by A1, A2, Th22;

      then ( product ff) c= W by A15;

      then

       A51: ( Product ff) c= ( card W) by A39, CARD_1: 11;

      ( On W) = ( card W) by A1, Th9;

      hence contradiction by A33, A51, A50, CARD_1: 4;

    end;

    theorem :: CLASSES2:30

    

     Th30: W is Tarski & W is epsilon-transitive implies W c= ( Rank ( card W))

    proof

      assume that

       A1: W is Tarski and

       A2: W is epsilon-transitive;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in W;

      then ( the_rank_of xx) in W by A1, A2, Th29;

      then

       A3: ( the_rank_of xx) in ( On W) by ORDINAL1:def 9;

      ( On W) = ( card W) by A1, Th9;

      then

       A4: ( Rank ( the_rank_of xx)) in ( Rank ( card W)) by A3, CLASSES1: 36;

      xx c= ( Rank ( the_rank_of xx)) by CLASSES1:def 9;

      hence thesis by A4, CLASSES1: 41;

    end;

    theorem :: CLASSES2:31

    

     Th31: W is Tarski & W is epsilon-transitive implies ( Rank ( card W)) = W by Th27, Th30;

    theorem :: CLASSES2:32

    W is Tarski & A in ( On W) implies ( card ( Rank A)) c= ( card W)

    proof

      assume that

       A1: W is Tarski and

       A2: A in ( On W);

      ( card ( Rank A)) in ( card W) by A1, A2, Th25;

      hence thesis by CARD_1: 3;

    end;

    theorem :: CLASSES2:33

    A in ( On ( Tarski-Class W)) implies ( card ( Rank A)) c= ( card ( Tarski-Class W))

    proof

      assume A in ( On ( Tarski-Class W));

      then ( card ( Rank A)) in ( card ( Tarski-Class W)) by Th25;

      hence thesis by CARD_1: 3;

    end;

    theorem :: CLASSES2:34

    

     Th34: W is Tarski implies ( card W) = ( card ( Rank ( card W)))

    proof

      assume W is Tarski;

      then

       A1: ( card ( Rank ( card W))) c= ( card W) by Th27, CARD_1: 11;

      ( card ( card W)) c= ( card ( Rank ( card W))) by CARD_1: 11, CLASSES1: 38;

      hence thesis by A1;

    end;

    theorem :: CLASSES2:35

    ( card ( Tarski-Class W)) = ( card ( Rank ( card ( Tarski-Class W)))) by Th34;

    theorem :: CLASSES2:36

    

     Th36: W is Tarski & X c= ( Rank ( card W)) implies (X,( Rank ( card W))) are_equipotent or X in ( Rank ( card W))

    proof

      assume that

       A1: W is Tarski and

       A2: X c= ( Rank ( card W)) and

       A3: not (X,( Rank ( card W))) are_equipotent ;

      defpred P[ object] means ex Y st Y in X & $1 = ( the_rank_of Y);

      consider LL be set such that

       A4: for x be object holds x in LL iff x in ( On W) & P[x] from XBOOLE_0:sch 1;

      consider ff be Cardinal-Function such that

       A5: ( dom ff) = LL & for x st x in LL holds (ff . x) = g(x) from CARD_3:sch 1;

      

       A6: LL c= ( On W) by A4;

      

       A7: ( product ff) c= ( Funcs (LL,W))

      proof

        let x be object;

        assume x in ( product ff);

        then

        consider g such that

         A8: x = g and

         A9: ( dom g) = ( dom ff) and

         A10: for x be object st x in ( dom ff) holds (g . x) in (ff . x) by CARD_3:def 5;

        ( rng g) c= W

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A11: x in ( dom g) and

           A12: y = (g . x) by FUNCT_1:def 3;

          reconsider x as set by TARSKI: 1;

          

           A13: (ff . x) = ( card ( bool x)) by A5, A9, A11;

          x in W by A6, A5, A9, A11, ORDINAL1:def 9;

          then ( bool x) in W by A1;

          then ( card ( bool x)) in W by A1, Th11;

          then

           A14: ( card ( bool x)) c= W by A1, Th5;

          y in (ff . x) by A9, A10, A11, A12;

          hence thesis by A13, A14;

        end;

        hence thesis by A5, A8, A9, FUNCT_2:def 2;

      end;

      

       A15: ( card W) = ( card ( Rank ( card W))) by A1, Th34;

      then

       A16: ( card X) <> ( card W) by A3, CARD_1: 5;

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

      then

       A17: LL c= W by A6;

      now

        let Z;

        assume Z in ( union LL);

        then

        consider Y such that

         A18: Z in Y and

         A19: Y in LL by TARSKI:def 4;

        Y in ( On W) by A4, A19;

        then

        reconsider Y as Ordinal by ORDINAL1:def 9;

        

         A20: Y c= ( union LL) by A19, ZFMISC_1: 74;

        

         A21: Z in Y by A18;

        hence Z is Ordinal;

        reconsider A = Z as Ordinal by A21;

        A c= Y by A18, ORDINAL1:def 2;

        hence Z c= ( union LL) by A20;

      end;

      then

      reconsider ULL = ( union LL) as epsilon-transitive epsilon-connected set by ORDINAL1: 19;

      

       A22: ( dom ( Card ( id LL))) = ( dom ( id LL)) by CARD_3:def 2;

      

       A23: ( dom ( id LL)) = LL by RELAT_1: 45;

      now

        let x be object;

        assume

         A24: x in ( dom ( Card ( id LL)));

        then

         A25: (( Card ( id LL)) . x) = ( card (( id LL) . x)) by A22, CARD_3:def 2;

        

         A26: (( id LL) . x) = x by A23, A22, A24, FUNCT_1: 18;

        reconsider xx = x as set by TARSKI: 1;

        (ff . x) = ( card ( bool xx)) by A5, A23, A22, A24;

        hence (( Card ( id LL)) . x) in (ff . x) by A26, A25, CARD_1: 14;

      end;

      then

       A27: ( Sum ( Card ( id LL))) in ( Product ff) by A5, A23, A22, CARD_3: 41;

      consider f such that

       A28: ( dom f) = X & for x be object st x in X holds (f . x) = f(x) from FUNCT_1:sch 3;

      LL c= ( rng f)

      proof

        let x be object;

        assume x in LL;

        then

        consider Y such that

         A29: Y in X and

         A30: x = ( the_rank_of Y) by A4;

        (f . Y) = x by A28, A29, A30;

        hence thesis by A28, A29, FUNCT_1:def 3;

      end;

      then

       A31: ( card LL) c= ( card X) by A28, CARD_1: 12;

      

       A32: ( card ( product ff)) = ( Product ff) by CARD_3:def 8;

      ( card X) c= ( card W) by A2, A15, CARD_1: 11;

      then ( card X) in ( card W) by A16, CARD_1: 3;

      then ( card LL) <> ( card W) by A31, ORDINAL1: 12;

      then not (LL,W) are_equipotent by CARD_1: 5;

      then LL in W by A1, A17;

      then ( Funcs (LL,W)) c= W by A1, A17, Th22;

      then ( product ff) c= W by A7;

      then

       A33: ( Product ff) c= ( card W) by A32, CARD_1: 11;

      

       A34: ( card W) is limit_ordinal by A1, Th19;

      

       A35: ( card W) = ( On W) by A1, Th9;

      X c= ( Rank ( succ ULL))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        defpred P[ Ordinal] means $1 in ( card W) & xx c= ( Rank $1);

        assume

         A36: x in X;

        then

         A37: (f . x) = ( the_rank_of xx) by A28;

        consider A such that

         A38: A in ( card W) and

         A39: x in ( Rank A) by A2, A34, A36, CLASSES1: 29, CLASSES1: 31;

         P[A] by A38, A39, ORDINAL1:def 2;

        then

         A40: ex A st P[A];

        consider A such that

         A41: P[A] and

         A42: for B st P[B] holds A c= B from ORDINAL1:sch 1( A40);

        now

          let B;

          assume xx c= ( Rank B);

          then A c= ( card W) & ( card W) c= B or A c= B by A41, A42, ORDINAL1: 16;

          hence A c= B;

        end;

        then A = ( the_rank_of xx) by A41, CLASSES1:def 9;

        then (f . x) in LL by A4, A35, A36, A37, A41;

        then ( the_rank_of xx) c= ULL by A37, ZFMISC_1: 74;

        then

         A43: ( Rank ( the_rank_of xx)) c= ( Rank ULL) by CLASSES1: 37;

        xx c= ( Rank ( the_rank_of xx)) by CLASSES1:def 9;

        then xx c= ( Rank ULL) by A43;

        hence thesis by CLASSES1: 32;

      end;

      then

       A44: X in ( Rank ( succ ( succ ULL))) by CLASSES1: 32;

      ( Union ( id LL)) = ( union ( rng ( id LL))) by CARD_3:def 4

      .= ULL by RELAT_1: 45;

      then ( card ULL) in ( card W) by A27, A33, CARD_3: 39, ORDINAL1: 12;

      then

       A45: ULL <> ( On W) by A35;

      ( union ( card W)) = ( card W) by A34;

      then ULL c= ( On W) by A6, A35, ZFMISC_1: 77;

      then ULL c< ( On W) by A45;

      then ULL in ( card W) by A35, ORDINAL1: 11;

      then ( succ ULL) in ( card W) by A34, ORDINAL1: 28;

      then ( succ ( succ ULL)) in ( card W) by A34, ORDINAL1: 28;

      hence thesis by A34, A44, CLASSES1: 31;

    end;

    theorem :: CLASSES2:37

    X c= ( Rank ( card ( Tarski-Class W))) implies (X,( Rank ( card ( Tarski-Class W)))) are_equipotent or X in ( Rank ( card ( Tarski-Class W))) by Th36;

    theorem :: CLASSES2:38

    

     Th38: W is Tarski implies ( Rank ( card W)) is Tarski

    proof

      assume

       A1: W is Tarski;

      set B = ( Rank ( card W));

      thus for X, Y holds X in B & Y c= X implies Y in B by CLASSES1: 41;

      now

        

         A2: ( card W) is limit_ordinal by A1, Th19;

        assume

         A3: W <> {} ;

        thus for X holds X in B implies ( bool X) in B

        proof

          let X;

          assume X in B;

          then

          consider A such that

           A4: A in ( card W) and

           A5: X in ( Rank A) by A3, A2, CLASSES1: 31;

          

           A6: ( bool X) in ( Rank ( succ A)) by A5, CLASSES1: 42;

          ( succ A) in ( card W) by A2, A4, ORDINAL1: 28;

          hence thesis by A2, A6, CLASSES1: 31;

        end;

      end;

      hence thesis by A1, Th36, CLASSES1: 29;

    end;

    theorem :: CLASSES2:39

    ( Rank ( card ( Tarski-Class W))) is Tarski by Th38;

    theorem :: CLASSES2:40

    

     Th40: X is epsilon-transitive & A in ( the_rank_of X) implies ex Y st Y in X & ( the_rank_of Y) = A

    proof

      assume that

       A1: X is epsilon-transitive and

       A2: A in ( the_rank_of X);

      defpred P[ Ordinal] means ex Y st A in $1 & Y in X & ( the_rank_of Y) = $1;

      assume

       A3: not thesis;

      

       A4: ex B st P[B]

      proof

        assume

         A5: for B, Y st A in B & Y in X holds ( the_rank_of Y) <> B;

        X c= ( Rank A)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume

           A6: x in X;

          then

           A7: ( the_rank_of xx) <> A by A3;

          ( the_rank_of xx) c= A by A5, A6, ORDINAL1: 16;

          then ( the_rank_of xx) c< A by A7;

          then ( the_rank_of xx) in A by ORDINAL1: 11;

          hence thesis by CLASSES1: 66;

        end;

        then ( the_rank_of X) c= A by CLASSES1: 65;

        hence contradiction by A2, ORDINAL1: 5;

      end;

      consider B such that

       A8: P[B] and

       A9: for C st P[C] holds B c= C from ORDINAL1:sch 1( A4);

      consider Y such that

       A10: A in B and

       A11: Y in X and

       A12: ( the_rank_of Y) = B by A8;

      Y c= ( Rank A)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        

         A13: Y c= X by A1, A11;

        assume

         A14: x in Y;

        then ( the_rank_of xx) in B by A12, CLASSES1: 68;

        then not A in ( the_rank_of xx) by A9, A14, A13, ORDINAL1: 5;

        then

         A15: ( the_rank_of xx) c= A by ORDINAL1: 16;

        ( the_rank_of xx) <> A by A3, A14, A13;

        then ( the_rank_of xx) c< A by A15;

        then ( the_rank_of xx) in A by ORDINAL1: 11;

        hence thesis by CLASSES1: 66;

      end;

      then ( the_rank_of Y) c= A by CLASSES1: 65;

      hence contradiction by A10, A12, ORDINAL1: 5;

    end;

    theorem :: CLASSES2:41

    

     Th41: X is epsilon-transitive implies ( card ( the_rank_of X)) c= ( card X)

    proof

      consider f such that

       A1: ( dom f) = X & for x be object st x in X holds (f . x) = f(x) from FUNCT_1:sch 3;

      assume

       A2: X is epsilon-transitive;

      ( the_rank_of X) c= ( rng f)

      proof

        let x be object;

        assume

         A3: x in ( the_rank_of X);

        then

        reconsider x9 = x as Ordinal;

        consider Y such that

         A4: Y in X and

         A5: ( the_rank_of Y) = x9 by A2, A3, Th40;

        (f . Y) = x by A1, A4, A5;

        hence thesis by A1, A4, FUNCT_1:def 3;

      end;

      hence thesis by A1, CARD_1: 12;

    end;

    theorem :: CLASSES2:42

    

     Th42: W is Tarski & X is epsilon-transitive & X in W implies X in ( Rank ( card W))

    proof

      assume

       A1: W is Tarski;

      assume

       A2: X is epsilon-transitive;

      assume X in W;

      then ( card X) in ( card W) by A1, Th1;

      then

       A3: ( card ( the_rank_of X)) in ( card W) by A2, Th41, ORDINAL1: 12;

      ( card ( card W)) = ( card W);

      then ( the_rank_of X) in ( card W) by A3, CARD_3: 43;

      then

       A4: ( Rank ( the_rank_of X)) in ( Rank ( card W)) by CLASSES1: 36;

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

      hence thesis by A4, CLASSES1: 41;

    end;

    theorem :: CLASSES2:43

    X is epsilon-transitive & X in ( Tarski-Class W) implies X in ( Rank ( card ( Tarski-Class W))) by Th42;

    theorem :: CLASSES2:44

    

     Th44: W is epsilon-transitive implies ( Rank ( card ( Tarski-Class W))) is_Tarski-Class_of W by CLASSES1: 2, Th38, Th42;

    theorem :: CLASSES2:45

    W is epsilon-transitive implies ( Rank ( card ( Tarski-Class W))) = ( Tarski-Class W)

    proof

      assume W is epsilon-transitive;

      then ( Rank ( card ( Tarski-Class W))) is_Tarski-Class_of W by Th44;

      hence ( Rank ( card ( Tarski-Class W))) c= ( Tarski-Class W) & ( Tarski-Class W) c= ( Rank ( card ( Tarski-Class W))) by Th28, CLASSES1:def 4;

    end;

    definition

      let IT be set;

      :: CLASSES2:def1

      attr IT is universal means IT is epsilon-transitive & IT is Tarski;

    end

    registration

      cluster universal -> epsilon-transitive Tarski for set;

      coherence ;

      cluster epsilon-transitive Tarski -> universal for set;

      coherence ;

    end

    registration

      cluster universal non empty for set;

      existence

      proof

        set X = the set;

        take V = ( Tarski-Class ( the_transitive-closure_of X));

        thus V is epsilon-transitive by CLASSES1: 23;

        thus thesis;

      end;

    end

    definition

      mode Universe is universal non empty set;

    end

    reserve U1,U2,U for Universe;

    theorem :: CLASSES2:46

    

     Th46: ( On U) is Ordinal

    proof

      ( On U) = ( card U) by Th9;

      hence thesis;

    end;

    theorem :: CLASSES2:47

    

     Th47: X is epsilon-transitive implies ( Tarski-Class X) is universal by CLASSES1: 23;

    theorem :: CLASSES2:48

    ( Tarski-Class U) is Universe by Th47;

    registration

      let U;

      cluster ( On U) -> ordinal;

      coherence by Th46;

      cluster ( Tarski-Class U) -> universal;

      coherence by Th47;

    end

    theorem :: CLASSES2:49

    

     Th49: ( Tarski-Class A) is universal by CLASSES1: 23;

    registration

      let A;

      cluster ( Tarski-Class A) -> universal;

      coherence by Th49;

    end

    theorem :: CLASSES2:50

    

     Th50: U = ( Rank ( On U))

    proof

      ( card U) = ( On U) by Th9;

      hence thesis by Th31;

    end;

    theorem :: CLASSES2:51

    

     Th51: ( On U) <> {} & ( On U) is limit_ordinal

    proof

      ( card U) = ( On U) by Th9;

      hence thesis by Th19;

    end;

    theorem :: CLASSES2:52

    U1 in U2 or U1 = U2 or U2 in U1

    proof

      

       A1: ( On U1) in ( On U2) or ( On U1) = ( On U2) or ( On U2) in ( On U1) by ORDINAL1: 14;

      

       A2: U2 = ( Rank ( On U2)) by Th50;

      U1 = ( Rank ( On U1)) by Th50;

      hence thesis by A1, A2, CLASSES1: 36;

    end;

    theorem :: CLASSES2:53

    

     Th53: U1 c= U2 or U2 in U1

    proof

      

       A1: ( On U1) c= ( On U2) or ( On U2) in ( On U1) by ORDINAL1: 16;

      

       A2: U2 = ( Rank ( On U2)) by Th50;

      U1 = ( Rank ( On U1)) by Th50;

      hence thesis by A1, A2, CLASSES1: 36, CLASSES1: 37;

    end;

    theorem :: CLASSES2:54

    

     Th54: (U1,U2) are_c=-comparable

    proof

      

       A1: ( On U1) c= ( On U2) or ( On U2) c= ( On U1);

      

       A2: U2 = ( Rank ( On U2)) by Th50;

      U1 = ( Rank ( On U1)) by Th50;

      hence U1 c= U2 or U2 c= U1 by A1, A2, CLASSES1: 37;

    end;

    theorem :: CLASSES2:55

    (U1 \/ U2) is Universe & (U1 /\ U2) is Universe

    proof

      (U1,U2) are_c=-comparable by Th54;

      then U1 c= U2 or U2 c= U1;

      hence thesis by XBOOLE_1: 12, XBOOLE_1: 28;

    end;

    theorem :: CLASSES2:56

    

     Th56: {} in U

    proof

       {} c= the Element of U;

      hence thesis by CLASSES1:def 1;

    end;

    theorem :: CLASSES2:57

    x in U implies {x} in U by Th2;

    theorem :: CLASSES2:58

    x in U & y in U implies {x, y} in U & [x, y] in U by Th2, Th3;

    theorem :: CLASSES2:59

    

     Th59: X in U implies ( bool X) in U & ( union X) in U & ( meet X) in U

    proof

      assume

       A1: X in U;

      hence ( bool X) in U by CLASSES1:def 2;

      U = ( Rank ( On U)) by Th50;

      hence

       A2: ( union X) in U by A1, CLASSES1: 35;

      ( meet X) c= ( union X) by SETFAM_1: 2;

      hence thesis by A2, CLASSES1:def 1;

    end;

    theorem :: CLASSES2:60

    

     Th60: X in U & Y in U implies (X \/ Y) in U & (X /\ Y) in U & (X \ Y) in U & (X \+\ Y) in U

    proof

      assume that

       A1: X in U and

       A2: Y in U;

      

       A3: ( union {X, Y}) = (X \/ Y) by ZFMISC_1: 75;

      

       A4: ( meet {X, Y}) = (X /\ Y) by SETFAM_1: 11;

       {X, Y} in U by A1, A2, Th2;

      hence

       A5: (X \/ Y) in U & (X /\ Y) in U by A3, A4, Th59;

      (X \+\ Y) = ((X \/ Y) \ (X /\ Y)) by XBOOLE_1: 101;

      hence thesis by A1, A5, CLASSES1:def 1;

    end;

    theorem :: CLASSES2:61

    

     Th61: X in U & Y in U implies [:X, Y:] in U & ( Funcs (X,Y)) in U

    proof

      assume that

       A1: X in U and

       A2: Y in U;

      (X \/ Y) in U by A1, A2, Th60;

      then ( bool (X \/ Y)) in U by Th59;

      then

       A3: ( bool ( bool (X \/ Y))) in U by Th59;

       [:X, Y:] c= ( bool ( bool (X \/ Y))) by ZFMISC_1: 86;

      hence [:X, Y:] in U by A3, CLASSES1:def 1;

      then

       A4: ( bool [:X, Y:]) in U by Th59;

      ( Funcs (X,Y)) c= ( bool [:X, Y:]) by FRAENKEL: 2;

      hence thesis by A4, CLASSES1:def 1;

    end;

    reserve u,v for Element of U;

    registration

      let U1;

      cluster non empty for Element of U1;

      existence

      proof

         {} in U1 by Th56;

        then

        reconsider x = ( bool {} ) as Element of U1 by Th59;

        take x;

        thus thesis;

      end;

    end

    definition

      let U, u;

      :: original: {

      redefine

      func {u} -> Element of U ;

      coherence by Th2;

      :: original: bool

      redefine

      func bool u -> Element of U ;

      coherence by Th59;

      :: original: union

      redefine

      func union u -> Element of U ;

      coherence by Th59;

      :: original: meet

      redefine

      func meet u -> Element of U ;

      coherence by Th59;

      let v;

      :: original: {

      redefine

      func {u,v} -> Element of U ;

      coherence by Th2;

      :: original: [

      redefine

      func [u,v] -> Element of U ;

      coherence by Th3;

      :: original: \/

      redefine

      func u \/ v -> Element of U ;

      coherence by Th60;

      :: original: /\

      redefine

      func u /\ v -> Element of U ;

      coherence by Th60;

      :: original: \

      redefine

      func u \ v -> Element of U ;

      coherence by Th60;

      :: original: \+\

      redefine

      func u \+\ v -> Element of U ;

      coherence by Th60;

      :: original: [:

      redefine

      func [:u,v:] -> Element of U ;

      coherence by Th61;

      :: original: Funcs

      redefine

      func Funcs (u,v) -> Element of U ;

      coherence by Th61;

    end

    definition

      :: CLASSES2:def2

      func FinSETS -> Universe equals ( Tarski-Class {} );

      correctness ;

    end

    

     Lm5: omega is limit_ordinal by ORDINAL1:def 11;

    theorem :: CLASSES2:62

    

     Th62: ( card ( Rank omega )) = ( card omega )

    proof

      deffunc h( Ordinal) = ( Rank $1);

      consider L such that

       A1: ( dom L) = omega & for A st A in omega holds (L . A) = h(A) from ORDINAL2:sch 2;

      now

        let X, Y;

        assume X in ( rng L);

        then

        consider x be object such that

         A2: x in ( dom L) and

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

        assume Y in ( rng L);

        then

        consider y be object such that

         A4: y in ( dom L) and

         A5: Y = (L . y) by FUNCT_1:def 3;

        reconsider x, y as Ordinal by A2, A4;

        

         A6: Y = ( Rank y) by A1, A4, A5;

        

         A7: x c= y or y c= x;

        X = ( Rank x) by A1, A2, A3;

        then X c= Y or Y c= X by A6, A7, CLASSES1: 37;

        hence (X,Y) are_c=-comparable ;

      end;

      then

       A8: ( rng L) is c=-linear;

      

       A9: ( card omega ) c= ( card ( Rank omega )) by CARD_1: 11, CLASSES1: 38;

       A10:

      now

        let X;

        assume X in ( rng L);

        then

        consider x be object such that

         A11: x in ( dom L) and

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

        reconsider x as Ordinal by A11;

        X = ( Rank x) by A1, A11, A12;

        hence ( card X) in ( card omega ) by A1, A11, CARD_2: 67, CARD_3: 42;

      end;

      ( Rank omega ) = ( Union L) by A1, Lm5, Th24

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

      then ( card ( Rank omega )) c= ( card omega ) by A8, A10, CARD_3: 46;

      hence thesis by A9;

    end;

    theorem :: CLASSES2:63

    

     Th63: ( Rank omega ) is Tarski

    proof

      thus X in ( Rank omega ) & Y c= X implies Y in ( Rank omega ) by CLASSES1: 41;

      thus X in ( Rank omega ) implies ( bool X) in ( Rank omega )

      proof

        assume X in ( Rank omega );

        then

        consider A such that

         A1: A in omega and

         A2: X in ( Rank A) by Lm5, CLASSES1: 31;

        

         A3: ( bool X) in ( Rank ( succ A)) by A2, CLASSES1: 42;

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

        hence thesis by A3, Lm5, CLASSES1: 31;

      end;

      thus X c= ( Rank omega ) implies (X,( Rank omega )) are_equipotent or X in ( Rank omega )

      proof

        

         A4: 0 in omega ;

        defpred P[ object, object] means ( the_rank_of $2) c= ( the_rank_of $1);

        assume that

         A5: X c= ( Rank omega ) and

         A6: not (X,( Rank omega )) are_equipotent and

         A7: not X in ( Rank omega );

        

         A8: ( card X) <> ( card omega ) by A6, Th62, CARD_1: 5;

        ( card X) c= ( card omega ) by A5, Th62, CARD_1: 11;

        then ( card X) in omega by A8, CARD_1: 3;

        then

        reconsider X as finite set;

        

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

        

         A10: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z] by XBOOLE_1: 1;

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

        then

         A11: X <> {} by A7, A4;

        consider x be object such that

         A12: x in X & for y be object st y in X holds P[x, y] from CARD_2:sch 2( A11, A9, A10);

        set A = ( the_rank_of x);

        for Y st Y in X holds ( the_rank_of Y) in ( succ A) by A12, ORDINAL1: 22;

        then

         A13: ( the_rank_of X) c= ( succ A) by CLASSES1: 69;

        A in omega by A5, A12, CLASSES1: 66;

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

        then ( the_rank_of X) in omega by A13, ORDINAL1: 12;

        hence thesis by A7, CLASSES1: 66;

      end;

    end;

    theorem :: CLASSES2:64

     FinSETS = ( Rank omega )

    proof

      

       A1: omega c= ( Rank omega ) by CLASSES1: 38;

      then

      reconsider M = ( Rank omega ) as non empty set;

       0 in omega ;

      then M is_Tarski-Class_of {} by A1, Th63;

      hence FinSETS c= ( Rank omega ) by CLASSES1:def 4;

      

       A2: {} in ( On FinSETS ) by Th51, ORDINAL3: 8;

      

       A3: FinSETS = ( Rank ( On FinSETS )) by Th50;

      ( On FinSETS ) is limit_ordinal by Th51;

      then omega c= ( On FinSETS ) by A2, ORDINAL1:def 11;

      hence thesis by A3, CLASSES1: 37;

    end;

    definition

      :: CLASSES2:def3

      func SETS -> Universe equals ( Tarski-Class FinSETS );

      correctness ;

    end

    registration

      let X be set;

      cluster ( the_transitive-closure_of X) -> epsilon-transitive;

      coherence ;

    end

    registration

      let X be epsilon-transitive set;

      cluster ( Tarski-Class X) -> epsilon-transitive;

      coherence by CLASSES1: 23;

    end

    definition

      let X be set;

      :: CLASSES2:def4

      func Universe_closure X -> Universe means

      : Def4: X c= it & for Y be Universe st X c= Y holds it c= Y;

      uniqueness ;

      existence

      proof

        per cases ;

          suppose ( Rank ( the_rank_of X)) is Universe;

          then

          reconsider R = ( Rank ( the_rank_of X)) as Universe;

          take R;

          thus X c= R by CLASSES1:def 9;

          let Y be Universe;

          assume X c= Y;

          then ( the_rank_of X) c= ( the_rank_of Y) by CLASSES1: 67;

          then

           A1: R c= ( Rank ( the_rank_of Y)) by CLASSES1: 37;

          

           A2: ( Rank ( card Y)) = Y by Th31;

          then ( the_rank_of Y) c= ( card Y) by CLASSES1:def 9;

          then ( Rank ( the_rank_of Y)) c= Y by A2, CLASSES1: 37;

          hence thesis by A1;

        end;

          suppose

           A3: not ( Rank ( the_rank_of X)) is Universe;

          take R = ( Tarski-Class ( Rank ( the_rank_of X)));

          

           A4: ( Rank ( the_rank_of X)) in R by CLASSES1: 2;

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

          then X in R by A4, CLASSES1:def 1;

          hence X c= R by ORDINAL1:def 2;

          let Y be Universe;

          assume X c= Y;

          then

           A5: ( the_rank_of X) c= ( the_rank_of Y) by CLASSES1: 67;

          

           A6: ( Rank ( card Y)) = Y by Th31;

          then

           A7: ( the_rank_of Y) c= ( card Y) by CLASSES1:def 9;

          Y c= ( Rank ( the_rank_of Y)) by CLASSES1:def 9;

          then ( card Y) c= ( the_rank_of Y) by A6, CLASSES1: 37;

          then ( card Y) = ( the_rank_of Y) by A7;

          then ( the_rank_of X) c< ( card Y) by A3, A5, A6;

          then ( the_rank_of X) in ( card Y) by ORDINAL1: 11;

          then ( Rank ( the_rank_of X)) in Y by A6, CLASSES1: 36;

          then Y is_Tarski-Class_of ( Rank ( the_rank_of X));

          hence thesis by CLASSES1:def 4;

        end;

      end;

    end

    deffunc C( Ordinal, set) = ( Tarski-Class $2);

    deffunc D( Ordinal, Sequence) = ( Universe_closure ( Union $2));

    definition

      mode FinSet is Element of FinSETS ;

      mode Set is Element of SETS ;

      let A;

      :: CLASSES2:def5

      func UNIVERSE A -> set means

      : Def5: ex L st it = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = FinSETS & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = ( Tarski-Class (L . C))) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = ( Universe_closure ( Union (L | C)));

      correctness

      proof

        (ex x be object, L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = FinSETS & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)) & for x1,x2 be set st (ex L st x1 = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = FinSETS & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)) & (ex L st x2 = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = FinSETS & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

    end

    deffunc u( Ordinal) = ( UNIVERSE $1);

     Lm6:

    now

      

       A1: for A holds for x be object holds x = u(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = FinSETS & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|) by Def5;

      thus u(0) = FinSETS from ORDINAL2:sch 8( A1);

      thus for A holds u(succ) = C(A,u) from ORDINAL2:sch 9( A1);

      let A, L;

      assume that

       A2: A <> 0 & A is limit_ordinal and

       A3: ( dom L) = A and

       A4: for B st B in A holds (L . B) = u(B);

      thus u(A) = D(A,L) from ORDINAL2:sch 10( A1, A2, A3, A4);

    end;

    registration

      let A;

      cluster ( UNIVERSE A) -> universal non empty;

      coherence

      proof

        defpred P[ Ordinal] means ( UNIVERSE $1) is Universe;

        

         A1: P[B] implies P[( succ B)]

        proof

          assume P[B];

          then

          reconsider UU = ( UNIVERSE B) as Universe;

          ( UNIVERSE ( succ B)) = ( Tarski-Class UU) by Lm6;

          hence thesis;

        end;

        

         A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A]

        proof

          let A such that

           A3: A <> 0 and

           A4: A is limit_ordinal and for B st B in A holds P[B];

          consider L such that

           A5: ( dom L) = A & for B st B in A holds (L . B) = u(B) from ORDINAL2:sch 2;

          ( UNIVERSE A) = ( Universe_closure ( Union L)) by A3, A4, A5, Lm6

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

          hence thesis;

        end;

        

         A6: P[ 0 ] by Lm6;

        for A holds P[A] from ORDINAL2:sch 1( A6, A1, A2);

        hence thesis;

      end;

    end

    theorem :: CLASSES2:65

    ( UNIVERSE {} ) = FinSETS by Lm6;

    theorem :: CLASSES2:66

    ( UNIVERSE ( succ A)) = ( Tarski-Class ( UNIVERSE A)) by Lm6;

    

     Lm7: 1 = ( succ 0 );

    theorem :: CLASSES2:67

    ( UNIVERSE 1) = SETS by Lm6, Lm7;

    theorem :: CLASSES2:68

    A <> {} & A is limit_ordinal & ( dom L) = A & (for B st B in A holds (L . B) = ( UNIVERSE B)) implies ( UNIVERSE A) = ( Universe_closure ( Union L)) by Lm6;

    theorem :: CLASSES2:69

     FinSETS c= U & ( Tarski-Class {} ) c= U & ( UNIVERSE {} ) c= U

    proof

      

       A1: ( On U) c= ( Rank ( On U)) by CLASSES1: 38;

      

       A2: ( Rank ( On U)) = U by Th50;

       {} in ( On U) by Th51, ORDINAL3: 8;

      hence thesis by A2, A1, Lm6, Th4;

    end;

    theorem :: CLASSES2:70

    

     Th70: A in B iff ( UNIVERSE A) in ( UNIVERSE B)

    proof

      defpred P[ Ordinal] means for A st A in $1 holds ( UNIVERSE A) in ( UNIVERSE $1);

      

       A1: for B st P[B] holds P[( succ B)]

      proof

        let B such that

         A2: P[B];

        let A;

        assume

         A3: A in ( succ B);

        A c< B iff A c= B & A <> B;

        then A in B or A = B by A3, ORDINAL1: 11, ORDINAL1: 22;

        then

         A4: ( UNIVERSE A) in ( UNIVERSE B) or ( UNIVERSE A) = ( UNIVERSE B) by A2;

        ( UNIVERSE ( succ B)) = ( Tarski-Class ( UNIVERSE B)) by Lm6;

        then ( UNIVERSE B) in ( UNIVERSE ( succ B)) by CLASSES1: 2;

        hence thesis by A4, ORDINAL1: 10;

      end;

      

       A5: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A]

      proof

        let B;

        assume that

         A6: B <> 0 and

         A7: B is limit_ordinal and for C st C in B holds for A st A in C holds ( UNIVERSE A) in ( UNIVERSE C);

        let A;

        consider L such that

         A8: ( dom L) = B & for C st C in B holds (L . C) = u(C) from ORDINAL2:sch 2;

        assume A in B;

        then

         A9: ( succ A) in B by A7, ORDINAL1: 28;

        then (L . ( succ A)) = ( UNIVERSE ( succ A)) by A8;

        then ( UNIVERSE ( succ A)) in ( rng L) by A9, A8, FUNCT_1:def 3;

        then

         A10: ( UNIVERSE ( succ A)) c= ( union ( rng L)) by ZFMISC_1: 74;

        ( UNIVERSE B) = ( Universe_closure ( Union L)) by A6, A7, A8, Lm6

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

        then ( union ( rng L)) c= ( UNIVERSE B) by Def4;

        then

         A11: ( UNIVERSE ( succ A)) c= ( UNIVERSE B) by A10;

        

         A12: ( UNIVERSE A) in ( Tarski-Class ( UNIVERSE A)) by CLASSES1: 2;

        ( UNIVERSE ( succ A)) = ( Tarski-Class ( UNIVERSE A)) by Lm6;

        hence thesis by A12, A11;

      end;

      

       A13: P[ 0 ];

      

       A14: for B holds P[B] from ORDINAL2:sch 1( A13, A1, A5);

      hence A in B implies ( UNIVERSE A) in ( UNIVERSE B);

      assume that

       A15: ( UNIVERSE A) in ( UNIVERSE B) and

       A16: not A in B;

      B in A or B = A by A16, ORDINAL1: 16;

      hence contradiction by A14, A15;

    end;

    theorem :: CLASSES2:71

    ( UNIVERSE A) = ( UNIVERSE B) implies A = B

    proof

      assume that

       A1: ( UNIVERSE A) = ( UNIVERSE B) and

       A2: A <> B;

      A in B or B in A by A2, ORDINAL1: 14;

      then ( UNIVERSE A) in ( UNIVERSE B) or ( UNIVERSE B) in ( UNIVERSE A) by Th70;

      hence contradiction by A1;

    end;

    theorem :: CLASSES2:72

    A c= B iff ( UNIVERSE A) c= ( UNIVERSE B)

    proof

      thus A c= B implies ( UNIVERSE A) c= ( UNIVERSE B)

      proof

        assume

         A1: A c= B;

        assume not ( UNIVERSE A) c= ( UNIVERSE B);

        then ( UNIVERSE B) in ( UNIVERSE A) by Th53;

        then B in A by Th70;

        hence contradiction by A1, ORDINAL1: 5;

      end;

      assume

       A2: ( UNIVERSE A) c= ( UNIVERSE B);

      assume not A c= B;

      then B in A by ORDINAL1: 16;

      then ( UNIVERSE B) in ( UNIVERSE A) by Th70;

      hence contradiction by A2, ORDINAL1: 5;

    end;

    reserve u,v for Element of ( Tarski-Class X);

    theorem :: CLASSES2:73

    ( Tarski-Class (X, {} )) in ( Tarski-Class (X,1)) & ( Tarski-Class (X, {} )) <> ( Tarski-Class (X,1))

    proof

      deffunc F( Ordinal) = ( Tarski-Class (X,$1));

      deffunc C( Ordinal, set) = (({ u : ex v st v in $2 & u c= v } \/ { ( bool v) : v in $2 }) \/ (( bool $2) /\ ( Tarski-Class X)));

      deffunc D( Ordinal, Sequence) = (( union ( rng $2)) /\ ( Tarski-Class X));

      

       A1: for A holds for x be object holds x = F(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = {X} & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|) by CLASSES1:def 5;

      

       A2: F(0) = {X} from ORDINAL2:sch 8( A1);

      then X in ( Tarski-Class (X, {} )) by TARSKI:def 1;

      then

       A3: ( bool X) in ( Tarski-Class X) by CLASSES1: 4;

       {X} c= ( bool X)

      proof

        let x be object;

        assume x in {X};

        then x = X by TARSKI:def 1;

        hence thesis by ZFMISC_1:def 1;

      end;

      then 1 = ( succ 0 ) & {X} in ( Tarski-Class X) by A3, CLASSES1: 3;

      hence

       A4: ( Tarski-Class (X, {} )) in ( Tarski-Class (X,1)) by A2, CLASSES1: 10;

      assume ( Tarski-Class (X, {} )) = ( Tarski-Class (X,1));

      hence contradiction by A4;

    end;