classes1.miz



    begin

    reserve W,X,Y,Z for set,

f,g for Function,

a,x,y,z for set;

    definition

      let B be set;

      :: CLASSES1:def1

      attr B is subset-closed means

      : Def1: for X, Y holds X in B & Y c= X implies Y in B;

    end

    definition

      let B be set;

      :: CLASSES1:def2

      attr B is Tarski means B is subset-closed & (for X holds X in B implies ( bool X) in B) & for X holds X c= B implies (X,B) are_equipotent or X in B;

    end

    definition

      let A,B be set;

      :: CLASSES1:def3

      pred B is_Tarski-Class_of A means A in B & B is Tarski;

    end

    definition

      let A be set;

      :: CLASSES1:def4

      func Tarski-Class A -> set means

      : Def4: it is_Tarski-Class_of A & for D be set st D is_Tarski-Class_of A holds it c= D;

      existence

      proof

        consider Big be set such that

         A1: A in Big and

         A2: for X, Y holds X in Big & Y c= X implies Y in Big and

         A3: (for X holds X in Big implies ( bool X) in Big) & for X holds X c= Big implies (X,Big) are_equipotent or X in Big by ZFMISC_1: 112;

        

         A4: Big is Tarski by A3, A2, Def1;

        defpred P[ set] means $1 is_Tarski-Class_of A;

        consider Classes be set such that

         A5: X in Classes iff X in ( bool Big) & P[X] from XFAMILY:sch 1;

        set IT = ( meet Classes);

        

         A6: Big in ( bool Big) & Big is_Tarski-Class_of A by A1, A4, ZFMISC_1:def 1;

        then

         A7: Big in Classes by A5;

        

         A8: Classes <> {} by A5, A6;

         A9:

        now

          let X;

          assume X in Classes;

          then X is_Tarski-Class_of A by A5;

          hence A in X;

        end;

        then

         A10: A in IT by A8, SETFAM_1:def 1;

        take IT;

        thus A in IT by A8, A9, SETFAM_1:def 1;

        thus

         A11: X in IT & Y c= X implies Y in IT

        proof

          assume that

           A12: X in IT and

           A13: Y c= X;

          now

            let Z;

            assume

             A14: Z in Classes;

            then Z is_Tarski-Class_of A by A5;

            then Z is Tarski;

            then

             A15: Z is subset-closed;

            X in Z by A12, A14, SETFAM_1:def 1;

            hence Y in Z by A13, A15;

          end;

          hence thesis by A8, SETFAM_1:def 1;

        end;

        thus

         A16: X in IT implies ( bool X) in IT

        proof

          assume

           A17: X in IT;

          now

            let Z;

            assume

             A18: Z in Classes;

            then Z is_Tarski-Class_of A by A5;

            then

             A19: Z is Tarski;

            X in Z by A17, A18, SETFAM_1:def 1;

            hence ( bool X) in Z by A19;

          end;

          hence thesis by A8, SETFAM_1:def 1;

        end;

        thus

         A20: X c= IT implies (X,IT) are_equipotent or X in IT

        proof

          assume that

           A21: X c= IT and

           A22: not (X,IT) are_equipotent ;

          now

            let Z;

            assume

             A23: Z in Classes;

            then Z is_Tarski-Class_of A by A5;

            then

             A24: Z is Tarski;

            

             A25: IT c= Z by A23, SETFAM_1: 3;

            then X c= Z by A21;

            then (X,Z) are_equipotent or X in Z by A24;

            hence X in Z by A21, A22, A25, CARD_1: 24;

          end;

          hence thesis by A8, SETFAM_1:def 1;

        end;

        let D be set;

        assume

         A26: D is_Tarski-Class_of A;

        then

         A27: A in D;

        

         A28: D is Tarski by A26;

        then

         A29: D is subset-closed;

        

         A30: (IT /\ D) is_Tarski-Class_of A

        proof

          thus A in (IT /\ D) by A10, A27, XBOOLE_0:def 4;

          thus X in (IT /\ D) & Y c= X implies Y in (IT /\ D)

          proof

            assume that

             A31: X in (IT /\ D) and

             A32: Y c= X;

            

             A33: X in IT by A31, XBOOLE_0:def 4;

            

             A34: X in D by A31, XBOOLE_0:def 4;

            

             A35: Y in IT by A11, A32, A33;

            Y in D by A29, A32, A34;

            hence thesis by A35, XBOOLE_0:def 4;

          end;

          thus X in (IT /\ D) implies ( bool X) in (IT /\ D)

          proof

            assume

             A36: X in (IT /\ D);

            then

             A37: X in IT by XBOOLE_0:def 4;

            

             A38: X in D by A36, XBOOLE_0:def 4;

            

             A39: ( bool X) in IT by A16, A37;

            ( bool X) in D by A28, A38;

            hence thesis by A39, XBOOLE_0:def 4;

          end;

          let X such that

           A40: X c= (IT /\ D) and

           A41: not (X,(IT /\ D)) are_equipotent ;

          

           A42: (IT /\ D) c= IT by XBOOLE_1: 17;

          

           A43: (IT /\ D) c= D by XBOOLE_1: 17;

          

           A44: not (X,IT) are_equipotent by A40, A41, A42, CARD_1: 24;

          

           A45: X c= D & not (X,D) are_equipotent by A40, A41, A43, CARD_1: 24;

          

           A46: X in IT by A20, A40, A42, A44, XBOOLE_1: 1;

          X in D by A28, A45;

          hence thesis by A46, XBOOLE_0:def 4;

        end;

        (IT /\ D) c= Big

        proof

          let x be object;

          assume x in (IT /\ D);

          then x in IT by XBOOLE_0:def 4;

          hence thesis by A7, SETFAM_1:def 1;

        end;

        then

         A47: IT c= (IT /\ D) by SETFAM_1: 3, A5, A30;

        (IT /\ D) c= D by XBOOLE_1: 17;

        hence thesis by A47;

      end;

      uniqueness ;

    end

    registration

      let A be set;

      cluster ( Tarski-Class A) -> non empty;

      coherence

      proof

        ( Tarski-Class A) is_Tarski-Class_of A by Def4;

        hence thesis;

      end;

    end

    theorem :: CLASSES1:1

    W is Tarski iff W is subset-closed & (for X st X in W holds ( bool X) in W) & for X st X c= W & ( card X) in ( card W) holds X in W

    proof

      hereby

        assume

         A1: W is Tarski;

        hence W is subset-closed & for X st X in W holds ( bool X) in W;

        let X;

        assume that

         A2: X c= W and

         A3: ( card X) in ( card W);

        ( card X) <> ( card W) by A3;

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

        hence X in W by A1, A2;

      end;

      now

        assume

         A4: for X st X c= W & ( card X) in ( card W) holds X in W;

        let X;

        assume X c= W;

        then ( card X) c= ( card W) & not ( card X) in ( card W) or X in W by A4, CARD_1: 11;

        hence (X,W) are_equipotent or X in W by CARD_1: 3, CARD_1: 5;

      end;

      hence thesis;

    end;

    theorem :: CLASSES1:2

    

     Th2: X in ( Tarski-Class X)

    proof

      ( Tarski-Class X) is_Tarski-Class_of X by Def4;

      hence thesis;

    end;

    theorem :: CLASSES1:3

    

     Th3: Y in ( Tarski-Class X) & Z c= Y implies Z in ( Tarski-Class X)

    proof

      ( Tarski-Class X) is_Tarski-Class_of X by Def4;

      then ( Tarski-Class X) is Tarski;

      then ( Tarski-Class X) is subset-closed;

      hence thesis;

    end;

    theorem :: CLASSES1:4

    

     Th4: Y in ( Tarski-Class X) implies ( bool Y) in ( Tarski-Class X)

    proof

      ( Tarski-Class X) is_Tarski-Class_of X by Def4;

      then ( Tarski-Class X) is Tarski;

      hence thesis;

    end;

    theorem :: CLASSES1:5

    

     Th5: Y c= ( Tarski-Class X) implies (Y,( Tarski-Class X)) are_equipotent or Y in ( Tarski-Class X)

    proof

      ( Tarski-Class X) is_Tarski-Class_of X by Def4;

      then ( Tarski-Class X) is Tarski;

      hence thesis;

    end;

    theorem :: CLASSES1:6

    Y c= ( Tarski-Class X) & ( card Y) in ( card ( Tarski-Class X)) implies Y in ( Tarski-Class X)

    proof

      assume that

       A1: Y c= ( Tarski-Class X) and

       A2: ( card Y) in ( card ( Tarski-Class X));

      ( card Y) <> ( card ( Tarski-Class X)) by A2;

      hence thesis by A1, Th5, CARD_1: 5;

    end;

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

A,B,C for Ordinal,

