classes3.miz



    begin

    reserve X,Y,Z for set,

x,y,z for object,

A,B,C for Ordinal;

    definition

      let X;

      :: CLASSES3:def1

      attr X is power-closed means

      : Def1: Y in X implies ( bool Y) in X;

    end

    definition

      let X;

      :: CLASSES3:def2

      attr X is union-closed means

      : Def2: Y in X implies ( union Y) in X;

    end

    definition

      let X;

      :: CLASSES3:def3

      attr X is FamUnion-closed means

      : Def3: for Y holds for f be Function st ( dom f) = Y & ( rng f) c= X & Y in X holds ( union ( rng f)) in X;

    end

    registration

      cluster Tarski -> power-closed subset-closed for set;

      coherence ;

    end

    registration

      cluster epsilon-transitive Tarski -> union-closed FamUnion-closed for set;

      coherence

      proof

        let X such that

         A1: X is epsilon-transitive Tarski;

        thus X is union-closed by A1, CLASSES2: 59;

        let Y;

        let f be Function such that

         A2: ( dom f) = Y & ( rng f) c= X & Y in X;

        reconsider X as Universe by A1, A2;

         not (Y,X) are_equipotent & ( card Y) in ( card X) by A2, CLASSES2: 1;

        then ( card ( rng f)) in ( card X) by A2, ORDINAL1: 12, CARD_1: 12;

        then

         A3: ( card ( rng f)) <> ( card X);

        (( rng f),X) are_equipotent or ( rng f) in X by A2, CLASSES1:def 2;

        hence thesis by A3, CARD_1: 5, CLASSES2: 59;

      end;

    end

    registration

      cluster epsilon-transitive FamUnion-closed -> union-closed for set;

      coherence

      proof

        let X be set such that

         A1: X is epsilon-transitive FamUnion-closed;

        let A be set such that

         A2: A in X;

        ( dom ( id A)) = A & ( rng ( id A)) = A c= X by A1, A2;

        hence thesis by A1, A2;

      end;

    end

    registration

      cluster epsilon-transitive power-closed -> subset-closed for set;

      coherence

      proof

        let X be set such that

         A1: X is epsilon-transitive power-closed;

        let A,B be set such that

         A2: A in X & B c= A;

        B in ( bool A) c= X by A1, A2;

        hence thesis;

      end;

    end

    definition

      mode Grothendieck is epsilon-transitive power-closed FamUnion-closed set;

    end

    begin

    definition

      let X be set;

      :: CLASSES3:def4

      mode Grothendieck of X -> Grothendieck means

      : Def4: X in it ;

      existence

      proof

        set R = ( the_transitive-closure_of {X});

        take T = ( Tarski-Class R);

        

         A1: ( union T) c= T by CLASSES1: 48;

        X in {X} & {X} c= R by CLASSES1: 52, TARSKI:def 1;

        then X in R & R in T by CLASSES1: 2;

        then X in ( union T) by TARSKI:def 4;

        hence thesis by A1;

      end;

    end

    registration

      let G1,G2 be Grothendieck;

      cluster (G1 /\ G2) -> epsilon-transitive power-closed FamUnion-closed;

      coherence

      proof

        thus (G1 /\ G2) is epsilon-transitive by CLASSES1: 50;

        hereby

          let X be set such that

           A1: X in (G1 /\ G2);

          

           A2: G1 is power-closed & G2 is power-closed;

          X in G1 & X in G2 by A1, XBOOLE_0:def 4;

          then ( bool X) in G1 & ( bool X) in G2 by A2;

          hence ( bool X) in (G1 /\ G2) by XBOOLE_0:def 4;

        end;

        let X;

        let f be Function such that

         A3: ( dom f) = X & ( rng f) c= (G1 /\ G2) & X in (G1 /\ G2);

        ( rng f) c= G1 & X in G1 by A3, XBOOLE_0:def 4;

        then

         A4: ( union ( rng f)) in G1 by A3, Def3;

        ( rng f) c= G2 & X in G2 by A3, XBOOLE_0:def 4;

        then ( union ( rng f)) in G2 by A3, Def3;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

    end

    theorem :: CLASSES3:1

    

     Th1: for G1,G2 be Grothendieck of X holds (G1 /\ G2) is Grothendieck of X

    proof

      let G1,G2 be Grothendieck of X;

      X in G1 & X in G2 by Def4;

      hence X in (G1 /\ G2) by XBOOLE_0:def 4;

    end;

    definition

      let X be set;

      :: CLASSES3:def5

      func GrothendieckUniverse X -> Grothendieck of X means

      : GDef: for G be Grothendieck of X holds it c= G;

      existence

      proof

        set g = the Grothendieck of X;

        defpred g[ set] means $1 is Grothendieck of X;

        consider Gclasses be set such that

         A1: Y in Gclasses iff Y in ( bool g) & g[Y] from XFAMILY:sch 1;

        

         A2: g in ( bool g) by ZFMISC_1:def 1;

        then

        reconsider Gclasses as non empty set by A1;

        set M = ( meet Gclasses);

        

         A3: M is epsilon-transitive

        proof

          let Y such that

           A4: Y in M;

          for Z st Z in Gclasses holds Y c= Z

          proof

            let Z;

            assume Z in Gclasses;

            then Y in Z & Z is epsilon-transitive by SETFAM_1:def 1, A4, A1;

            hence Y c= Z;

          end;

          hence Y c= M by SETFAM_1: 5;

        end;

        

         A5: M is power-closed

        proof

          let Z such that

           A6: Z in M;

          for Y st Y in Gclasses holds ( bool Z) in Y

          proof

            let Y;

            assume Y in Gclasses;

            then Z in Y & Y is power-closed by A1, A6, SETFAM_1:def 1;

            hence ( bool Z) in Y;

          end;

          hence ( bool Z) in M by SETFAM_1:def 1;

        end;

        M is FamUnion-closed

        proof

          let Z;

          let f be Function such that

           A7: ( dom f) = Z & ( rng f) c= M & Z in M;

          for Y st Y in Gclasses holds ( union ( rng f)) in Y

          proof

            let Y such that

             A8: Y in Gclasses;

            

             A9: Z in Y & Y is FamUnion-closed by A8, A1, A7, SETFAM_1:def 1;

            ( rng f) c= M & M c= Y by A8, A7, SETFAM_1: 7;

            then ( rng f) c= Y;

            hence ( union ( rng f)) in Y by A7, A9;

          end;

          hence ( union ( rng f)) in M by SETFAM_1:def 1;

        end;

        then

        reconsider M as Grothendieck by A3, A5;

        M is Grothendieck of X

        proof

          now

            let Y;

            assume Y in Gclasses;

            then Y is Grothendieck of X by A1;

            hence X in Y by Def4;

          end;

          hence X in M by SETFAM_1:def 1;

        end;

        then

        reconsider M as Grothendieck of X;

        take M;

        let G1 be Grothendieck of X;

        

         A10: (M /\ G1) is Grothendieck of X by Th1;

        (M /\ G1) c= M c= g by SETFAM_1: 3, A2, A1, XBOOLE_1: 17;

        then

         A11: (M /\ G1) c= g & (M /\ G1) c= G1 by XBOOLE_1: 17;

        then M c= (M /\ G1) by A10, A1, SETFAM_1: 3;

        hence thesis by A11;

      end;

      uniqueness ;

    end

    scheme :: CLASSES3:sch1

    ClosedUnderReplacement { X() -> set , U() -> Grothendieck of X() , F( set) -> set } :