L for Sequence;

    definition

      let X, A;

      :: CLASSES1:def5

      func Tarski-Class (X,A) -> set means

      : Def5: ex L st it = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = {X} & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = (({ u : ex v st v in (L . C) & u c= v } \/ { ( bool v) : v in (L . C) }) \/ (( bool (L . C)) /\ ( Tarski-Class X)))) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = (( union ( rng (L | C))) /\ ( Tarski-Class X));

      correctness

      proof

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

        (ex x be object, 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,|)) & for x1,x2 be set st (ex L st x1 = ( 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,|)) & (ex L st x2 = ( 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,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

    end

     Lm1:

    now

      let X;

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

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

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

      thus A <> 0 & A is limit_ordinal & ( dom L) = A & (for B st B in A holds (L . B) = ( Tarski-Class (X,B))) implies ( Tarski-Class (X,A)) = (( union ( rng L)) /\ ( Tarski-Class X))

      proof

        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) = F(B);

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

      end;

    end;

    definition

      let X, A;

      :: original: Tarski-Class

      redefine

      func Tarski-Class (X,A) -> Subset of ( Tarski-Class X) ;

      coherence

      proof

        defpred P[ Ordinal] means ( Tarski-Class (X,$1)) is Subset of ( Tarski-Class X);

         {X} c= ( Tarski-Class X)

        proof

          let x be object;

          assume x in {X};

          then x = X by TARSKI:def 1;

          hence thesis by Th2;

        end;

        then

         A1: P[ 0 ] by Lm1;

        

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

        proof

          assume ( Tarski-Class (X,B)) is Subset of ( Tarski-Class X);

          then

          reconsider S = ( Tarski-Class (X,B)) as Subset of ( Tarski-Class X);

          set Y = ( Tarski-Class (X,( succ B)));

          Y c= ( Tarski-Class X)

          proof

            let x be object;

            assume x in Y;

            then x in (({ u : ex v st v in S & u c= v } \/ { ( bool v) : v in S }) \/ (( bool S) /\ ( Tarski-Class X))) by Lm1;

            then

             A3: x in ({ u : ex v st v in S & u c= v } \/ { ( bool v) : v in S }) or x in (( bool S) /\ ( Tarski-Class X)) by XBOOLE_0:def 3;

             A4:

            now

              assume x in { u : ex v st v in S & u c= v };

              then ex u st x = u & ex v st v in S & u c= v;

              hence thesis;

            end;

            now

              assume x in { ( bool v) : v in S };

              then ex v st x = ( bool v) & v in S;

              hence thesis by Th4;

            end;

            hence thesis by A3, A4, XBOOLE_0:def 3, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        

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

        proof

          let B such that

           A6: B <> 0 & B is limit_ordinal and for C st C in B holds ( Tarski-Class (X,C)) is Subset of ( Tarski-Class X);

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

          consider L such that

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

          ( Tarski-Class (X,B)) = (( union ( rng L)) /\ ( Tarski-Class X)) by A6, A7, Lm1;

          hence thesis by XBOOLE_1: 17;

        end;

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

        hence thesis;

      end;

    end

    theorem :: CLASSES1:7

    ( Tarski-Class (X, {} )) = {X} by Lm1;

    theorem :: CLASSES1:8

    ( Tarski-Class (X,( succ A))) = (({ u : ex v st v in ( Tarski-Class (X,A)) & u c= v } \/ { ( bool v) : v in ( Tarski-Class (X,A)) }) \/ (( bool ( Tarski-Class (X,A))) /\ ( Tarski-Class X))) by Lm1;

    theorem :: CLASSES1:9

    

     Th9: A <> {} & A is limit_ordinal implies ( Tarski-Class (X,A)) = { u : ex B st B in A & u in ( Tarski-Class (X,B)) }

    proof

      assume

       A1: A <> {} & A is limit_ordinal;

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

      consider L such that

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

      

       A3: ( Tarski-Class (X,A)) = (( union ( rng L)) /\ ( Tarski-Class X)) by A1, A2, Lm1;

      thus ( Tarski-Class (X,A)) c= { u : ex B st B in A & u in ( Tarski-Class (X,B)) }

      proof

        let x be object;

        assume x in ( Tarski-Class (X,A));

        then x in ( union ( rng L)) by A3, XBOOLE_0:def 4;

        then

        consider Y such that

         A4: x in Y and

         A5: Y in ( rng L) by TARSKI:def 4;

        consider y be object such that

         A6: y in ( dom L) and

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

        reconsider y as Ordinal by A6;

        Y = ( Tarski-Class (X,y)) by A2, A6, A7;

        hence thesis by A2, A4, A6;

      end;

      let x be object;

      assume x in { u : ex B st B in A & u in ( Tarski-Class (X,B)) };

      then

      consider u such that

       A8: x = u and

       A9: ex B st B in A & u in ( Tarski-Class (X,B));

      consider B such that

       A10: B in A and

       A11: u in ( Tarski-Class (X,B)) by A9;

      (L . B) = ( Tarski-Class (X,B)) by A2, A10;

      then ( Tarski-Class (X,B)) in ( rng L) by A2, A10, FUNCT_1:def 3;

      then u in ( union ( rng L)) by A11, TARSKI:def 4;

      hence thesis by A3, A8, XBOOLE_0:def 4;

    end;

    theorem :: CLASSES1:10

    

     Th10: Y in ( Tarski-Class (X,( succ A))) iff Y c= ( Tarski-Class (X,A)) & Y in ( Tarski-Class X) or ex Z st Z in ( Tarski-Class (X,A)) & (Y c= Z or Y = ( bool Z))

    proof

      set T1 = { u : ex v st v in ( Tarski-Class (X,A)) & u c= v };

      set T2 = { ( bool v) : v in ( Tarski-Class (X,A)) };

      set T3 = (( bool ( Tarski-Class (X,A))) /\ ( Tarski-Class X));

      

       A1: ( Tarski-Class (X,( succ A))) = ((T1 \/ T2) \/ T3) by Lm1;

      thus Y in ( Tarski-Class (X,( succ A))) implies Y c= ( Tarski-Class (X,A)) & Y in ( Tarski-Class X) or ex Z st Z in ( Tarski-Class (X,A)) & (Y c= Z or Y = ( bool Z))

      proof

        assume Y in ( Tarski-Class (X,( succ A)));

        then

         A2: Y in (T1 \/ T2) or Y in T3 by A1, XBOOLE_0:def 3;

         A3:

        now

          assume Y in T1;

          then ex u st Y = u & ex v st v in ( Tarski-Class (X,A)) & u c= v;

          hence ex Z st Z in ( Tarski-Class (X,A)) & (Y c= Z or Y = ( bool Z));

        end;

        now

          assume Y in T2;

          then ex v st Y = ( bool v) & v in ( Tarski-Class (X,A));

          hence ex Z st Z in ( Tarski-Class (X,A)) & (Y c= Z or Y = ( bool Z));

        end;

        hence thesis by A2, A3, XBOOLE_0:def 3, XBOOLE_0:def 4;

      end;

      assume

       A4: Y c= ( Tarski-Class (X,A)) & Y in ( Tarski-Class X) or ex Z st Z in ( Tarski-Class (X,A)) & (Y c= Z or Y = ( bool Z));

       A5:

      now

        assume Y c= ( Tarski-Class (X,A)) & Y in ( Tarski-Class X);

        then Y in T3 by XBOOLE_0:def 4;

        hence thesis by A1, XBOOLE_0:def 3;

      end;

      now

        given Z such that

         A6: Z in ( Tarski-Class (X,A)) and

         A7: Y c= Z or Y = ( bool Z);

        reconsider Z as Element of ( Tarski-Class X) by A6;

        reconsider y = Y as Element of ( Tarski-Class X) by A6, A7, Th3, Th4;

         A8:

        now

          assume Y c= Z;

          then y in T1 by A6;

          then Y in (T1 \/ T2) by XBOOLE_0:def 3;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

        now

          assume Y = ( bool Z);

          then y in T2 by A6;

          then Y in (T1 \/ T2) by XBOOLE_0:def 3;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

        hence thesis by A7, A8;

      end;

      hence thesis by A4, A5;

    end;

    theorem :: CLASSES1:11

    Y c= Z & Z in ( Tarski-Class (X,A)) implies Y in ( Tarski-Class (X,( succ A))) by Th10;

    theorem :: CLASSES1:12

    Y in ( Tarski-Class (X,A)) implies ( bool Y) in ( Tarski-Class (X,( succ A))) by Th10;

    theorem :: CLASSES1:13

    

     Th13: A <> {} & A is limit_ordinal implies (x in ( Tarski-Class (X,A)) iff ex B st B in A & x in ( Tarski-Class (X,B)))

    proof

      assume

       A1: A <> {} & A is limit_ordinal;

      then

       A2: ( Tarski-Class (X,A)) = { u : ex B st B in A & u in ( Tarski-Class (X,B)) } by Th9;

      thus x in ( Tarski-Class (X,A)) implies ex B st B in A & x in ( Tarski-Class (X,B))

      proof

        assume x in ( Tarski-Class (X,A));

        then ex u st x = u & ex B st B in A & u in ( Tarski-Class (X,B)) by A2;

        hence thesis;

      end;

      given B such that

       A3: B in A and

       A4: x in ( Tarski-Class (X,B));

      reconsider u = x as Element of ( Tarski-Class X) by A4;

      u in { v : ex B st B in A & v in ( Tarski-Class (X,B)) } by A3, A4;

      hence thesis by A1, Th9;

    end;

    theorem :: CLASSES1:14

    A <> {} & A is limit_ordinal & Y in ( Tarski-Class (X,A)) & (Z c= Y or Z = ( bool Y)) implies Z in ( Tarski-Class (X,A))

    proof

      assume that

       A1: A <> {} and

       A2: A is limit_ordinal and

       A3: Y in ( Tarski-Class (X,A));

      consider B such that

       A4: B in A and

       A5: Y in ( Tarski-Class (X,B)) by A1, A2, A3, Th13;

      

       A6: ( bool Y) in ( Tarski-Class (X,( succ B))) by A5, Th10;

      

       A7: Z c= Y implies Z in ( Tarski-Class (X,( succ B))) by A5, Th10;

      

       A8: ( succ B) in A by A2, A4, ORDINAL1: 28;

      assume Z c= Y or Z = ( bool Y);

      hence thesis by A2, A6, A7, A8, Th13;

    end;

    theorem :: CLASSES1:15

    

     Th15: ( Tarski-Class (X,A)) c= ( Tarski-Class (X,( succ A)))

    proof

      let x be object;

      assume x in ( Tarski-Class (X,A));

      then x in { u : ex v st v in ( Tarski-Class (X,A)) & u c= v };

      then

       A1: x in ({ u : ex v st v in ( Tarski-Class (X,A)) & u c= v } \/ { ( bool v) : v in ( Tarski-Class (X,A)) }) by XBOOLE_0:def 3;

      ( Tarski-Class (X,( succ A))) = (({ u : ex v st v in ( Tarski-Class (X,A)) & u c= v } \/ { ( bool v) : v in ( Tarski-Class (X,A)) }) \/ (( bool ( Tarski-Class (X,A))) /\ ( Tarski-Class X))) by Lm1;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    theorem :: CLASSES1:16

    

     Th16: A c= B implies ( Tarski-Class (X,A)) c= ( Tarski-Class (X,B))

    proof

      defpred OnP[ Ordinal] means A c= $1 implies ( Tarski-Class (X,A)) c= ( Tarski-Class (X,$1));

      

       A1: for B st for C st C in B holds OnP[C] holds OnP[B]

      proof

        let B such that

         A2: for C st C in B holds OnP[C] and

         A3: A c= B;

        let x be object;

        assume

         A4: x in ( Tarski-Class (X,A));

        now

          assume

           A5: A <> B;

          then

           A6: A in B by ORDINAL1: 11, A3, XBOOLE_0:def 8;

          

           A7: B <> {} by A3, A5;

           A8:

          now

            given C such that

             A9: B = ( succ C);

            A c= C & C in B by A6, A9, ORDINAL1: 22;

            then

             A10: ( Tarski-Class (X,A)) c= ( Tarski-Class (X,C)) by A2;

            ( Tarski-Class (X,C)) c= ( Tarski-Class (X,B)) by A9, Th15;

            then ( Tarski-Class (X,A)) c= ( Tarski-Class (X,B)) by A10;

            hence thesis by A4;

          end;

          now

            assume for C holds B <> ( succ C);

            then ( Tarski-Class (X,B)) = { v : ex C st C in B & v in ( Tarski-Class (X,C)) } by A7, Th9, ORDINAL1: 29;

            hence thesis by A4, A6;

          end;

          hence thesis by A8;

        end;

        hence thesis by A4;

      end;

      for B holds OnP[B] from ORDINAL1:sch 2( A1);

      hence thesis;

    end;

    theorem :: CLASSES1:17

    

     Th17: ex A st ( Tarski-Class (X,A)) = ( Tarski-Class (X,( succ A)))

    proof

      assume

       A1: for A holds ( Tarski-Class (X,A)) <> ( Tarski-Class (X,( succ A)));

      defpred P[ object] means ex A st $1 in ( Tarski-Class (X,A));

      consider Z such that

       A2: for x be object holds x in Z iff x in ( Tarski-Class X) & P[x] from XBOOLE_0:sch 1;

      defpred P[ object, object] means ex A st $2 = A & $1 in ( Tarski-Class (X,( succ A))) & not $1 in ( Tarski-Class (X,A));

      

       A3: for x,y,z be object st P[x, y] & P[x, z] holds y = z

      proof

        let x,y,z be object;

        given A such that

         A4: y = A and

         A5: x in ( Tarski-Class (X,( succ A))) and

         A6: not x in ( Tarski-Class (X,A));

        given B such that

         A7: z = B and

         A8: x in ( Tarski-Class (X,( succ B))) and

         A9: not x in ( Tarski-Class (X,B));

        assume

         A10: y <> z;

        A c= B or B c= A;

        then

         A11: A c< B or B c< A by A4, A7, A10;

        now

          assume A c< B;

          then ( succ A) c= B by ORDINAL1: 11, ORDINAL1: 21;

          then ( Tarski-Class (X,( succ A))) c= ( Tarski-Class (X,B)) by Th16;

          hence contradiction by A5, A9;

        end;

        then ( succ B) c= A by ORDINAL1: 11, ORDINAL1: 21, A11;

        then ( Tarski-Class (X,( succ B))) c= ( Tarski-Class (X,A)) by Th16;

        hence contradiction by A6, A8;

      end;

      consider Y such that

       A12: for x be object holds x in Y iff ex y be object st y in Z & P[y, x] from TARSKI:sch 1( A3);

      now

        let A;

        

         A13: ( Tarski-Class (X,A)) c= ( Tarski-Class (X,( succ A))) by Th15;

        consider x be object such that

         A14: not (x in ( Tarski-Class (X,A)) iff x in ( Tarski-Class (X,( succ A)))) by A1, TARSKI: 2;

        x in Z by A2, A14;

        hence A in Y by A12, A13, A14;

      end;

      hence contradiction by ORDINAL1: 26;

    end;

    theorem :: CLASSES1:18

    

     Th18: ( Tarski-Class (X,A)) = ( Tarski-Class (X,( succ A))) implies ( Tarski-Class (X,A)) = ( Tarski-Class X)

    proof

      assume

       A1: ( Tarski-Class (X,A)) = ( Tarski-Class (X,( succ A)));

       {} c= A;

      then

       A2: ( Tarski-Class (X, {} )) c= ( Tarski-Class (X,A)) by Th16;

      

       A3: ( Tarski-Class (X, {} )) = {X} & X in {X} by Lm1, TARSKI:def 1;

      ( Tarski-Class (X,A)) is_Tarski-Class_of X

      proof

        thus X in ( Tarski-Class (X,A)) by A2, A3;

        

         A4: ( Tarski-Class (X,( succ A))) = (({ u : ex v st v in ( Tarski-Class (X,A)) & u c= v } \/ { ( bool v) : v in ( Tarski-Class (X,A)) }) \/ (( bool ( Tarski-Class (X,A))) /\ ( Tarski-Class X))) by Lm1;

        ( Tarski-Class X) is_Tarski-Class_of X by Def4;

        then

         A5: ( Tarski-Class X) is Tarski;

        thus for Z,Y be set st Z in ( Tarski-Class (X,A)) & Y c= Z holds Y in ( Tarski-Class (X,A))

        proof

          let Z,Y be set;

          assume

           A6: Z in ( Tarski-Class (X,A)) & Y c= Z;

          ( Tarski-Class X) is_Tarski-Class_of X by Def4;

          then ( Tarski-Class X) is Tarski;

          then ( Tarski-Class X) is subset-closed;

          then

          reconsider y = Y as Element of ( Tarski-Class X) by A6;

          ex v st v in ( Tarski-Class (X,A)) & y c= v by A6;

          then Y in { u : ex v st v in ( Tarski-Class (X,A)) & u c= v };

          then Y in ({ u : ex v st v in ( Tarski-Class (X,A)) & u c= v } \/ { ( bool v) : v in ( Tarski-Class (X,A)) }) by XBOOLE_0:def 3;

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

        end;

        thus Y in ( Tarski-Class (X,A)) implies ( bool Y) in ( Tarski-Class (X,A))

        proof

          assume Y in ( Tarski-Class (X,A));

          then ( bool Y) in { ( bool u) : u in ( Tarski-Class (X,A)) };

          then ( bool Y) in ({ u : ex v st v in ( Tarski-Class (X,A)) & u c= v } \/ { ( bool v) : v in ( Tarski-Class (X,A)) }) by XBOOLE_0:def 3;

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

        end;

        let Y;

        assume that

         A7: Y c= ( Tarski-Class (X,A)) and

         A8: not (Y,( Tarski-Class (X,A))) are_equipotent ;

        Y c= ( Tarski-Class X) by A7, XBOOLE_1: 1;

        then (Y,( Tarski-Class X)) are_equipotent or Y in ( Tarski-Class X) by A5;

        hence thesis by A1, A7, A8, Th10, CARD_1: 24;

      end;

      hence ( Tarski-Class (X,A)) c= ( Tarski-Class X) & ( Tarski-Class X) c= ( Tarski-Class (X,A)) by Def4;

    end;

    theorem :: CLASSES1:19

    

     Th19: ex A st ( Tarski-Class (X,A)) = ( Tarski-Class X)

    proof

      consider A such that

       A1: ( Tarski-Class (X,A)) = ( Tarski-Class (X,( succ A))) by Th17;

      take A;

      thus thesis by A1, Th18;

    end;

    theorem :: CLASSES1:20

    ex A st ( Tarski-Class (X,A)) = ( Tarski-Class X) & for B st B in A holds ( Tarski-Class (X,B)) <> ( Tarski-Class X)

    proof

      defpred P[ Ordinal] means ( Tarski-Class (X,$1)) = ( Tarski-Class X);

      

       A1: ex A st P[A] by Th19;

      consider A such that

       A2: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A1);

      take A;

      thus ( Tarski-Class (X,A)) = ( Tarski-Class X) by A2;

      let B;

      assume B in A;

      hence thesis by A2, ORDINAL1: 5;

    end;

    theorem :: CLASSES1:21

    Y <> X & Y in ( Tarski-Class X) implies ex A st not Y in ( Tarski-Class (X,A)) & Y in ( Tarski-Class (X,( succ A)))

    proof

      assume that

       A1: Y <> X and

       A2: Y in ( Tarski-Class X);

      defpred P[ Ordinal] means Y in ( Tarski-Class (X,$1));

      ex A st ( Tarski-Class (X,A)) = ( Tarski-Class X) by Th19;

      then

       A3: ex A st P[A] by A2;

      consider A such that

       A4: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A3);

      

       A5: not Y in {X} by A1, TARSKI:def 1;

      

       A6: ( Tarski-Class (X, {} )) = {X} by Lm1;

      now

        assume A is limit_ordinal;

        then ex B st B in A & Y in ( Tarski-Class (X,B)) by A4, A5, A6, Th13;

        hence contradiction by A4, ORDINAL1: 5;

      end;

      then

      consider B such that

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

      take B;

       not A c= B by A7, ORDINAL1: 5, ORDINAL1: 6;

      hence thesis by A4, A7;

    end;

    theorem :: CLASSES1:22

    

     Th22: X is epsilon-transitive implies for A st A <> {} holds ( Tarski-Class (X,A)) is epsilon-transitive

    proof

      assume

       A1: Y in X implies Y c= X;

      defpred OnP[ Ordinal] means $1 <> {} implies ( Tarski-Class (X,$1)) is epsilon-transitive;

      

       A2: for A st for B st B in A holds OnP[B] holds OnP[A]

      proof

        let A such that

         A3: for B st B in A holds OnP[B] and

         A4: A <> {} ;

        let Y such that

         A5: Y in ( Tarski-Class (X,A));

         A6:

        now

          given B such that

           A7: A = ( succ B);

          

           A8: B c= A by ORDINAL1: 6, ORDINAL1:def 2, A7;

          

           A9: OnP[B] by A3, A7, ORDINAL1: 6;

          

           A10: ( Tarski-Class (X,B)) c= ( Tarski-Class (X,A)) by A8, Th16;

          now

            assume not Y c= ( Tarski-Class (X,B));

            then

            consider Z such that

             A11: Z in ( Tarski-Class (X,B)) and

             A12: Y c= Z or Y = ( bool Z) by A5, A7, Th10;

            

             A13: Y = ( bool Z) implies thesis by A7, A11, Th10;

            now

              assume

               A14: Y c= Z;

              thus thesis

              proof

                let x be object;

                reconsider xx = x as set by TARSKI: 1;

                assume

                 A15: x in Y;

                then

                 A16: x in Z by A14;

                 A17:

                now

                  assume B = {} ;

                  then ( Tarski-Class (X,B)) = {X} by Lm1;

                  then Z = X by A11, TARSKI:def 1;

                  hence thesis by A7, A11, Th10, A1, A14, A15;

                end;

                now

                  assume B <> {} ;

                  then Z c= ( Tarski-Class (X,B)) by A9, A11, ORDINAL1:def 2;

                  then x in ( Tarski-Class (X,B)) by A16;

                  hence thesis by A10;

                end;

                hence thesis by A17;

              end;

            end;

            hence thesis by A12, A13;

          end;

          hence thesis by A10;

        end;

        now

          assume

           A18: for B holds A <> ( succ B);

          then A is limit_ordinal by ORDINAL1: 29;

          then

          consider B such that

           A19: B in A and

           A20: Y in ( Tarski-Class (X,B)) by A4, A5, Th13;

          

           A21: ( succ B) <> A by A18;

          

           A22: ( Tarski-Class (X,B)) c= ( Tarski-Class (X,( succ B))) by Th15;

          

           A23: ( succ B) c< A by A19, ORDINAL1: 21, A21;

          

           A24: ( Tarski-Class (X,( succ B))) c= ( Tarski-Class (X,A)) by A19, ORDINAL1: 21, Th16;

          ( Tarski-Class (X,( succ B))) is epsilon-transitive by A3, A23, ORDINAL1: 11;

          then Y c= ( Tarski-Class (X,( succ B))) by A20, A22;

          hence thesis by A24;

        end;

        hence thesis by A6;

      end;

      thus for A holds OnP[A] from ORDINAL1:sch 2( A2);

    end;

    theorem :: CLASSES1:23

    

     Th23: X is epsilon-transitive implies ( Tarski-Class X) is epsilon-transitive

    proof

      consider A such that

       A1: ( Tarski-Class (X,A)) = ( Tarski-Class X) by Th19;

      ( Tarski-Class (X,A)) c= ( Tarski-Class (X,( succ A))) by Th15;

      then

       A2: ( Tarski-Class (X,A)) = ( Tarski-Class (X,( succ A))) by A1;

      assume X is epsilon-transitive;

      hence thesis by A1, A2, Th22;

    end;

    theorem :: CLASSES1:24

    

     Th24: Y in ( Tarski-Class X) implies ( card Y) in ( card ( Tarski-Class X))

    proof

      assume

       A1: Y in ( Tarski-Class X);

      ( bool Y) c= ( Tarski-Class X) by A1, Th3;

      then ( card Y) in ( card ( bool Y)) & ( card ( bool Y)) c= ( card ( Tarski-Class X)) by CARD_1: 11, CARD_1: 14;

      hence thesis;

    end;

    theorem :: CLASSES1:25

    

     Th25: Y in ( Tarski-Class X) implies not (Y,( Tarski-Class X)) are_equipotent

    proof

      assume Y in ( Tarski-Class X);

      then ( card Y) in ( card ( Tarski-Class X)) by Th24;

      then ( card Y) <> ( card ( Tarski-Class X));

      hence thesis by CARD_1: 5;

    end;

    theorem :: CLASSES1:26

    

     Th26: (x in ( Tarski-Class X) implies {x} in ( Tarski-Class X)) & (x in ( Tarski-Class X) & y in ( Tarski-Class X) implies {x, y} in ( Tarski-Class X))

    proof

      now

        assume x in ( Tarski-Class X);

        then ( bool x) in ( Tarski-Class X) by Th4;

        hence {x} in ( Tarski-Class X) by Th3, ZFMISC_1: 68;

      end;

      assume that

       A1: x in ( Tarski-Class X) and

       A2: y in ( Tarski-Class X);

      

       A3: {x} in ( Tarski-Class X) by Z1, A1;

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

      then

       A4: not ( { {} , {x}},( Tarski-Class X)) are_equipotent by A3, Th4, Th25;

      now

        assume

         A5: x <> y;

        ( { {} , {x}}, {x, y}) are_equipotent

        proof

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

          deffunc f( object) = x;

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

          take f;

          thus f is one-to-one

          proof

            let x1,x2 be object;

            assume that

             A7: x1 in ( dom f) and

             A8: x2 in ( dom f);

            

             A9: x2 = {} or x2 = {x} by A6, A8, TARSKI:def 2;

            

             A10: x1 = {} implies (f . x1) = x by A6, A7;

            x1 <> {} implies (f . x1) = y by A6, A7;

            hence thesis by A5, A6, A7, A8, A9, A10, TARSKI:def 2;

          end;

          thus ( dom f) = { {} , {x}} by A6;

          thus ( rng f) c= {x, y}

          proof

            let z be object;

            assume z in ( rng f);

            then ex u be object st u in ( dom f) & z = (f . u) by FUNCT_1:def 3;

            then z = x or z = y by A6;

            hence thesis by TARSKI:def 2;

          end;

          let z be object;

          assume z in {x, y};

          then

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

          

           A12: {} in ( dom f) by A6, TARSKI:def 2;

          

           A13: {x} in ( dom f) by A6, TARSKI:def 2;

          

           A14: (f . {} ) = x by A6, A12;

          (f . {x}) = y by A6, A13;

          hence thesis by A11, A12, A13, A14, FUNCT_1:def 3;

        end;

        then

         A15: not ( {x, y},( Tarski-Class X)) are_equipotent by A4, WELLORD2: 15;

         {x, y} c= ( Tarski-Class X) by A1, A2, ZFMISC_1: 32;

        hence thesis by A15, Th5;

      end;

      hence thesis by A3, ENUMSET1: 29;

    end;

    theorem :: CLASSES1:27

    

     Th27: x in ( Tarski-Class X) & y in ( Tarski-Class X) implies [x, y] in ( Tarski-Class X)

    proof

      assume x in ( Tarski-Class X) & y in ( Tarski-Class X);

      then {x, y} in ( Tarski-Class X) & {x} in ( Tarski-Class X) by Th26;

      hence thesis by Th26;

    end;

    theorem :: CLASSES1:28

    Y c= ( Tarski-Class X) & Z c= ( Tarski-Class X) implies [:Y, Z:] c= ( Tarski-Class X)

    proof

      assume

       A1: Y c= ( Tarski-Class X) & Z c= ( Tarski-Class X);

      let x,y be object;

      assume [x, y] in [:Y, Z:];

      then x in Y & y in Z by ZFMISC_1: 87;

      hence thesis by A1, Th27;

    end;

    definition

      let A;

      :: CLASSES1:def6

      func Rank (A) -> set means

      : Def6: ex L st it = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = {} & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = ( bool (L . C))) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = ( union ( rng (L | C)));

      correctness

      proof

        deffunc C( Ordinal, set) = ( bool $2);

        deffunc D( Ordinal, Sequence) = ( union ( rng $2));

        (ex x be object, L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = {} & (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 ) = {} & (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 ) = {} & (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 F( Ordinal) = ( Rank $1);

     Lm2:

    now

      deffunc C( Ordinal, set) = ( bool $2);

      deffunc D( Ordinal, Sequence) = ( union ( rng $2));

      

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

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

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

      thus A <> 0 & A is limit_ordinal & ( dom L) = A & (for B st B in A holds (L . B) = ( Rank B)) implies ( Rank A) = ( union ( rng L))

      proof

        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) = F(B);

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

      end;

    end;

    theorem :: CLASSES1:29

    ( Rank {} ) = {} by Lm2;

    theorem :: CLASSES1:30

    ( Rank ( succ A)) = ( bool ( Rank A)) by Lm2;

    theorem :: CLASSES1:31

    

     Th31: A <> {} & A is limit_ordinal implies for x holds x in ( Rank A) iff ex B st B in A & x in ( Rank B)

    proof

      assume

       A1: A <> {} & A is limit_ordinal;

      consider L such that

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

      

       A3: ( Rank A) = ( union ( rng L)) by A1, A2, Lm2;

      let x;

      thus x in ( Rank A) implies ex B st B in A & x in ( Rank B)

      proof

        assume x in ( Rank A);

        then

        consider Y such that

         A4: x in Y and

         A5: Y in ( rng L) by A3, TARSKI:def 4;

        consider y be object such that

         A6: y in ( dom L) and

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

        reconsider y as Ordinal by A6;

        take y;

        thus thesis by A2, A4, A6, A7;

      end;

      given B such that

       A8: B in A and

       A9: x in ( Rank B);

      (L . B) = ( Rank B) by A2, A8;

      then ( Rank B) in ( rng L) by A2, A8, FUNCT_1:def 3;

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

    end;

    theorem :: CLASSES1:32

    

     Th32: X c= ( Rank A) iff X in ( Rank ( succ A))

    proof

      thus X c= ( Rank A) implies X in ( Rank ( succ A))

      proof

        assume X c= ( Rank A);

        then X in ( bool ( Rank A));

        hence thesis by Lm2;

      end;

      assume X in ( Rank ( succ A));

      then X in ( bool ( Rank A)) by Lm2;

      hence thesis;

    end;

    registration

      let A;

      cluster ( Rank A) -> epsilon-transitive;

      coherence

      proof

        defpred P[ Ordinal] means for X holds X in ( Rank $1) implies X c= ( Rank $1);

        

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

        proof

          let A such that

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

          let X such that

           A3: X in ( Rank A);

          let x be object such that

           A4: x in X;

          reconsider xx = x as set by TARSKI: 1;

           A5:

          now

            assume

             A6: A is limit_ordinal;

            then

            consider B such that

             A7: B in A and

             A8: X in ( Rank B) by A3, Lm2, Th31;

            X c= ( Rank B) by A2, A7, A8;

            hence thesis by A4, A6, A7, Th31;

          end;

          now

            assume not A is limit_ordinal;

            then

            consider B such that

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

            X c= ( Rank B) by A3, A9, Th32;

            then xx c= ( Rank B) by A2, A4, A9, ORDINAL1: 6;

            hence thesis by A9, Th32;

          end;

          hence thesis by A5;

        end;

        for A holds P[A] from ORDINAL1:sch 2( A1);

        hence P[A];

      end;

    end

    theorem :: CLASSES1:33

    ( Rank A) c= ( Rank ( succ A))

    proof

      ( Rank A) in ( bool ( Rank A)) by ZFMISC_1:def 1;

      then ( Rank A) in ( Rank ( succ A)) by Lm2;

      hence thesis by ORDINAL1:def 2;

    end;

    theorem :: CLASSES1:34

    

     Th34: ( union ( Rank A)) c= ( Rank A)

    proof

      let x be object;

      assume x in ( union ( Rank A));

      then

      consider X such that

       A1: x in X and

       A2: X in ( Rank A) by TARSKI:def 4;

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

      hence thesis by A1;

    end;

    theorem :: CLASSES1:35

    X in ( Rank A) implies ( union X) in ( Rank A)

    proof

      assume

       A1: X in ( Rank A);

       A2:

      now

        given B such that

         A3: A = ( succ B);

        

         A4: ( union X) c= ( union ( Rank B)) by ZFMISC_1: 77, A1, A3, Th32;

        ( union ( Rank B)) c= ( Rank B) by Th34;

        hence thesis by A3, Th32, A4, XBOOLE_1: 1;

      end;

      now

        assume that

         A5: A <> {} and

         A6: for B holds A <> ( succ B);

        

         A7: A is limit_ordinal by A6, ORDINAL1: 29;

        then

        consider B such that

         A8: B in A and

         A9: X in ( Rank B) by A1, A5, Th31;

        

         A10: ( union X) c= ( union ( Rank B)) by ZFMISC_1: 77, A9, ORDINAL1:def 2;

        

         A11: ( union ( Rank B)) c= ( Rank B) by Th34;

        ( succ B) <> A by A6;

        then

         A12: ( succ B) c< A by A8, ORDINAL1: 21;

        

         A13: ( union X) in ( Rank ( succ B)) by A11, Th32, A10, XBOOLE_1: 1;

        ( succ B) in A by A12, ORDINAL1: 11;

        hence thesis by A7, A13, Th31;

      end;

      hence thesis by A1, A2, Lm2;

    end;

    theorem :: CLASSES1:36

    

     Th36: A in B iff ( Rank A) in ( Rank B)

    proof

      defpred OnP[ Ordinal, Ordinal] means $1 in $2 implies ( Rank $1) in ( Rank $2);

       A1:

      now

        let A;

        defpred P[ Ordinal] means OnP[A, $1];

        

         A2: for B st for C st C in B holds P[C] holds P[B]

        proof

          let B such that

           A3: for C st C in B holds OnP[A, C] and

           A4: A in B;

           A5:

          now

            given C such that

             A6: B = ( succ C);

            

             A7: A in C implies ( Rank A) in ( Rank C) by A3, A6, ORDINAL1: 6;

            now

              assume

               A8: not A in C;

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

              hence ( Rank A) = ( Rank C) by A4, A6, A8, ORDINAL1: 11, ORDINAL1: 22;

            end;

            then ( Rank A) c= ( Rank C) by A7, ORDINAL1:def 2;

            hence thesis by A6, Th32;

          end;

          now

            assume

             A9: for C holds B <> ( succ C);

            then

             A10: B is limit_ordinal by ORDINAL1: 29;

            

             A11: B <> ( succ A) by A9;

            ( succ A) c< B by A11, A4, ORDINAL1: 21;

            then

             A12: ( succ A) in B by ORDINAL1: 11;

            ( Rank A) in ( Rank ( succ A)) by Th32;

            hence thesis by A10, A12, Th31;

          end;

          hence thesis by A5;

        end;

        thus for B holds P[B] from ORDINAL1:sch 2( A2);

      end;

      hence OnP[A, B];

      assume that

       A13: ( Rank A) in ( Rank B) and

       A14: not A in B;

      B in A or B = A by A14, ORDINAL1: 14;

      hence contradiction by A1, A13;

    end;

    theorem :: CLASSES1:37

    

     Th37: A c= B iff ( Rank A) c= ( Rank B)

    proof

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

      proof

        

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

        assume A c= B;

        then ( Rank A) = ( Rank B) or ( Rank A) in ( Rank B) by Th36, A1, ORDINAL1: 11;

        hence thesis by ORDINAL1:def 2;

      end;

      assume that

       A2: ( Rank A) c= ( Rank B) and

       A3: not A c= B;

      B in A by A3, ORDINAL1: 16;

      hence contradiction by A2, ORDINAL1: 5, Th36;

    end;

    theorem :: CLASSES1:38

    

     Th38: A c= ( Rank A)

    proof

      defpred P[ Ordinal] means $1 c= ( Rank $1);

      

       A1: P[ 0 ] by XBOOLE_1: 2;

      

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

      proof

        assume B c= ( Rank B);

        then B in ( Rank ( succ B)) by Th32;

        then B c= ( Rank ( succ B)) & {B} c= ( Rank ( succ B)) by ORDINAL1:def 2, ZFMISC_1: 31;

        hence thesis by XBOOLE_1: 8;

      end;

      

       A3: 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 A <> 0 and

         A4: A is limit_ordinal and

         A5: for B st B in A holds B c= ( Rank B);

        let x be object;

        assume

         A6: x in A;

        then

        reconsider B = x as Ordinal;

        

         A7: B c= ( Rank B) by A5, A6;

        

         A8: ( succ B) c= A by A4, A6, ORDINAL1: 28, ORDINAL1:def 2;

        

         A9: B in ( Rank ( succ B)) by A7, Th32;

        ( Rank ( succ B)) c= ( Rank A) by A8, Th37;

        hence thesis by A9;

      end;

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

      hence thesis;

    end;

    theorem :: CLASSES1:39

    for A, X st X in ( Rank A) holds not (X,( Rank A)) are_equipotent & ( card X) in ( card ( Rank A))

    proof

      defpred OnP[ Ordinal] means for X st X in ( Rank $1) holds not (X,( Rank $1)) are_equipotent ;

      

       A1: for A st for B st B in A holds OnP[B] holds OnP[A]

      proof

        let A such that

         A2: for B st B in A holds OnP[B];

        let X;

        assume

         A3: X in ( Rank A);

         A4:

        now

          given B such that

           A5: A = ( succ B);

          

           A6: B c= A by A5, ORDINAL1: 6, ORDINAL1:def 2;

          

           A7: ( Rank ( succ B)) = ( bool ( Rank B)) by Lm2;

          then

           A8: not (( Rank B),( Rank A)) are_equipotent by A5, CARD_1: 13;

          ( Rank B) c= ( Rank A) by A6, Th37;

          hence thesis by A3, A5, A7, A8, CARD_1: 24;

        end;

        now

          assume that

           A9: A <> {} and

           A10: for B holds A <> ( succ B);

          A is limit_ordinal by A10, ORDINAL1: 29;

          then

          consider B such that

           A11: B in A and

           A12: X in ( Rank B) by A3, A9, Th31;

          

           A13: ( not (X,( Rank B)) are_equipotent ) & X c= ( Rank B) by A2, A11, A12, ORDINAL1:def 2;

          ( Rank B) c= ( Rank A) by A11, Th36, ORDINAL1:def 2;

          hence thesis by A13, CARD_1: 24;

        end;

        hence thesis by A3, A4, Lm2;

      end;

      

       A14: for A holds OnP[A] from ORDINAL1:sch 2( A1);

      let A, X;

      assume

       A15: X in ( Rank A);

      

       A16: ( card X) c= ( card ( Rank A)) by A15, CARD_1: 11, ORDINAL1:def 2;

      ( card X) <> ( card ( Rank A)) by A14, A15, CARD_1: 5;

      hence thesis by A14, A15, A16, CARD_1: 3;

    end;

    theorem :: CLASSES1:40

    X c= ( Rank A) iff ( bool X) c= ( Rank ( succ A))

    proof

      thus X c= ( Rank A) implies ( bool X) c= ( Rank ( succ A))

      proof

        assume

         A1: X c= ( Rank A);

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( bool X);

        then

         A2: xx c= ( Rank A) by A1;

        ( Rank ( succ A)) = ( bool ( Rank A)) by Lm2;

        hence thesis by A2;

      end;

      assume

       A3: ( bool X) c= ( Rank ( succ A));

      let x be object;

      assume x in X;

      then {x} c= X by ZFMISC_1: 31;

      then

       A4: {x} in ( bool X);

      ( Rank ( succ A)) = ( bool ( Rank A)) & x in {x} by Lm2, TARSKI:def 1;

      hence thesis by A3, A4;

    end;

    theorem :: CLASSES1:41

    

     Th41: X c= Y & Y in ( Rank A) implies X in ( Rank A)

    proof

      assume that

       A1: X c= Y and

       A2: Y in ( Rank A);

       A3:

      now

        given B such that

         A4: A = ( succ B);

        

         A5: ( Rank ( succ B)) = ( bool ( Rank B)) by Lm2;

        then X c= ( Rank B) by A1, A2, A4, XBOOLE_1: 1;

        hence thesis by A4, A5;

      end;

      now

        assume

         A6: for B holds A <> ( succ B);

        then

         A7: A is limit_ordinal by ORDINAL1: 29;

        then

        consider B such that

         A8: B in A and

         A9: Y in ( Rank B) by A2, Lm2, Th31;

        Y c= ( Rank B) by A9, ORDINAL1:def 2;

        then

         A10: X c= ( Rank B) by A1;

        

         A11: ( bool ( Rank B)) = ( Rank ( succ B)) by Lm2;

        ( succ B) in A by A6, A8, ORDINAL1: 28, ORDINAL1: 29;

        hence thesis by A7, A10, A11, Th31;

      end;

      hence thesis by A3;

    end;

    theorem :: CLASSES1:42

    

     Th42: X in ( Rank A) iff ( bool X) in ( Rank ( succ A))

    proof

      thus X in ( Rank A) implies ( bool X) in ( Rank ( succ A))

      proof

        assume

         A1: X in ( Rank A);

        ( bool X) c= ( Rank A) by A1, Th41;

        hence thesis by Th32;

      end;

      assume ( bool X) in ( Rank ( succ A));

      then X in ( bool X) & ( bool X) c= ( Rank A) by Th32, ZFMISC_1:def 1;

      hence thesis;

    end;

    theorem :: CLASSES1:43

    

     Th43: x in ( Rank A) iff {x} in ( Rank ( succ A))

    proof

      x in ( Rank A) iff {x} c= ( Rank A) by ZFMISC_1: 31;

      hence thesis by Th32;

    end;

    theorem :: CLASSES1:44

    

     Th44: x in ( Rank A) & y in ( Rank A) iff {x, y} in ( Rank ( succ A))

    proof

      x in ( Rank A) & y in ( Rank A) iff {x, y} c= ( Rank A) by ZFMISC_1: 32;

      hence thesis by Th32;

    end;

    theorem :: CLASSES1:45

    x in ( Rank A) & y in ( Rank A) iff [x, y] in ( Rank ( succ ( succ A)))

    proof

      

       A1: x in ( Rank A) iff {x} in ( Rank ( succ A)) by Th43;

      x in ( Rank A) & y in ( Rank A) iff {x, y} in ( Rank ( succ A)) by Th44;

      hence thesis by A1, Th44;

    end;

    theorem :: CLASSES1:46

    

     Th46: X is epsilon-transitive & (( Rank A) /\ ( Tarski-Class X)) = (( Rank ( succ A)) /\ ( Tarski-Class X)) implies ( Tarski-Class X) c= ( Rank A)

    proof

      assume that

       A1: X is epsilon-transitive and

       A2: (( Rank A) /\ ( Tarski-Class X)) = (( Rank ( succ A)) /\ ( Tarski-Class X));

      given x be object such that

       A3: x in ( Tarski-Class X) & not x in ( Rank A);

      x in (( Tarski-Class X) \ ( Rank A)) by A3, XBOOLE_0:def 5;

      then

      consider Y such that

       A4: Y in (( Tarski-Class X) \ ( Rank A)) and

       A5: not ex x be object st x in (( Tarski-Class X) \ ( Rank A)) & x in Y by TARSKI: 3;

      

       A6: Y c= ( Tarski-Class X) by A4, ORDINAL1:def 2, A1, Th23;

      Y c= ( Rank A)

      proof

        let x be object;

        assume

         A7: x in Y;

        then not x in (( Tarski-Class X) \ ( Rank A)) by A5;

        hence thesis by A6, A7, XBOOLE_0:def 5;

      end;

      then Y in ( Rank ( succ A)) by Th32;

      then

       A8: Y in (( Rank ( succ A)) /\ ( Tarski-Class X)) by A4, XBOOLE_0:def 4;

       not Y in ( Rank A) by A4, XBOOLE_0:def 5;

      hence contradiction by A2, A8, XBOOLE_0:def 4;

    end;

    theorem :: CLASSES1:47

    

     Th47: X is epsilon-transitive implies ex A st ( Tarski-Class X) c= ( Rank A)

    proof

      assume

       A1: X is epsilon-transitive;

      assume

       A2: not ( Tarski-Class X) c= ( Rank A);

      defpred P[ object] means ex A st $1 in ( Rank A);

      consider Power be set such that

       A3: for x be object holds x in Power iff x in ( Tarski-Class X) & P[x] from XBOOLE_0:sch 1;

      defpred P[ object, object] means ex A st $2 = A & not $1 in ( Rank A) & $1 in ( Rank ( succ A));

      

       A4: for x,y,z be object st P[x, y] & P[x, z] holds y = z

      proof

        let x,y,z be object;

        given A1 be Ordinal such that

         A5: y = A1 and

         A6: not x in ( Rank A1) and

         A7: x in ( Rank ( succ A1));

        given A2 be Ordinal such that

         A8: z = A2 and

         A9: not x in ( Rank A2) and

         A10: x in ( Rank ( succ A2));

        assume y <> z;

        then

         A11: A1 in A2 or A2 in A1 by A5, A8, ORDINAL1: 14;

        now

          assume ( succ A1) c= A2;

          then ( Rank ( succ A1)) c= ( Rank A2) by Th37;

          hence contradiction by A7, A9;

        end;

        then ( Rank ( succ A2)) c= ( Rank A1) by A11, Th37, ORDINAL1: 21;

        hence contradiction by A6, A10;

      end;

      consider Y such that

       A12: for x be object holds x in Y iff ex y be object st y in Power & P[y, x] from TARSKI:sch 1( A4);

      now

        let A;

        (( Rank A) /\ ( Tarski-Class X)) <> (( Rank ( succ A)) /\ ( Tarski-Class X)) by A1, A2, Th46;

        then

        consider y be object such that

         A13: not (y in (( Rank A) /\ ( Tarski-Class X)) iff y in (( Rank ( succ A)) /\ ( Tarski-Class X))) by TARSKI: 2;

        

         A14: A c= ( succ A) by ORDINAL1: 6, ORDINAL1:def 2;

        then

         A15: ( Rank A) c= ( Rank ( succ A)) by Th37;

        (( Rank A) /\ ( Tarski-Class X)) c= (( Rank ( succ A)) /\ ( Tarski-Class X)) by XBOOLE_1: 26, A14, Th37;

        then

         A16: y in ( Rank ( succ A)) by A13, XBOOLE_0:def 4;

        

         A17: y in ( Tarski-Class X) by A13, XBOOLE_0:def 4;

        then

         A18: not y in ( Rank A) by A13, A15, XBOOLE_0:def 4;

        y in Power by A3, A16, A17;

        hence A in Y by A12, A16, A18;

      end;

      hence contradiction by ORDINAL1: 26;

    end;

    theorem :: CLASSES1:48

    

     Th48: X is epsilon-transitive implies ( union X) c= X

    proof

      assume

       A1: Y in X implies Y c= X;

      let x be object;

      assume x in ( union X);

      then

      consider Y such that

       A2: x in Y and

       A3: Y in X by TARSKI:def 4;

      Y c= X by A1, A3;

      hence thesis by A2;

    end;

    theorem :: CLASSES1:49

    

     Th49: X is epsilon-transitive & Y is epsilon-transitive implies (X \/ Y) is epsilon-transitive

    proof

      assume that

       A1: (Z in X implies Z c= X) and

       A2: (Z in Y implies Z c= Y);

      let Z;

      assume Z in (X \/ Y);

      then Z in X or Z in Y by XBOOLE_0:def 3;

      then

       A3: Z c= X or Z c= Y by A1, A2;

      X c= (X \/ Y) & Y c= (X \/ Y) by XBOOLE_1: 7;

      hence thesis by A3;

    end;

    theorem :: CLASSES1:50

    X is epsilon-transitive & Y is epsilon-transitive implies (X /\ Y) is epsilon-transitive

    proof

      assume that

       A1: Z in X implies Z c= X and

       A2: Z in Y implies Z c= Y;

      let Z;

      assume

       A3: Z in (X /\ Y);

      then

       A4: Z in X by XBOOLE_0:def 4;

      

       A5: Z in Y by A3, XBOOLE_0:def 4;

      

       A6: Z c= X by A1, A4;

      Z c= Y by A2, A5;

      hence thesis by A6, XBOOLE_1: 19;

    end;

    reserve n for Element of omega ;

    deffunc f( set, set) = ( union $2);

    definition

      let X;

      :: CLASSES1:def7

      func the_transitive-closure_of X -> set means

      : Def7: for x be object holds x in it iff ex f, n st x in (f . n) & ( dom f) = omega & (f . 0 ) = X & for k be Nat holds (f . ( succ k)) = ( union (f . k));

      existence

      proof

        consider f such that

         A1: ( dom f) = omega & (f . 0 ) = X & for n be Nat holds (f . ( succ n)) = f(n,.) from ORDINAL2:sch 18;

        take UNI = ( union ( rng f));

        let x be object;

        thus x in UNI implies ex f, n st x in (f . n) & ( dom f) = omega & (f . 0 ) = X & for k be Nat holds (f . ( succ k)) = ( union (f . k))

        proof

          assume x in UNI;

          then

          consider Y such that

           A2: x in Y and

           A3: Y in ( rng f) by TARSKI:def 4;

          consider y be object such that

           A4: y in ( dom f) and

           A5: Y = (f . y) by A3, FUNCT_1:def 3;

          reconsider y as Element of omega by A1, A4;

          take f, y;

          thus thesis by A1, A2, A5;

        end;

        deffunc f( set, set) = ( union $2);

        given g, n such that

         A6: x in (g . n) and

         A7: ( dom g) = omega and

         A8: (g . 0 ) = X and

         A9: for k be Nat holds (g . ( succ k)) = f(k,.);

        

         A10: ( dom f) = omega by A1;

        

         A11: (f . 0 ) = X by A1;

        

         A12: for n be Nat holds (f . ( succ n)) = f(n,.) by A1;

        g = f from ORDINAL2:sch 20( A7, A8, A9, A10, A11, A12);

        then (g . n) in ( rng f) by A1, FUNCT_1:def 3;

        hence thesis by A6, TARSKI:def 4;

      end;

      uniqueness

      proof

        defpred P[ object] means ex f, n st $1 in (f . n) & ( dom f) = omega & (f . 0 ) = X & for k be Nat holds (f . ( succ k)) = ( union (f . k));

        let U1,U2 be set such that

         A13: for x be object holds x in U1 iff P[x] and

         A14: for x be object holds x in U2 iff P[x];

        thus U1 = U2 from XBOOLE_0:sch 2( A13, A14);

      end;

    end

    registration

      let X;

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

      coherence

      proof

        let Y;

        assume Y in ( the_transitive-closure_of X);

        then

        consider f, n such that

         A1: Y in (f . n) and

         A2: ( dom f) = omega & (f . 0 ) = X and

         A3: for k be Nat holds (f . ( succ k)) = ( union (f . k)) by Def7;

        let x be object;

        assume x in Y;

        then

         A4: x in ( union (f . n)) by A1, TARSKI:def 4;

        reconsider m = ( succ n) as Element of omega by ORDINAL1:def 12;

        x in (f . m) by A3, A4;

        hence x in ( the_transitive-closure_of X) by A2, A3, Def7;

      end;

    end

    theorem :: CLASSES1:51

    ( the_transitive-closure_of X) is epsilon-transitive;

    theorem :: CLASSES1:52

    

     Th52: X c= ( the_transitive-closure_of X)

    proof

      let x be object such that

       A1: x in X;

      consider f such that

       A2: ( dom f) = omega and

       A3: (f . 0 ) = X and

       A4: for n be Nat holds (f . ( succ n)) = f(n,.) from ORDINAL2:sch 18;

      reconsider z = 0 as Element of omega by ORDINAL1:def 12;

      x in (f . z) by A1, A3;

      hence x in ( the_transitive-closure_of X) by A2, A3, A4, Def7;

    end;

    theorem :: CLASSES1:53

    

     Th53: X c= Y & Y is epsilon-transitive implies ( the_transitive-closure_of X) c= Y

    proof

      assume that

       A1: X c= Y and

       A2: Y is epsilon-transitive;

      let x be object;

      assume x in ( the_transitive-closure_of X);

      then

      consider f, n such that

       A3: x in (f . n) and ( dom f) = omega and

       A4: (f . 0 ) = X and

       A5: for k be Nat holds (f . ( succ k)) = ( union (f . k)) by Def7;

      defpred P[ Nat] means (f . $1) c= Y;

      

       A6: P[ 0 ] by A1, A4;

      

       A7: for k be Nat st P[k] holds P[( succ k)]

      proof

        let k be Nat;

        assume (f . k) c= Y;

        then

         A8: ( union (f . k)) c= ( union Y) by ZFMISC_1: 77;

        (f . ( succ k)) = ( union (f . k)) & ( union Y) c= Y by A2, A5, Th48;

        hence thesis by A8, XBOOLE_1: 1;

      end;

       P[n] from ORDINAL2:sch 17( A6, A7);

      hence thesis by A3;

    end;

    theorem :: CLASSES1:54

    

     Th54: (for Z st X c= Z & Z is epsilon-transitive holds Y c= Z) & X c= Y & Y is epsilon-transitive implies ( the_transitive-closure_of X) = Y by Th53, Th52;

    theorem :: CLASSES1:55

    

     Th55: X is epsilon-transitive implies ( the_transitive-closure_of X) = X

    proof

      for Z st X c= Z & Z is epsilon-transitive holds X c= Z;

      hence thesis by Th54;

    end;

    theorem :: CLASSES1:56

    ( the_transitive-closure_of {} ) = {} by Th55;

    theorem :: CLASSES1:57

    ( the_transitive-closure_of A) = A by Th55;

    theorem :: CLASSES1:58

    

     Th58: X c= Y implies ( the_transitive-closure_of X) c= ( the_transitive-closure_of Y)

    proof

      assume

       A1: X c= Y;

      Y c= ( the_transitive-closure_of Y) by Th52;

      then X c= ( the_transitive-closure_of Y) by A1;

      hence thesis by Th53;

    end;

    theorem :: CLASSES1:59

    ( the_transitive-closure_of ( the_transitive-closure_of X)) = ( the_transitive-closure_of X) by Th55;

    theorem :: CLASSES1:60

    ( the_transitive-closure_of (X \/ Y)) = (( the_transitive-closure_of X) \/ ( the_transitive-closure_of Y))

    proof

      X c= ( the_transitive-closure_of X) & Y c= ( the_transitive-closure_of Y) by Th52;

      then

       A1: (X \/ Y) c= (( the_transitive-closure_of X) \/ ( the_transitive-closure_of Y)) by XBOOLE_1: 13;

      ( the_transitive-closure_of (X \/ Y)) c= ( the_transitive-closure_of (( the_transitive-closure_of X) \/ ( the_transitive-closure_of Y))) by A1, Th58;

      hence ( the_transitive-closure_of (X \/ Y)) c= (( the_transitive-closure_of X) \/ ( the_transitive-closure_of Y)) by Th49, Th55;

      ( the_transitive-closure_of X) c= ( the_transitive-closure_of (X \/ Y)) & ( the_transitive-closure_of Y) c= ( the_transitive-closure_of (X \/ Y)) by Th58, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: CLASSES1:61

    ( the_transitive-closure_of (X /\ Y)) c= (( the_transitive-closure_of X) /\ ( the_transitive-closure_of Y))

    proof

      ( the_transitive-closure_of (X /\ Y)) c= ( the_transitive-closure_of X) & ( the_transitive-closure_of (X /\ Y)) c= ( the_transitive-closure_of Y) by Th58, XBOOLE_1: 17;

      hence thesis by XBOOLE_1: 19;

    end;

    theorem :: CLASSES1:62

    

     Th62: ex A st X c= ( Rank A)

    proof

      consider A such that

       A1: ( Tarski-Class ( the_transitive-closure_of X)) c= ( Rank A) by Th47;

      take A;

      ( the_transitive-closure_of X) in ( Tarski-Class ( the_transitive-closure_of X)) by Th2;

      then X in ( Tarski-Class ( the_transitive-closure_of X)) by Th3, Th52;

      hence thesis by A1, ORDINAL1:def 2;

    end;

    definition

      let x be object;

      :: CLASSES1:def8

      func the_rank_of x -> Ordinal means

      : Def8: x in ( Rank ( succ it )) & for B st x in ( Rank ( succ B)) holds it c= B;

      existence

      proof

        defpred P[ Ordinal] means x in ( Rank ( succ $1));

        reconsider x as set by TARSKI: 1;

        consider A such that

         A1: x c= ( Rank A) by Th62;

        x in ( bool ( Rank A)) by A1;

        then x in ( Rank ( succ A)) by Lm2;

        then

         A2: ex A st P[A];

        thus ex A st P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A2);

      end;

      uniqueness ;

    end

    definition

      let X;

      :: original: the_rank_of

      redefine

      :: CLASSES1:def9

      func the_rank_of X means

      : Def9: X c= ( Rank it ) & for B st X c= ( Rank B) holds it c= B;

      compatibility

      proof

        let O be Ordinal;

        thus O = ( the_rank_of X) implies X c= ( Rank O) & for B st X c= ( Rank B) holds O c= B

        proof

          assume

           A1: O = ( the_rank_of X);

          then X in ( Rank ( succ O)) by Def8;

          then X in ( bool ( Rank O)) by Lm2;

          hence X c= ( Rank O);

          let B;

          assume X c= ( Rank B);

          then X in ( bool ( Rank B));

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

          hence O c= B by A1, Def8;

        end;

        assume X c= ( Rank O);

        then X in ( bool ( Rank O));

        then

         A2: X in ( Rank ( succ O)) by Lm2;

        assume

         A3: for B st X c= ( Rank B) holds O c= B;

        for B st X in ( Rank ( succ B)) holds O c= B

        proof

          let B;

          assume X in ( Rank ( succ B));

          then X in ( bool ( Rank B)) by Lm2;

          hence O c= B by A3;

        end;

        hence O = ( the_rank_of X) by A2, Def8;

      end;

    end

    theorem :: CLASSES1:63

    

     Th63: ( the_rank_of ( bool X)) = ( succ ( the_rank_of X))

    proof

      

       A1: X c= ( Rank ( the_rank_of X)) by Def9;

      

       A2: ( bool X) c= ( Rank ( succ ( the_rank_of X)))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( bool X);

        then

         A3: xx c= ( Rank ( the_rank_of X)) by A1;

        ( bool ( Rank ( the_rank_of X))) = ( Rank ( succ ( the_rank_of X))) by Lm2;

        hence thesis by A3;

      end;

      for A st ( bool X) c= ( Rank A) holds ( succ ( the_rank_of X)) c= A

      proof

        let A such that

         A4: ( bool X) c= ( Rank A);

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

        

         A5: X in ( bool X) by ZFMISC_1:def 1;

        then

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

        consider B such that

         A7: P[B] & for C st P[C] holds B c= C from ORDINAL1:sch 1( A6);

        now

          assume for C holds B <> ( succ C);

          then B is limit_ordinal by ORDINAL1: 29;

          then ex C st C in B & X in ( Rank C) by A7, Lm2, Th31;

          hence contradiction by A7, ORDINAL1: 5;

        end;

        then

        consider C such that

         A8: B = ( succ C);

        X c= ( Rank C) by A7, A8, Th32;

        then ( the_rank_of X) c= C by Def9;

        then

         A9: ( the_rank_of X) in B by A8, ORDINAL1: 22;

        B c= A by A4, A5, A7;

        hence thesis by A9, ORDINAL1: 21;

      end;

      hence thesis by A2, Def9;

    end;

    theorem :: CLASSES1:64

    ( the_rank_of ( Rank A)) = A

    proof

      for B st ( Rank A) c= ( Rank B) holds A c= B by Th37;

      hence thesis by Def9;

    end;

    theorem :: CLASSES1:65

    

     Th65: X c= ( Rank A) iff ( the_rank_of X) c= A

    proof

      thus X c= ( Rank A) implies ( the_rank_of X) c= A by Def9;

      assume ( the_rank_of X) c= A;

      then

       A1: ( Rank ( the_rank_of X)) c= ( Rank A) by Th37;

      X c= ( Rank ( the_rank_of X)) by Def9;

      hence thesis by A1;

    end;

    theorem :: CLASSES1:66

    

     Th66: X in ( Rank A) iff ( the_rank_of X) in A

    proof

      thus X in ( Rank A) implies ( the_rank_of X) in A

      proof

        assume X in ( Rank A);

        then ( bool X) in ( Rank ( succ A)) by Th42;

        then

         A1: ( bool X) c= ( Rank A) by Th32;

        ( the_rank_of ( bool X)) = ( succ ( the_rank_of X)) by Th63;

        then

         A2: ( the_rank_of X) in ( the_rank_of ( bool X)) by ORDINAL1: 6;

        ( the_rank_of ( bool X)) c= A by A1, Def9;

        hence thesis by A2;

      end;

      assume

       A3: ( the_rank_of X) in A;

      X c= ( Rank ( the_rank_of X)) by Def9;

      then

       A4: X in ( Rank ( succ ( the_rank_of X))) by Th32;

      ( Rank ( succ ( the_rank_of X))) c= ( Rank A) by A3, Th37, ORDINAL1: 21;

      hence thesis by A4;

    end;

    theorem :: CLASSES1:67

    X c= Y implies ( the_rank_of X) c= ( the_rank_of Y)

    proof

      assume

       A1: X c= Y;

      Y c= ( Rank ( the_rank_of Y)) by Def9;

      then X c= ( Rank ( the_rank_of Y)) by A1;

      hence thesis by Def9;

    end;

    theorem :: CLASSES1:68

    

     Th68: X in Y implies ( the_rank_of X) in ( the_rank_of Y)

    proof

      assume

       A1: X in Y;

      Y c= ( Rank ( the_rank_of Y)) by Def9;

      hence thesis by A1, Th66;

    end;

    theorem :: CLASSES1:69

    

     Th69: ( the_rank_of X) c= A iff for Y st Y in X holds ( the_rank_of Y) in A

    proof

      set R = ( the_rank_of X);

      

       A1: X c= ( Rank R) by Def9;

      thus ( the_rank_of X) c= A implies for Y st Y in X holds ( the_rank_of Y) in A by A1, Th66;

      assume

       A2: for Y st Y in X holds ( the_rank_of Y) in A;

      X c= ( Rank A)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in X;

        then ( the_rank_of xx) in A by A2;

        hence thesis by Th66;

      end;

      hence thesis by Def9;

    end;

    theorem :: CLASSES1:70

    

     Th70: A c= ( the_rank_of X) iff for B st B in A holds ex Y st Y in X & B c= ( the_rank_of Y)

    proof

      thus A c= ( the_rank_of X) implies for B st B in A holds ex Y st Y in X & B c= ( the_rank_of Y)

      proof

        assume

         A1: A c= ( the_rank_of X);

        let B;

        assume B in A;

        then not ( the_rank_of X) c= B by A1, ORDINAL1: 5;

        then not X c= ( Rank B) by Def9;

        then

         A2: (X \ ( Rank B)) <> {} by XBOOLE_1: 37;

        set x = the Element of (X \ ( Rank B));

        take x;

        

         A3: not x in ( Rank B) by A2, XBOOLE_0:def 5;

        thus x in X by A2, XBOOLE_0:def 5;

        thus thesis by ORDINAL1: 16, A3, Th66;

      end;

      assume

       A4: for B st B in A holds ex Y st Y in X & B c= ( the_rank_of Y);

      let x be object;

      assume

       A5: x in A;

      then

      reconsider x as Ordinal;

      consider Y such that

       A6: Y in X and

       A7: x c= ( the_rank_of Y) by A4, A5;

      ( the_rank_of Y) in ( the_rank_of X) by A6, Th68;

      hence thesis by A7, ORDINAL1: 12;

    end;

    theorem :: CLASSES1:71

    ( the_rank_of X) = {} iff X = {}

    proof

      thus ( the_rank_of X) = {} implies X = {}

      proof

        assume ( the_rank_of X) = {} ;

        then X c= ( Rank {} ) by Def9;

        hence thesis by Lm2;

      end;

      assume X = {} ;

      then for Y st Y in X holds ( the_rank_of Y) in {} ;

      hence ( the_rank_of X) c= {} by Th69;

      thus {} c= ( the_rank_of X);

    end;

    theorem :: CLASSES1:72

    

     Th72: ( the_rank_of X) = ( succ A) implies ex Y st Y in X & ( the_rank_of Y) = A

    proof

      assume

       A1: ( the_rank_of X) = ( succ A);

      consider Y such that

       A2: Y in X and

       A3: A c= ( the_rank_of Y) by A1, Th70, ORDINAL1: 6;

      take Y;

      ( the_rank_of Y) c= A by A1, ORDINAL1: 22, A2, Th68;

      hence thesis by A2, A3;

    end;

    theorem :: CLASSES1:73

    ( the_rank_of A) = A

    proof

      A c= ( Rank A) by Th38;

      hence ( the_rank_of A) c= A by Th65;

      defpred P[ Ordinal] means $1 c= ( the_rank_of $1);

      

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

      proof

        let A such that

         A2: for B st B in A holds B c= ( the_rank_of B);

        now

          let B such that

           A3: B in A;

          reconsider Y = B as set;

          take Y;

          thus Y in A & B c= ( the_rank_of Y) by A2, A3;

        end;

        hence thesis by Th70;

      end;

       P[B] from ORDINAL1:sch 2( A1);

      hence thesis;

    end;

    theorem :: CLASSES1:74

    ( the_rank_of ( Tarski-Class X)) <> {} & ( the_rank_of ( Tarski-Class X)) is limit_ordinal

    proof

      

       A1: ( Tarski-Class X) c= ( Rank ( the_rank_of ( Tarski-Class X))) by Def9;

      thus ( the_rank_of ( Tarski-Class X)) <> {}

      proof

        assume ( the_rank_of ( Tarski-Class X)) = {} ;

        then ( Tarski-Class X) c= {} by Def9, Lm2;

        hence contradiction;

      end;

      assume not thesis;

      then

      consider A such that

       A2: ( the_rank_of ( Tarski-Class X)) = ( succ A) by ORDINAL1: 29;

      consider Y such that

       A3: Y in ( Tarski-Class X) and

       A4: ( the_rank_of Y) = A by A2, Th72;

      

       A5: ( bool Y) in ( Tarski-Class X) by A3, Th4;

      

       A6: ( the_rank_of ( bool Y)) = ( succ A) by A4, Th63;

      ( bool Y) c= ( Rank A) by A1, A2, A5, Th32;

      then ( succ A) c= A by A6, Def9;

      then A in A by ORDINAL1: 21;

      hence contradiction;

    end;

    begin

    reserve e,u for set;

    scheme :: CLASSES1:sch1

    NonUniqFuncEx { X() -> set , P[ object, object] } :