{ F(x) where x be Element of X() : x in X() } in U()

      provided

       A1: Y in X() implies F(Y) in U();

      

       A2: U() is epsilon-transitive power-closed FamUnion-closed;

      deffunc S( set) = {F($1)};

      consider s be Function such that

       A3: ( dom s) = X() & for X st X in X() holds (s . X) = S(X) from FUNCT_1:sch 5;

      ( rng s) c= U()

      proof

        let y;

        assume y in ( rng s);

        then

        consider x such that

         A4: x in ( dom s) & (s . x) = y by FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

        ( bool F(x)) in U() by A2, A1, A4, A3;

        then

         A5: ( bool ( bool F(x))) c= U() by A2;

         S(x) c= ( bool F(x)) by ZFMISC_1: 68;

        then S(x) in ( bool ( bool F(x)));

        then y in ( bool ( bool F(x))) by A4, A3;

        hence thesis by A5;

      end;

      then

       A6: ( union ( rng s)) in U() by A3, A2, Def4;

      set FX = { F(x) where x be Element of X() : x in X() };

      

       A7: ( Union s) c= FX

      proof

        let y;

        assume y in ( Union s);

        then

        consider x such that

         A8: x in ( dom s) & y in (s . x) by CARD_5: 2;

        reconsider x as set by TARSKI: 1;

        (s . x) = S(x) by A8, A3;

        then y = F(x) by A8, TARSKI:def 1;

        hence thesis by A8, A3;

      end;

      FX c= ( Union s)

      proof

        let fx be object;

        assume fx in FX;

        then

        consider x be Element of X() such that

         A9: fx = F(x) & x in X();

        fx in S(x) = (s . x) by A9, A3, TARSKI:def 1;

        hence thesis by A9, A3, CARD_5: 2;

      end;

      then FX = ( Union s) by A7;

      hence thesis by CARD_3:def 4, A6;

    end;

    reserve U for Grothendieck;

    theorem :: CLASSES3:2

    

     Th2: for f be Function st ( dom f) in U & ( rng f) c= U holds ( rng f) in U

    proof

      let f be Function such that

       A1: ( dom f) in U & ( rng f) c= U;

      set A = ( dom f);

      

       A2: U is epsilon-transitive power-closed FamUnion-closed;

      deffunc S( set) = {(f . $1)};

      consider s be Function such that

       A3: ( dom s) = A & for X st X in A holds (s . X) = S(X) from FUNCT_1:sch 5;

      ( rng s) c= U

      proof

        let y;

        assume y in ( rng s);

        then

        consider x such that

         A4: x in ( dom s) & (s . x) = y by FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

        (f . x) in ( rng f) by A4, A3, FUNCT_1:def 3;

        then ( bool (f . x)) in U by A1, A2;

        then

         A5: ( bool ( bool (f . x))) c= U by A2;

         S(x) c= ( bool (f . x)) by ZFMISC_1: 68;

        then S(x) in ( bool ( bool (f . x)));

        then y in ( bool ( bool (f . x))) by A4, A3;

        hence thesis by A5;

      end;

      then

       A6: ( union ( rng s)) in U by A3, A1, A2;

      

       A7: ( Union s) c= ( rng f)

      proof

        let y;

        assume y in ( Union s);

        then

        consider x such that

         A8: x in ( dom s) & y in (s . x) by CARD_5: 2;

        reconsider x as set by TARSKI: 1;

        (s . x) = S(x) by A8, A3;

        then y = (f . x) by A8, TARSKI:def 1;

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

      end;

      ( rng f) c= ( Union s)

      proof

        let fx be object;

        assume fx in ( rng f);

        then

        consider x such that

         A9: x in ( dom f) & (f . x) = fx by FUNCT_1:def 3;

        reconsider x as set by A9;

        fx in S(x) = (s . x) by A9, A3, TARSKI:def 1;

        hence thesis by A9, A3, CARD_5: 2;

      end;

      then ( rng f) = ( Union s) by A7;

      hence thesis by CARD_3:def 4, A6;

    end;

    begin

    definition

      let x be object;

      :: CLASSES3:def6

      func Rrank x -> epsilon-transitive set equals ( Rank ( the_rank_of x));

      coherence ;

    end

    theorem :: CLASSES3:3

    

     Th3: X in ( Rank A) iff ex B st B in A & X in ( bool ( Rank B))

    proof

      thus X in ( Rank A) implies ex B st B in A & X in ( bool ( Rank B))

      proof

        assume

         A1: X in ( Rank A);

        per cases ;

          suppose A is limit_ordinal;

          then

          consider B such that

           A3: B in A & X in ( Rank B) by A1, CLASSES1: 29, CLASSES1: 31;

          take B;

          B c= (B \/ {B}) by XBOOLE_1: 7;

          then B c= ( succ B) by ORDINAL1:def 1;

          then ( Rank B) c= ( Rank ( succ B)) by CLASSES1: 37;

          then X in ( Rank ( succ B)) by A3;

          hence thesis by A3, CLASSES1: 30;

        end;

          suppose not A is limit_ordinal;

          then

          consider B be Ordinal such that

           A4: A = ( succ B) by ORDINAL1: 29;

          take B;

          thus thesis by A1, A4, ORDINAL1: 6, CLASSES1: 30;

        end;

      end;

      thus thesis by CLASSES1: 36, CLASSES1: 41;

    end;

    theorem :: CLASSES3:4

    

     Th4: Y in ( Rrank X) iff ex Z st Z in X & Y in ( bool ( Rrank Z))

    proof

      thus Y in ( Rrank X) implies ex Z st Z in X & Y in ( bool ( Rrank Z))

      proof

        assume Y in ( Rrank X);

        then

        consider B be Ordinal such that

         A1: B in ( the_rank_of X) & Y in ( bool ( Rank B)) by Th3;

        consider a be set such that

         A2: a in X & B c= ( the_rank_of a) by A1, CLASSES1: 70;

        ( Rank B) c= ( Rrank a) by A2, CLASSES1: 37;

        then Y c= ( Rrank a) by A1;

        hence thesis by A2;

      end;

      given Z be set such that

       A3: Z in X & Y in ( bool ( Rrank Z));

      ( succ ( the_rank_of Z)) c= ( the_rank_of X) by A3, CLASSES1: 68, ORDINAL1: 21;

      then

       A4: ( Rank ( succ ( the_rank_of Z))) c= ( Rrank X) by CLASSES1: 37;

      Y in ( Rank ( succ ( the_rank_of Z))) by A3, CLASSES1: 30;

      hence thesis by A4;

    end;

    theorem :: CLASSES3:5

    x in X & y in ( Rrank x) implies y in ( Rrank X)

    proof

      assume

       A1: x in X & y in ( Rrank x);

      reconsider x, y as set by TARSKI: 1;

      ( the_rank_of x) in ( the_rank_of X) by A1, CLASSES1: 68;

      then ( Rrank x) c= ( Rrank X) by ORDINAL1:def 2, CLASSES1: 36;

      hence thesis by A1;

    end;

    theorem :: CLASSES3:6

    Y in ( Rrank X) implies ex x st x in X & Y c= ( Rrank x)

    proof

      assume Y in ( Rrank X);

      then ex Z st Z in X & Y in ( bool ( Rrank Z)) by Th4;

      hence thesis;

    end;

    theorem :: CLASSES3:7

    X c= ( Rrank X) by CLASSES1:def 9;

    theorem :: CLASSES3:8

    X c= ( Rrank Y) implies ( Rrank X) c= ( Rrank Y)

    proof

      assume X c= ( Rrank Y);

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

      hence thesis by CLASSES1: 37;

    end;

    theorem :: CLASSES3:9

    X in ( Rrank Y) implies ( Rrank X) in ( Rrank Y)

    proof

      assume X in ( Rrank Y);

      then ( the_rank_of X) in ( the_rank_of Y) by CLASSES1: 66;

      hence thesis by CLASSES1: 36;

    end;

    theorem :: CLASSES3:10

    X in ( Rrank Y) or ( Rrank Y) c= ( Rrank X)

    proof

      assume not X in ( Rrank Y);

      then not ( the_rank_of X) in ( the_rank_of Y) by CLASSES1: 66;

      hence thesis by CLASSES1: 37, ORDINAL1: 16;

    end;

    theorem :: CLASSES3:11

    ( Rrank X) in ( Rrank Y) or ( Rrank Y) c= ( Rrank X)

    proof

      assume not ( Rrank X) in ( Rrank Y);

      then not ( the_rank_of X) in ( the_rank_of Y) by CLASSES1: 36;

      hence thesis by CLASSES1: 37, ORDINAL1: 16;

    end;

    theorem :: CLASSES3:12

    X in U & (X,A) are_equipotent implies A in U

    proof

      defpred P[ Ordinal] means for X st (X,$1) are_equipotent & X in U holds $1 in U;

      

       A1: for A be Ordinal st for C be Ordinal st C in A holds P[C] holds P[A]

      proof

        let A be Ordinal such that

         A2: for C be Ordinal st C in A holds P[C];

        let S be set such that

         A3: (S,A) are_equipotent & S in U;

        consider f be Function such that

         A4: f is one-to-one & ( dom f) = S & ( rng f) = A by A3, WELLORD2:def 4;

        ( rng f) c= U

        proof

          let y such that

           A5: y in ( rng f);

          reconsider B = y as Ordinal by A5, A4;

          

           A6: (B |` f) is one-to-one by A4, FUNCT_1: 58;

          

           A7: ( rng (B |` f)) = B by A4, RELAT_1: 89, A5, ORDINAL1:def 2;

          ( dom (B |` f)) in U by A3, A4, CLASSES1:def 1, RELAT_1: 186;

          hence thesis by A7, A6, WELLORD2:def 4, A5, A4, A2;

        end;

        hence A in U by A4, A3, Th2;

      end;

      for O be Ordinal holds P[O] from ORDINAL1:sch 2( A1);

      hence thesis;

    end;

    theorem :: CLASSES3:13

    

     Th13: X in Y in U implies X in U

    proof

      assume X in Y in U;

      then ( union Y) in U & X c= ( union Y) by Def2, ZFMISC_1: 74;

      hence thesis by CLASSES1:def 1;

    end;

    theorem :: CLASSES3:14

    

     Th14: X in U implies ( Rrank X) in U

    proof

      defpred P[ Ordinal] means for A be set st ( the_rank_of A) in $1 & A in U holds ( Rrank A) in U;

      

       A1: for A st for C st C in A holds P[C] holds P[A]

      proof

        let A such that

         A2: for C st C in A holds P[C];

        let S be set such that

         A3: ( the_rank_of S) in A & S in U;

        deffunc V( object) = ( bool ( Rrank $1));

        consider v be Function such that

         A4: ( dom v) = S & for x be object st x in S holds (v . x) = V(x) from FUNCT_1:sch 3;

        

         A5: ( rng v) c= U

        proof

          let y such that

           A6: y in ( rng v);

          consider x such that

           A7: x in ( dom v) & (v . x) = y by A6, FUNCT_1:def 3;

          ( succ ( the_rank_of x)) c= ( the_rank_of S) by ORDINAL1: 21, A7, A4, CLASSES1: 68;

          then

           A8: for S be set st ( the_rank_of S) in ( succ ( the_rank_of x)) & S in U holds ( Rrank S) in U by A2, A3;

          

           A9: x in U by A3, Th13, A7, A4;

          ( Rrank x) in U by A8, A9, ORDINAL1: 6;

          then ( bool ( Rrank x)) in U by Def1;

          hence thesis by A7, A4;

        end;

        

         A10: ( union ( rng v)) c= ( Rrank S)

        proof

          let a be object;

          assume a in ( union ( rng v));

          then

          consider b be set such that

           A11: a in b & b in ( rng v) by TARSKI:def 4;

          consider x be object such that

           A12: x in ( dom v) & (v . x) = b by A11, FUNCT_1:def 3;

          reconsider a, b, x as set by TARSKI: 1;

          b = ( bool ( Rrank x)) by A12, A4;

          hence thesis by A11, A12, A4, Th4;

        end;

        ( Rrank S) c= ( union ( rng v))

        proof

          let x be object;

          assume x in ( Rrank S);

          then

          consider a be set such that

           A13: a in S & x in ( bool ( Rrank a)) by Th4;

          (v . a) = ( bool ( Rrank a)) & (v . a) in ( rng v) by A13, A4, FUNCT_1:def 3;

          hence thesis by A13, TARSKI:def 4;

        end;

        then ( union ( rng v)) = ( Rrank S) by A10;

        hence ( Rrank S) in U by A5, A4, A3, Def3;

      end;

      

       A14: for O be Ordinal holds P[O] from ORDINAL1:sch 2( A1);

      ( the_rank_of X) in ( succ ( the_rank_of X)) by ORDINAL1: 6;

      hence thesis by A14;

    end;

    theorem :: CLASSES3:15

    A in U implies ( Rank A) in U

    proof

      defpred P[ Ordinal] means $1 in U implies ( Rank $1) in U;

      

       A1: for A st for C st C in A holds P[C] holds P[A]

      proof

        let A such that

         A2: for C st C in A holds P[C];

        assume

         A3: A in U;

        deffunc BR( Ordinal) = ( bool ( Rank $1));

        consider br be Sequence such that

         A4: ( dom br) = A & for O be Ordinal st O in A holds (br . O) = BR(O) from ORDINAL2:sch 2;

        

         A5: ( rng br) c= U

        proof

          let y be object;

          assume y in ( rng br);

          then

          consider B be object such that

           A6: B in ( dom br) & (br . B) = y by FUNCT_1:def 3;

          reconsider B as Ordinal by A6;

          B in U by A6, A4, A3, Th13;

          then ( bool ( Rank B)) in U & (br . B) = ( bool ( Rank B)) by A2, A4, A6, Def1;

          hence thesis by A6;

        end;

        

         A7: ( union ( rng br)) c= ( Rank A)

        proof

          let z;

          assume z in ( union ( rng br));

          then

          consider y be set such that

           A8: z in y & y in ( rng br) by TARSKI:def 4;

          consider B be object such that

           A9: B in ( dom br) & (br . B) = y by A8, FUNCT_1:def 3;

          reconsider B as Ordinal by A9;

          (br . B) = ( bool ( Rank B)) by A4, A9;

          hence thesis by A8, A9, A4, Th3;

        end;

        ( Rank A) c= ( union ( rng br))

        proof

          let x such that

           A10: x in ( Rank A);

          reconsider X = x as set by TARSKI: 1;

          consider B such that

           A11: B in A & X in ( bool ( Rank B)) by A10, Th3;

          

           A12: (br . B) in ( rng br) by A11, A4, FUNCT_1:def 3;

          (br . B) = ( bool ( Rank B)) by A11, A4;

          hence thesis by A11, A12, TARSKI:def 4;

        end;

        then ( Rank A) = ( union ( rng br)) by A7;

        hence thesis by A5, Def3, A4, A3;

      end;

      for O be Ordinal holds P[O] from ORDINAL1:sch 2( A1);

      hence thesis;

    end;

    begin

    theorem :: CLASSES3:16

    

     Th16: for X st X c= U & not X in U holds ex f be Function st f is one-to-one & ( dom f) = ( On U) & ( rng f) = X

    proof

      let X such that

       A1: X c= U & not X in U;

      for x be set st x in ( On U) holds x is Ordinal & x c= ( On U)

      proof

        let x be set;

        assume

         A2: x in ( On U);

        then x in U & x is Ordinal by ORDINAL1:def 9;

        then x c= U by ORDINAL1:def 2;

        hence thesis by A2, ORDINAL1:def 9;

      end;

      then ( On U) is epsilon-transitive epsilon-connected by ORDINAL1: 19;

      then

      reconsider Lambda = ( On U) as Ordinal;

      ex THE be Function st for x be set st {} <> x c= X holds (THE . x) in x

      proof

        consider V be Relation such that

         A3: V well_orders X by WELLORD2: 17;

        defpred The[ object, object] means for A be set st A = $1 holds $2 in A & for b be object st b in A holds [$2, b] in V;

        

         A4: for x st x in (( bool X) \ { {} }) holds ex u be object st The[x, u]

        proof

          let x such that

           A5: x in (( bool X) \ { {} });

          reconsider y = x as set by TARSKI: 1;

          consider a be object such that

           A6: a in y and

           A7: for b be object st b in y holds [a, b] in V by A3, WELLORD1: 5, A5, ZFMISC_1: 56;

          take a;

          thus thesis by A6, A7;

        end;

        consider THE be Function such that ( dom THE) = (( bool X) \ { {} }) and

         A8: for e be object st e in (( bool X) \ { {} }) holds The[e, (THE . e)] from CLASSES1:sch 1( A4);

        take THE;

        let x be set;

        assume {} <> x c= X;

        then x in (( bool X) \ { {} }) by ZFMISC_1: 56;

        hence thesis by A8;

      end;

      then

      consider THE be Function such that

       A9: for x be set st {} <> x c= X holds (THE . x) in x;

      deffunc ranks( set) = { ( the_rank_of x) where x be Element of $1 : x in $1 };

      

       A10: for A be set, x be object holds x in ranks(A) iff ex a be set st a in A & x = ( the_rank_of a)

      proof

        let A be set, x be object;

        thus x in ranks(A) implies ex a be set st a in A & x = ( the_rank_of a)

        proof

          assume x in ranks(A);

          then

          consider a be Element of A such that

           A11: x = ( the_rank_of a) & a in A;

          take a;

          thus thesis by A11;

        end;

        assume ex a be set st a in A & x = ( the_rank_of a);

        hence thesis;

      end;

      defpred Q[ set, object] means $2 in (X \ $1) & for B be Ordinal st B in ranks(\) holds ( the_rank_of $2) c= B;

      deffunc F( Sequence) = (THE . { x where x be Element of X : Q[( rng $1), x] });

      consider f be Sequence such that

       A12: ( dom f) = Lambda and

       A13: for A be Ordinal, L be Sequence st A in Lambda & L = (f | A) holds (f . A) = F(L) from ORDINAL1:sch 4;

      

       A14: for A be Ordinal st A in Lambda holds Q[( rng (f | A)), (f . A)]

      proof

        let A be Ordinal such that

         A15: A in Lambda;

        

         A16: A in U by A15, ORDINAL1:def 9;

        

         A17: ( dom (f | A)) = A by A12, RELAT_1: 62, A15, ORDINAL1:def 2;

        

         A18: (f . A) = F(|) by A15, A13;

        set II = { x where x be Element of X : Q[( rng (f | A)), x] };

        II c= X

        proof

          let i be object;

          assume i in II;

          then ex x be Element of X st i = x & Q[( rng (f | A)), x];

          hence thesis;

        end;

        then

        reconsider II as Subset of X;

        defpred P[ Ordinal] means ex a be set st a in (X \ ( rng (f | A))) & $1 = ( the_rank_of a);

        

         A19: ex O be Ordinal st P[O]

        proof

          assume

           A20: for O be Ordinal holds not P[O];

          

           A21: (X \ ( rng (f | A))) = {}

          proof

            assume (X \ ( rng (f | A))) <> {} ;

            then

            consider a be object such that

             A22: a in (X \ ( rng (f | A))) by XBOOLE_0:def 1;

             P[( the_rank_of a)] by A22;

            hence contradiction by A20;

          end;

          

           A23: ( dom (X |` (f | A))) in U by A17, A16, CLASSES1:def 1, FUNCT_1: 56;

          ( rng (X |` (f | A))) = X by A21, XBOOLE_1: 37, RELAT_1: 89;

          hence contradiction by A1, Th2, A23;

        end;

        consider Min be Ordinal such that

         A24: P[Min] & for O be Ordinal st P[O] holds Min c= O from ORDINAL1:sch 1( A19);

        consider t be set such that

         A25: t in (X \ ( rng (f | A))) & Min = ( the_rank_of t) by A24;

        for B be Ordinal st B in ranks(\) holds ( the_rank_of t) c= B

        proof

          let B be Ordinal such that

           A26: B in ranks(\);

          ex a be set st a in (X \ ( rng (f | A))) & B = ( the_rank_of a) by A10, A26;

          hence thesis by A24, A25;

        end;

        then t in II by A25;

        then (THE . II) in II by A9;

        then ex x be Element of X st x = (THE . II) & Q[( rng (f | A)), x];

        hence Q[( rng (f | A)), (f . A)] by A18;

      end;

      

       A27: f is one-to-one

      proof

        let x1,x2 be object such that

         A28: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        assume

         A29: x1 <> x2;

        reconsider x1, x2 as Ordinal by A28;

        

         A30: (f . x1) in (X \ ( rng (f | x1))) & (f . x2) in (X \ ( rng (f | x2))) by A14, A28, A12;

        per cases by A28, ORDINAL1:def 3, A29;

          suppose x1 in x2;

          then x1 in ( dom (f | x2)) & (f . x1) = ((f | x2) . x1) by A28, RELAT_1: 57, FUNCT_1: 49;

          then (f . x1) in ( rng (f | x2)) by FUNCT_1:def 3;

          hence contradiction by A30, XBOOLE_0:def 5, A28;

        end;

          suppose x2 in x1;

          then x2 in ( dom (f | x1)) & (f . x2) = ((f | x1) . x2) by A28, RELAT_1: 57, FUNCT_1: 49;

          then (f . x2) in ( rng (f | x1)) by FUNCT_1:def 3;

          hence contradiction by A30, XBOOLE_0:def 5, A28;

        end;

      end;

      

       A31: ( rng f) c= X

      proof

        let y such that

         A32: y in ( rng f);

        consider A be object such that

         A33: A in ( dom f) & (f . A) = y by A32, FUNCT_1:def 3;

        reconsider A as Ordinal by A33;

         Q[( rng (f | A)), (f . A)] by A12, A14, A33;

        hence thesis by A33;

      end;

      

       A34: X c= ( rng f)

      proof

        let x such that

         A35: x in X;

        assume

         A36: not x in ( rng f);

        ( Rrank x) in U by A1, A35, Th14;

        then

         A37: ( bool ( Rrank x)) in U by Def1;

        ( rng f) c= ( bool ( Rrank x))

        proof

          let y be object such that

           A38: y in ( rng f);

          consider A be object such that

           A39: A in ( dom f) & (f . A) = y by A38, FUNCT_1:def 3;

          reconsider A as Ordinal by A39;

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

          then not x in ( rng (f | A)) by A36;

          then x in (X \ ( rng (f | A))) by A35, XBOOLE_0:def 5;

          then ( the_rank_of x) in ranks(\);

          then ( the_rank_of (f . A)) in ( succ ( the_rank_of x)) by A39, A12, A14, ORDINAL1: 22;

          then

           A40: ( Rank ( succ ( the_rank_of (f . A)))) c= ( Rank ( succ ( the_rank_of x))) by CLASSES1: 37, ORDINAL1: 21;

          (f . A) in ( Rank ( succ ( the_rank_of (f . A)))) by CLASSES1:def 8;

          then (f . A) in ( Rank ( succ ( the_rank_of x))) by A40;

          hence thesis by A39, CLASSES1: 30;

        end;

        then

         A41: ( rng f) in U by A37, CLASSES1:def 1;

        

         A42: ( rng (f " )) = ( dom f) & ( dom (f " )) = ( rng f) by A27, FUNCT_1: 33;

        ( dom f) in U by A42, A41, A12, ORDINAL2: 7, Th2;

        then ( dom f) in Lambda by ORDINAL1:def 9;

        hence thesis by A12;

      end;

      take f;

      thus thesis by A34, A31, A27, A12;

    end;

    theorem :: CLASSES3:17

    

     Th17: for U be Grothendieck holds U is Tarski

    proof

      let U be Grothendieck;

      thus U is subset-closed;

      thus for X be set holds X in U implies ( bool X) in U by Def1;

      let X be set such that

       A1: X c= U;

       not X in U implies (X,U) are_equipotent

      proof

        assume not X in U;

        then

        consider f be Function such that

         A2: f is one-to-one & ( dom f) = ( On U) & ( rng f) = X by A1, Th16;

         not U in U;

        then

        consider g be Function such that

         A3: g is one-to-one & ( dom g) = ( On U) & ( rng g) = U by Th16;

        set gf = (g * (f " ));

        ( dom (f " )) = X & ( rng (f " )) = ( On U) by A2, FUNCT_1: 33;

        then ( dom gf) = X & ( rng gf) = U by A3, RELAT_1: 27, RELAT_1: 28;

        hence thesis by A2, A3, WELLORD2:def 4;

      end;

      hence thesis;

    end;

    registration

      cluster epsilon-transitive power-closed FamUnion-closed -> universal for set;

      coherence

      proof

        let X be set;

        assume

         A1: X is epsilon-transitive power-closed FamUnion-closed;

        then X is Tarski by Th17;

        hence thesis by A1;

      end;

      cluster universal -> epsilon-transitive power-closed FamUnion-closed for set;

      coherence ;

    end

    theorem :: CLASSES3:18

    

     Th18: for G be Grothendieck of X holds ( Tarski-Class X) c= G

    proof

      let G be Grothendieck of X;

      G is_Tarski-Class_of X by Def4;

      hence thesis by CLASSES1:def 4;

    end;

    theorem :: CLASSES3:19

    

     Th19: for X be infinite set holds not X in ( Tarski-Class {X})

    proof

      let A be infinite set;

      deffunc Bool( set, set) = ($2 \/ ( bool $2));

      consider f be Function such that

       A1: ( dom f) = NAT & (f . 0 ) = { {A}, {} } and

       A2: for n be Nat holds (f . (n + 1)) = Bool(n,.) from NAT_1:sch 11;

      set U = ( Union f);

      (f . ( 0 + 1)) = ((f . 0 ) \/ ( bool (f . 0 ))) & {} c= { {A}, {} } by A2;

      then

       A3: {} in (f . 1) by A1, XBOOLE_0:def 3;

      then

       A4: {} in U by A1, CARD_5: 2;

      defpred Min[ object, object] means $1 in (f . $2) & $2 in ( dom f) & for i,j be Nat st i < j = $2 holds not $1 in (f . i);

      

       A5: for x be object st x in U holds ex y be object st Min[x, y]

      proof

        let x such that

         A6: x in U;

        consider k be object such that

         A7: k in ( dom f) & x in (f . k) by A6, CARD_5: 2;

        reconsider k as Nat by A7, A1;

        defpred M[ Nat] means x in (f . $1);

         M[k] by A7;

        then

         A8: ex k be Nat st M[k];

        consider k be Nat such that

         A9: M[k] and

         A10: for n be Nat st M[n] holds k <= n from NAT_1:sch 5( A8);

        take k;

        thus thesis by A10, A9, A1, ORDINAL1:def 12;

      end;

      consider Min be Function such that

       A11: ( dom Min) = U & for x be object st x in U holds Min[x, (Min . x)] from CLASSES1:sch 1( A5);

      

       A12: U is subset-closed

      proof

        let X, Y such that

         A13: X in U & Y c= X;

        set x = (Min . X);

        

         A14: Min[X, x] by A11, A13;

        then

        reconsider x as Nat by A1;

        per cases by NAT_1: 3;

          suppose X = Y;

          hence thesis by A13;

        end;

          suppose x = 0 & X <> Y;

          then X = {A} or X = {} by A1, TARSKI:def 2, A14;

          hence thesis by A4, A13, ZFMISC_1: 33;

        end;

          suppose x > 0 ;

          then

          reconsider x1 = (x - 1) as Element of NAT by NAT_1: 20;

          x1 < (x1 + 1) by NAT_1: 13;

          then

           A15: not X in (f . x1) by A11, A13;

          

           A16: (f . (x1 + 1)) = ((f . x1) \/ ( bool (f . x1))) by A2;

          then X in ( bool (f . x1)) by A14, A15, XBOOLE_0:def 3;

          then X c= (f . x1);

          then Y c= (f . x1) by A13;

          then Y in (f . x) by A16, XBOOLE_0:def 3;

          hence thesis by A14, CARD_5: 2;

        end;

      end;

      

       A17: for X st X in U holds ( bool X) in U

      proof

        let X such that

         A18: X in U;

        set x = (Min . X);

        

         A19: Min[X, x] by A11, A18;

        reconsider x as Nat by A19, A1;

        

         A20: (f . (x + 1)) = ((f . x) \/ ( bool (f . x))) by A2;

        per cases by NAT_1: 3;

          suppose

           A21: x = 0 ;

          then X = {A} or X = {} by A1, TARSKI:def 2, A19;

          then ( bool X) c= { {A}, {} } by ZFMISC_1: 7, ZFMISC_1: 24, ZFMISC_1: 1;

          then ( bool X) in (f . 1) by A20, A21, A1, XBOOLE_0:def 3;

          hence thesis by A1, CARD_5: 2;

        end;

          suppose x > 0 ;

          then

          reconsider x1 = (x - 1) as Element of NAT by NAT_1: 20;

          x1 < (x1 + 1) by NAT_1: 13;

          then

           A22: not X in (f . x1) by A11, A18;

          

           A23: (f . (x1 + 1)) = ((f . x1) \/ ( bool (f . x1))) by A2;

          

           A24: (f . (x + 1)) = ((f . x) \/ ( bool (f . x))) by A2;

          X in ( bool (f . x1)) by A23, A19, A22, XBOOLE_0:def 3;

          then ( bool X) c= ( bool (f . x1)) by ZFMISC_1: 67;

          then ( bool X) c= (f . x) by A23, XBOOLE_1: 10;

          then ( bool X) in (f . (x + 1)) by A24, XBOOLE_0:def 3;

          hence thesis by A1, CARD_5: 2;

        end;

      end;

      defpred D[ Nat] means (f . $1) is finite;

      

       A25: D[ 0 ] by A1;

      

       A26: for n be Nat st D[n] holds D[(n + 1)]

      proof

        let n be Nat such that

         A27: D[n];

        (f . (n + 1)) = ((f . n) \/ ( bool (f . n))) by A2;

        hence thesis by A27;

      end;

      

       A28: for n be Nat holds D[n] from NAT_1:sch 2( A25, A26);

      

       A29: for x be set st x in ( dom f) holds (f . x) is countable

      proof

        let x be set such that

         A30: x in ( dom f);

        reconsider x as Nat by A30, A1;

         D[x] by A28;

        hence thesis;

      end;

      then

       A31: U is countable by CARD_4: 11, A1;

      for X holds X c= U implies (X,U) are_equipotent or X in U

      proof

        let X such that

         A32: X c= U;

        per cases ;

          suppose ( card X) = omega or X = {} ;

          then ( card U) = ( card X) or X = {} by A32, CARD_1: 11, CARD_3:def 14, A29, CARD_4: 11, A1;

          hence thesis by A3, A1, CARD_5: 2, CARD_1: 5;

        end;

          suppose

           A33: ( card X) <> omega & X <> {} ;

          then ( card X) c< omega by A32, CARD_3:def 14, A31;

          then ( card X) in omega by ORDINAL1: 11;

          then

           A34: X is finite;

          defpred P[ object, object] means $1 in (f . $2) & $2 in ( dom f);

          

           A35: for x be object st x in X holds ex u be object st P[x, u]

          proof

            let x;

            assume x in X;

            then ex n be object st n in ( dom f) & x in (f . n) by A32, CARD_5: 2;

            hence thesis;

          end;

          consider fX be Function such that

           A36: ( dom fX) = X and

           A37: for x be object st x in X holds P[x, (fX . x)] from CLASSES1:sch 1( A35);

           A38:

          now

            let y be object;

            assume y in ( rng fX);

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

            hence y is natural by A1, A37, A36;

          end;

          reconsider RNG = ( rng fX) as finite natural-membered non empty set by A33, RELAT_1: 42, A38, MEMBERED:def 6, A36, A34, FINSET_1: 8;

          set m = ( max RNG);

          m in omega by ORDINAL1:def 12;

          then

          reconsider m as Nat;

          

           A39: (f . (m + 1)) = ((f . m) \/ ( bool (f . m))) & (m + 1) in omega by A2;

          X c= (f . m)

          proof

            let x be object such that

             A40: x in X;

             P[x, (fX . x)] by A40, A37;

            then

            reconsider k = (fX . x) as Nat by A1;

            k in ( rng fX) by A40, A36, FUNCT_1:def 3;

            then

             A41: k <= m by XXREAL_2:def 8;

            defpred Q[ Nat] means x in (f . $1);

            

             A42: Q[k] by A40, A37;

            

             A43: for i be Nat st k <= i & Q[i] holds Q[(i + 1)]

            proof

              let i be Nat such that

               A44: k <= i & Q[i];

              (f . (i + 1)) = ((f . i) \/ ( bool (f . i))) by A2;

              hence thesis by A44, XBOOLE_0:def 3;

            end;

            for i be Nat st k <= i holds Q[i] from NAT_1:sch 8( A42, A43);

            hence thesis by A41;

          end;

          then X in (f . (m + 1)) by A39, XBOOLE_0:def 3;

          hence thesis by A1, CARD_5: 2;

        end;

      end;

      then

       A45: U is Tarski by A12, A17;

       {A} in (f . 0 ) & 0 in omega by A1, TARSKI:def 2;

      then U is_Tarski-Class_of {A} by A45, CARD_5: 2, A1;

      then

       A46: ( Tarski-Class {A}) c= U by CLASSES1:def 4;

       not A in U

      proof

        assume

         A48: A in U;

        then

         A49: Min[A, (Min . A)] by A11;

        then

        reconsider x = (Min . A) as Nat by A1;

        per cases by NAT_1: 3;

          suppose x = 0 ;

          hence thesis by A1, A49;

        end;

          suppose x > 0 ;

          then

          reconsider x1 = (x - 1) as Element of NAT by NAT_1: 20;

          x1 < (x1 + 1) by NAT_1: 13;

          then

           A50: not A in (f . x1) by A48, A11;

          

           A51: (f . (x1 + 1)) = ((f . x1) \/ ( bool (f . x1))) by A2;

          A in ( bool (f . x1)) by A51, A49, A50, XBOOLE_0:def 3;

          then A c= (f . x1) & (f . x1) is finite by A28;

          hence thesis;

        end;

      end;

      hence thesis by A46;

    end;

    theorem :: CLASSES3:20

    for X be infinite set holds ( Tarski-Class {X}) c< ( GrothendieckUniverse {X})

    proof

      let X be infinite set;

      thus ( Tarski-Class {X}) c= ( GrothendieckUniverse {X}) by Th18;

      ( GrothendieckUniverse {X}) is union-closed;

      then ( union {X}) in ( GrothendieckUniverse {X}) by Def4;

      hence thesis by Th19;

    end;

    theorem :: CLASSES3:21

    ( GrothendieckUniverse X) is Universe & for U be Universe st X in U holds ( GrothendieckUniverse X) c= U

    proof

      set G = ( GrothendieckUniverse X);

      thus G is Universe by Def4;

      let U be Universe;

      assume X in U;

      then U is Grothendieck of X by Def4;

      hence thesis by GDef;

    end;

    theorem :: CLASSES3:22

    for X be epsilon-transitive set holds ( Tarski-Class X) = ( GrothendieckUniverse X)

    proof

      let X be epsilon-transitive set;

      ( Tarski-Class X) is Grothendieck of X by Def4, CLASSES1: 2;

      hence thesis by GDef, Th18;

    end;