ex f be Function st ( dom f) = X() & for e be object st e in X() holds P[e, (f . e)]

      provided

       A1: for e be object st e in X() holds ex u be object st P[e, u];

      per cases ;

        suppose X() = {} ;

        then

         A2: for e be object st e in X() holds ex u be object st u in {} & P[e, u];

        ex f be Function st ( dom f) = X() & ( rng f) c= {} & for e be object st e in X() holds P[e, (f . e)] from FUNCT_1:sch 6( A2);

        hence thesis;

      end;

        suppose X() <> {} ;

        then

        reconsider D = X() as non empty set;

        defpred Q[ set, Ordinal] means ex u st u in ( Rank $2) & P[$1, u];

        

         A3: for e be Element of D holds ex A st Q[e, A]

        proof

          let e be Element of D;

          consider u be object such that

           A4: P[e, u] by A1;

          reconsider u as set by TARSKI: 1;

          u c= ( Rank ( the_rank_of u)) by Def9;

          then u in ( Rank ( succ ( the_rank_of u))) by Th32;

          hence thesis by A4;

        end;

        consider F be Function such that

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

        

         A6: for e be object st e in X() holds ex u be object st u in ( Rank ( sup ( rng F))) & P[e, u]

        proof

          let e be object;

          assume

           A7: e in X();

          then

          consider A such that

           A8: A = (F . e) and

           A9: ex u st u in ( Rank A) & P[e, u] and for B st ex u st u in ( Rank B) & P[e, u] holds A c= B by A5;

          consider u such that

           A10: u in ( Rank A) & P[e, u] by A9;

          take u;

          A in ( rng F) by A5, A7, A8, FUNCT_1:def 3;

          then A in ( sup ( rng F)) by ORDINAL2: 19;

          then ( Rank A) c= ( Rank ( sup ( rng F))) by Th37, ORDINAL1:def 2;

          hence thesis by A10;

        end;

        ex f be Function st ( dom f) = X() & ( rng f) c= ( Rank ( sup ( rng F))) & for e be object st e in X() holds P[e, (f . e)] from FUNCT_1:sch 6( A6);

        hence thesis;

      end;

    end;

    definition

      let F,G be Relation;

      :: CLASSES1:def10

      pred F,G are_fiberwise_equipotent means for x be object holds ( card ( Coim (F,x))) = ( card ( Coim (G,x)));

      reflexivity ;

      symmetry ;

    end

    

     Lm3: for F be Function, x be object st not x in ( rng F) holds ( Coim (F,x)) = {}

    proof

      let F be Function, x be object;

      assume

       A1: not x in ( rng F);

      now

        assume ( rng F) meets {x};

        then ex y be object st y in ( rng F) & y in {x} by XBOOLE_0: 3;

        hence contradiction by A1, TARSKI:def 1;

      end;

      hence thesis by RELAT_1: 138;

    end;

    theorem :: CLASSES1:75

    

     Th75: for F,G be Function st (F,G) are_fiberwise_equipotent holds ( rng F) = ( rng G)

    proof

      let F,G be Function;

      assume

       A1: (F,G) are_fiberwise_equipotent ;

      thus ( rng F) c= ( rng G)

      proof

        let x be object;

        assume that

         A2: x in ( rng F) and

         A3: not x in ( rng G);

        

         A4: ( card ( Coim (F,x))) = ( card ( Coim (G,x))) by A1;

        

         A5: ex y be object st y in ( dom F) & (F . y) = x by A2, FUNCT_1:def 3;

        ( Coim (G,x)) = {} by A3, Lm3;

        then x in {x} & (F " {x}) = {} by A4, CARD_1: 5, CARD_1: 26, TARSKI:def 1;

        hence contradiction by A5, FUNCT_1:def 7;

      end;

      let x be object;

      assume that

       A6: x in ( rng G) and

       A7: not x in ( rng F);

      

       A8: ( card ( Coim (G,x))) = ( card ( Coim (F,x))) by A1;

      

       A9: ex y be object st y in ( dom G) & (G . y) = x by A6, FUNCT_1:def 3;

      ( Coim (F,x)) = {} by A7, Lm3;

      then x in {x} & ( Coim (G,x)) = {} by A8, CARD_1: 5, CARD_1: 26, TARSKI:def 1;

      hence contradiction by A9, FUNCT_1:def 7;

    end;

    theorem :: CLASSES1:76

    for F,G,H be Function st (F,G) are_fiberwise_equipotent & (F,H) are_fiberwise_equipotent holds (G,H) are_fiberwise_equipotent

    proof

      let F,G,H be Function;

      assume that

       A1: (F,G) are_fiberwise_equipotent and

       A2: (F,H) are_fiberwise_equipotent ;

      let x be object;

      

      thus ( card ( Coim (G,x))) = ( card ( Coim (F,x))) by A1

      .= ( card ( Coim (H,x))) by A2;

    end;

    theorem :: CLASSES1:77

    

     Th77: for F,G be Function holds (F,G) are_fiberwise_equipotent iff ex H be Function st ( dom H) = ( dom F) & ( rng H) = ( dom G) & H is one-to-one & F = (G * H)

    proof

      let F,G be Function;

      thus (F,G) are_fiberwise_equipotent implies ex H be Function st ( dom H) = ( dom F) & ( rng H) = ( dom G) & H is one-to-one & F = (G * H)

      proof

        assume

         A1: (F,G) are_fiberwise_equipotent ;

        defpred P[ object, object] means $2 is Function & for f be Function st $2 = f holds ( dom f) = (F " {$1}) & ( rng f) = (G " {$1}) & f is one-to-one;

        

         A2: for x be object st x in ( rng F) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in ( rng F);

          ( card ( Coim (F,x))) = ( card ( Coim (G,x))) by A1;

          then

          consider H be Function such that

           A3: H is one-to-one & ( dom H) = (F " {x}) & ( rng H) = (G " {x}) by WELLORD2:def 4, CARD_1: 5;

          take H;

          thus H is Function;

          let g be Function;

          assume g = H;

          hence thesis by A3;

        end;

        consider W be Function such that

         A4: ( dom W) = ( rng F) & for x be object st x in ( rng F) holds P[x, (W . x)] from NonUniqFuncEx( A2);

        defpred Q[ object, object] means for H be Function st H = (W . (F . $1)) holds $2 = (H . $1);

        set df = ( dom F), dg = ( dom G);

        

         A5: for x be object st x in df holds ex y be object st y in dg & Q[x, y]

        proof

          let x be object;

          assume

           A6: x in df;

          then

           A7: (F . x) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider f = (W . (F . x)) as Function by A4;

          

           A8: ( dom f) = (F " {(F . x)}) & ( rng f) = (G " {(F . x)}) by A4, A7;

          take y = (f . x);

          (F . x) in {(F . x)} by TARSKI:def 1;

          then x in (F " {(F . x)}) by A6, FUNCT_1:def 7;

          then (f . x) in (G " {(F . x)}) by A8, FUNCT_1:def 3;

          hence y in dg by FUNCT_1:def 7;

          let g be Function;

          assume g = (W . (F . x));

          hence thesis;

        end;

        consider IT be Function such that

         A9: ( dom IT) = df & ( rng IT) c= dg & for x be object st x in df holds Q[x, (IT . x)] from FUNCT_1:sch 6( A5);

        take IT;

        thus ( dom IT) = df by A9;

        ( dom G) c= ( rng IT)

        proof

          let x be object;

          assume

           A10: x in dg;

          then

           A11: (G . x) in ( rng G) by FUNCT_1:def 3;

          

           A12: ( rng F) = ( rng G) by A1, Th75;

          then

          reconsider f = (W . (G . x)) as Function by A4, A11;

          

           A13: ( dom f) = (F " {(G . x)}) by A4, A11, A12;

          

           A14: ( rng f) = (G " {(G . x)}) by A4, A11, A12;

          (G . x) in {(G . x)} by TARSKI:def 1;

          then x in ( rng f) by A10, A14, FUNCT_1:def 7;

          then

          consider z be object such that

           A15: z in ( dom f) and

           A16: (f . z) = x by FUNCT_1:def 3;

          

           A17: z in df by A13, A15, FUNCT_1:def 7;

          (F . z) in {(G . x)} by A13, A15, FUNCT_1:def 7;

          then (F . z) = (G . x) by TARSKI:def 1;

          then (IT . z) = x by A9, A16, A17;

          hence thesis by A9, A17, FUNCT_1:def 3;

        end;

        hence ( rng IT) = dg by A9;

        now

          let x,y be object;

          assume that

           A18: x in ( dom IT) and

           A19: y in ( dom IT) and

           A20: (IT . x) = (IT . y);

          

           A21: (F . x) in ( rng F) by A9, A18, FUNCT_1:def 3;

          

           A22: (F . y) in ( rng F) by A9, A19, FUNCT_1:def 3;

          then

          reconsider f1 = (W . (F . x)), f2 = (W . (F . y)) as Function by A4, A21;

          

           A23: (IT . x) = (f1 . x) & (IT . y) = (f2 . y) by A9, A18, A19;

          

           A24: ( dom f1) = (F " {(F . x)}) by A4, A21;

          

           A25: ( rng f1) = (G " {(F . x)}) by A4, A21;

          

           A26: f1 is one-to-one by A4, A21;

          

           A27: ( dom f2) = (F " {(F . y)}) by A4, A22;

          

           A28: ( rng f2) = (G " {(F . y)}) by A4, A22;

          

           A29: (F . x) in {(F . x)} by TARSKI:def 1;

          

           A30: (F . y) in {(F . y)} by TARSKI:def 1;

          

           A31: x in (F " {(F . x)}) by A9, A18, A29, FUNCT_1:def 7;

          

           A32: y in (F " {(F . y)}) by A9, A19, A30, FUNCT_1:def 7;

          

           A33: (f1 . x) in ( rng f1) by A24, A31, FUNCT_1:def 3;

          (f2 . y) in ( rng f2) by A27, A32, FUNCT_1:def 3;

          then (f1 . x) in ((G " {(F . x)}) /\ (G " {(F . y)})) by A20, A23, A25, A28, A33, XBOOLE_0:def 4;

          then (f1 . x) in (G " ( {(F . x)} /\ {(F . y)})) by FUNCT_1: 68;

          then

           A34: (G . (f1 . x)) in ( {(F . x)} /\ {(F . y)}) by FUNCT_1:def 7;

          then

           A35: (G . (f1 . x)) in {(F . x)} by XBOOLE_0:def 4;

          

           A36: (G . (f1 . x)) in {(F . y)} by A34, XBOOLE_0:def 4;

          

           A37: (G . (f1 . x)) = (F . x) by A35, TARSKI:def 1;

          (G . (f1 . x)) = (F . y) by A36, TARSKI:def 1;

          hence x = y by A20, A23, A24, A26, A31, A32, A37;

        end;

        hence IT is one-to-one;

        

         A38: ( dom (G * IT)) = df by A9, RELAT_1: 27;

        now

          let x be object;

          assume

           A39: x in df;

          then

           A40: (F . x) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider f = (W . (F . x)) as Function by A4;

          

           A41: ( dom f) = (F " {(F . x)}) & ( rng f) = (G " {(F . x)}) by A4, A40;

          (F . x) in {(F . x)} by TARSKI:def 1;

          then x in (F " {(F . x)}) by A39, FUNCT_1:def 7;

          then (f . x) in (G " {(F . x)}) by A41, FUNCT_1:def 3;

          then (G . (f . x)) in {(F . x)} by FUNCT_1:def 7;

          then

           A42: (G . (f . x)) = (F . x) by TARSKI:def 1;

          (IT . x) = (f . x) by A9, A39;

          hence (F . x) = ((G * IT) . x) by A9, A39, A42, FUNCT_1: 13;

        end;

        hence thesis by A38;

      end;

      given H be Function such that

       A43: ( dom H) = ( dom F) and

       A44: ( rng H) = ( dom G) and

       A45: H is one-to-one and

       A46: F = (G * H);

      let x be object;

      set t = (H | (F " {x}));

      

       A47: t is one-to-one by A45, FUNCT_1: 52;

      

       A48: ( dom t) = (F " {x}) by A43, RELAT_1: 62, RELAT_1: 132;

      ( rng t) = (G " {x})

      proof

        thus ( rng t) c= (G " {x})

        proof

          let z be object;

          assume z in ( rng t);

          then

          consider y be object such that

           A49: y in ( dom t) and

           A50: (t . y) = z by FUNCT_1:def 3;

          (F . y) in {x} by A48, A49, FUNCT_1:def 7;

          then

           A51: (F . y) = x by TARSKI:def 1;

          

           A52: z = (H . y) by A49, A50, FUNCT_1: 47;

          ( dom t) = (( dom H) /\ (F " {x})) by RELAT_1: 61;

          then

           A53: y in ( dom H) by A49, XBOOLE_0:def 4;

          then

           A54: z in ( dom G) by A44, A52, FUNCT_1:def 3;

          x = (G . z) by A46, A51, A52, A53, FUNCT_1: 13;

          then (G . z) in {x} by TARSKI:def 1;

          hence thesis by A54, FUNCT_1:def 7;

        end;

        let z be object;

        assume

         A55: z in (G " {x});

        then

         A56: z in ( dom G) by FUNCT_1:def 7;

        (G . z) in {x} by A55, FUNCT_1:def 7;

        then

         A57: (G . z) = x by TARSKI:def 1;

        consider y be object such that

         A58: y in ( dom H) and

         A59: (H . y) = z by A44, A56, FUNCT_1:def 3;

        (F . y) = x by A46, A57, A58, A59, FUNCT_1: 13;

        then (F . y) in {x} by TARSKI:def 1;

        then

         A60: y in ( dom t) by A43, A48, A58, FUNCT_1:def 7;

        then (t . y) in ( rng t) by FUNCT_1:def 3;

        hence thesis by A59, A60, FUNCT_1: 47;

      end;

      hence thesis by CARD_1: 5, A47, A48, WELLORD2:def 4;

    end;

    theorem :: CLASSES1:78

    

     Th78: for F,G be Function holds (F,G) are_fiberwise_equipotent iff for X be set holds ( card (F " X)) = ( card (G " X))

    proof

      let F,G be Function;

      thus (F,G) are_fiberwise_equipotent implies for X be set holds ( card (F " X)) = ( card (G " X))

      proof

        assume (F,G) are_fiberwise_equipotent ;

        then

        consider H be Function such that

         A1: ( dom H) = ( dom F) and

         A2: ( rng H) = ( dom G) and

         A3: H is one-to-one and

         A4: F = (G * H) by Th77;

        let X be set;

        set t = (H | (F " X));

        

         A5: t is one-to-one by A3, FUNCT_1: 52;

        

         A6: ( dom t) = (F " X) by A1, RELAT_1: 62, RELAT_1: 132;

        ( rng t) = (G " X)

        proof

          thus ( rng t) c= (G " X)

          proof

            let z be object;

            assume z in ( rng t);

            then

            consider y be object such that

             A7: y in ( dom t) and

             A8: (t . y) = z by FUNCT_1:def 3;

            

             A9: (F . y) in X by A6, A7, FUNCT_1:def 7;

            

             A10: z = (H . y) by A7, A8, FUNCT_1: 47;

            ( dom t) = (( dom H) /\ (F " X)) by RELAT_1: 61;

            then

             A11: y in ( dom H) by A7, XBOOLE_0:def 4;

            then

             A12: z in ( dom G) by A2, A10, FUNCT_1:def 3;

            (G . z) in X by A4, A9, A10, A11, FUNCT_1: 13;

            hence thesis by A12, FUNCT_1:def 7;

          end;

          let z be object;

          assume

           A13: z in (G " X);

          then

           A14: z in ( dom G) by FUNCT_1:def 7;

          

           A15: (G . z) in X by A13, FUNCT_1:def 7;

          consider y be object such that

           A16: y in ( dom H) and

           A17: (H . y) = z by A2, A14, FUNCT_1:def 3;

          (F . y) in X by A4, A15, A16, A17, FUNCT_1: 13;

          then

           A18: y in ( dom t) by A1, A6, A16, FUNCT_1:def 7;

          then (t . y) in ( rng t) by FUNCT_1:def 3;

          hence thesis by A17, A18, FUNCT_1: 47;

        end;

        hence thesis by CARD_1: 5, A5, A6, WELLORD2:def 4;

      end;

      assume for X be set holds ( card (F " X)) = ( card (G " X));

      hence for x be object holds ( card ( Coim (F,x))) = ( card ( Coim (G,x)));

    end;

    theorem :: CLASSES1:79

    for D be non empty set, F,G be Function st ( rng F) c= D & ( rng G) c= D & for d be Element of D holds ( card ( Coim (F,d))) = ( card ( Coim (G,d))) holds (F,G) are_fiberwise_equipotent

    proof

      let D be non empty set, F,G be Function;

      assume that

       A1: ( rng F) c= D and

       A2: ( rng G) c= D;

      assume

       A3: for d be Element of D holds ( card ( Coim (F,d))) = ( card ( Coim (G,d)));

      let x be object;

      per cases ;

        suppose not x in ( rng F);

        then

         A4: ( Coim (F,x)) = {} by Lm3;

        now

          assume

           A5: x in ( rng G);

          then

          reconsider d = x as Element of D by A2;

          ( card ( Coim (G,d))) = ( card ( Coim (F,d))) by A3;

          then

           A6: (G " {x}) = {} by A4, CARD_1: 5, CARD_1: 26;

          consider y be object such that

           A7: y in ( dom G) and

           A8: (G . y) = x by A5, FUNCT_1:def 3;

          (G . y) in {x} by A8, TARSKI:def 1;

          hence contradiction by A6, A7, FUNCT_1:def 7;

        end;

        hence thesis by A4, Lm3;

      end;

        suppose x in ( rng F);

        then

        reconsider d = x as Element of D by A1;

        ( card ( Coim (F,d))) = ( card ( Coim (G,d))) by A3;

        hence thesis;

      end;

    end;

    theorem :: CLASSES1:80

    

     Th80: for F,G be Function st ( dom F) = ( dom G) holds (F,G) are_fiberwise_equipotent iff ex P be Permutation of ( dom F) st F = (G * P)

    proof

      let F,G be Function;

      assume

       A1: ( dom F) = ( dom G);

      thus (F,G) are_fiberwise_equipotent implies ex P be Permutation of ( dom F) st F = (G * P)

      proof

        assume (F,G) are_fiberwise_equipotent ;

        then

        consider I be Function such that

         A2: ( dom I) = ( dom F) and

         A3: ( rng I) = ( dom G) and

         A4: I is one-to-one and

         A5: F = (G * I) by Th77;

        reconsider I as Function of ( dom F), ( dom F) by A1, A2, A3, FUNCT_2: 2;

        reconsider I as Permutation of ( dom F) by A1, A3, A4, FUNCT_2: 57;

        take I;

        thus thesis by A5;

      end;

      given P be Permutation of ( dom F) such that

       A6: F = (G * P);

      P is Function of ( dom F), ( dom F) & ( dom F) = {} implies ( dom F) = {} ;

      then ( rng P) = ( dom F) & ( dom P) = ( dom F) by FUNCT_2:def 1, FUNCT_2:def 3;

      hence thesis by A1, A6, Th77;

    end;

    theorem :: CLASSES1:81

    for F,G be Function st (F,G) are_fiberwise_equipotent holds ( card ( dom F)) = ( card ( dom G))

    proof

      let F,G be Function;

      assume (F,G) are_fiberwise_equipotent ;

      then ( card (F " ( rng F))) = ( card (G " ( rng F))) & ( rng F) = ( rng G) by Th75, Th78;

      

      hence ( card ( dom F)) = ( card (G " ( rng G))) by RELAT_1: 134

      .= ( card ( dom G)) by RELAT_1: 134;

    end;

    theorem :: CLASSES1:82

    for f be set, p be Relation holds for x be set st x in ( rng p) holds ( the_rank_of x) in ( the_rank_of [p, f])

    proof

      let f be set;

      let p be Relation;

      let y be set;

      assume y in ( rng p);

      then

      consider x be object such that

       A1: [x, y] in p by XTUPLE_0:def 13;

      

       A2: p in {p, f} by TARSKI:def 2;

      

       A3: {p, f} in { {p, f}, {p}} by TARSKI:def 2;

      

       A4: y in {x, y} by TARSKI:def 2;

      

       A5: {x, y} in { {x, y}, {x}} by TARSKI:def 2;

      

       A6: ( the_rank_of y) in ( the_rank_of {x, y}) by A4, Th68;

      

       A7: ( the_rank_of {x, y}) in ( the_rank_of [x, y]) by A5, Th68;

      

       A8: ( the_rank_of p) in ( the_rank_of {p, f}) by A2, Th68;

      

       A9: ( the_rank_of {p, f}) in ( the_rank_of [p, f]) by A3, Th68;

      

       A10: ( the_rank_of y) in ( the_rank_of [x, y]) by A6, A7, ORDINAL1: 10;

      

       A11: ( the_rank_of [x, y]) in ( the_rank_of p) by A1, Th68;

      

       A12: ( the_rank_of p) in ( the_rank_of [p, f]) by A8, A9, ORDINAL1: 10;

      ( the_rank_of y) in ( the_rank_of p) by A10, A11, ORDINAL1: 10;

      hence thesis by A12, ORDINAL1: 10;

    end;

    theorem :: CLASSES1:83

    for f,g,h be Function st ( dom f) = ( dom g) & ( rng f) c= ( dom h) & ( rng g) c= ( dom h) & (f,g) are_fiberwise_equipotent holds ((h * f),(h * g)) are_fiberwise_equipotent

    proof

      let f,g,h be Function such that

       A1: ( dom f) = ( dom g) and

       A2: ( rng f) c= ( dom h) and

       A3: ( rng g) c= ( dom h) and

       A4: (f,g) are_fiberwise_equipotent ;

      consider p be Permutation of ( dom f) such that

       A5: f = (g * p) by A1, A4, Th80;

      

       A6: ( dom (h * f)) = ( dom f) by A2, RELAT_1: 27;

      

       A7: ( dom (h * g)) = ( dom g) by A3, RELAT_1: 27;

      (h * f) = ((h * g) * p) by A5, RELAT_1: 36;

      hence thesis by A1, A6, A7, Th80;

    end;

    scheme :: CLASSES1:sch2

    LambdaAB { A,B() -> set , F( Element of B()) -> set } :

ex f be Function st ( dom f) = A() & for x be Element of B() st x in A() holds (f . x) = F(x);

      defpred P[ object, object] means ($1 is Element of B() implies ex x be Element of B() st x = $1 & $2 = F(x)) & ( not $1 is Element of B() implies $2 = 0 );

      

       A1: for x be object st x in A() holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in A();

        per cases ;

          suppose x is Element of B();

          then

          reconsider z = x as Element of B();

          take F(z);

          thus thesis;

        end;

          suppose not x is Element of B();

          hence thesis;

        end;

      end;

      consider f be Function such that

       A2: ( dom f) = A() and

       A3: for x be object st x in A() holds P[x, (f . x)] from NonUniqFuncEx( A1);

      take f;

      thus ( dom f) = A() by A2;

      let x be Element of B();

      assume x in A();

      then P[x, (f . x)] by A3;

      hence (f . x) = F(x);

    end;

    theorem :: CLASSES1:84

    for x,y be set holds ( the_rank_of x) in ( the_rank_of [x, y]) & ( the_rank_of y) in ( the_rank_of [x, y])

    proof

      let x,y be set;

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

      then

       A1: ( the_rank_of {x}) in ( the_rank_of { {x, y}, {x}}) by Th68;

      x in {x} by TARSKI:def 1;

      then ( the_rank_of x) in ( the_rank_of {x}) by Th68;

      hence ( the_rank_of x) in ( the_rank_of [x, y]) by A1, ORDINAL1: 10;

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

      then

       A2: ( the_rank_of {x, y}) in ( the_rank_of { {x, y}, {x}}) by Th68;

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

      then ( the_rank_of y) in ( the_rank_of {x, y}) by Th68;

      hence thesis by A2, ORDINAL1: 10;

    end;