card_1.miz



    begin

    reserve A,B,C for Ordinal,

X,X1,Y,Y1,Z for set,

a,b,b1,b2,x,y,z for object,

R for Relation,

f,g,h for Function,

k,m,n for Nat;

    definition

      let IT be object;

      :: CARD_1:def1

      attr IT is cardinal means

      : Def1: ex B st IT = B & for A st (A,B) are_equipotent holds B c= A;

    end

    registration

      cluster cardinal for set;

      existence

      proof

        set A = the Ordinal;

        defpred P[ Ordinal] means ($1,A) are_equipotent ;

        

         A1: ex A st P[A];

        consider B such that

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

        reconsider IT = B as set;

        take IT, B;

        thus thesis by A2, WELLORD2: 15;

      end;

    end

    definition

      mode Cardinal is cardinal set;

    end

    registration

      cluster cardinal -> ordinal for set;

      coherence ;

    end

    reserve M,N for Cardinal;

    ::$Canceled

    theorem :: CARD_1:2

    

     Th1: (M,N) are_equipotent implies M = N

    proof

      

       A1: ex A st M = A & for C st (C,A) are_equipotent holds A c= C by Def1;

      ex B st N = B & for C st (C,B) are_equipotent holds B c= C by Def1;

      hence thesis by A1;

    end;

    theorem :: CARD_1:3

    M in N iff M c= N & M <> N by ORDINAL1: 11, XBOOLE_0:def 8;

    theorem :: CARD_1:4

    M in N iff not N c= M by ORDINAL1: 5, ORDINAL1: 16;

    definition

      let X;

      :: CARD_1:def2

      func card X -> Cardinal means

      : Def2: (X,it ) are_equipotent ;

      existence

      proof

        defpred P[ Ordinal] means (X,$1) are_equipotent ;

        consider R such that

         A1: R well_orders X by WELLORD2: 17;

        set Q = (R |_2 X), A = ( order_type_of Q);

        Q is well-ordering by A1, WELLORD2: 16;

        then (Q,( RelIncl A)) are_isomorphic by WELLORD2:def 2;

        then

        consider f such that

         A2: f is_isomorphism_of (Q,( RelIncl A)) by WELLORD1:def 8;

        (X,A) are_equipotent

        proof

          take f;

          ( dom f) = ( field Q) & ( rng f) = ( field ( RelIncl A)) by A2, WELLORD1:def 7;

          hence thesis by A1, A2, WELLORD1:def 7, WELLORD2: 16, WELLORD2:def 1;

        end;

        then

         A3: ex A st P[A];

        consider A such that

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

        A is cardinal

        proof

          take A;

          thus A = A;

          let B;

          assume (B,A) are_equipotent ;

          hence thesis by A4, WELLORD2: 15;

        end;

        then

        reconsider M = A as Cardinal;

        take M;

        thus thesis by A4;

      end;

      uniqueness by Th1, WELLORD2: 15;

      projectivity ;

    end

    registration

      let C be Cardinal;

      reduce ( card C) to C;

      reducibility by Def2;

    end

    registration

      cluster empty -> cardinal for set;

      coherence

      proof

        let S be set;

        assume

         A1: S is empty;

        take {} ;

        thus S = {} by A1;

        let A such that (A, {} ) are_equipotent ;

        thus thesis;

      end;

    end

    registration

      let X be empty set;

      cluster ( card X) -> empty;

      coherence ;

    end

    registration

      let X be empty set;

      cluster ( card X) -> zero;

      coherence ;

    end

    registration

      let X be non empty set;

      cluster ( card X) -> non empty;

      coherence

      proof

        assume ( card X) is empty;

        then ex f st f is one-to-one & ( dom f) = X & ( rng f) = {} by Def2, WELLORD2:def 4;

        hence contradiction by RELAT_1: 42;

      end;

    end

    registration

      let X be non empty set;

      cluster ( card X) -> non zero;

      coherence ;

    end

    theorem :: CARD_1:5

    

     Th4: (X,Y) are_equipotent iff ( card X) = ( card Y)

    proof

      

       A1: (Y,( card Y)) are_equipotent by Def2;

      

       A2: (X,( card X)) are_equipotent by Def2;

      hence (X,Y) are_equipotent implies ( card X) = ( card Y) by Def2, WELLORD2: 15;

      assume ( card X) = ( card Y);

      hence thesis by A2, A1, WELLORD2: 15;

    end;

    theorem :: CARD_1:6

    

     Th5: R is well-ordering implies (( field R),( order_type_of R)) are_equipotent

    proof

      assume R is well-ordering;

      then (R,( RelIncl ( order_type_of R))) are_isomorphic by WELLORD2:def 2;

      then

      consider f such that

       A1: f is_isomorphism_of (R,( RelIncl ( order_type_of R))) by WELLORD1:def 8;

      take f;

      ( field ( RelIncl ( order_type_of R))) = ( order_type_of R) by WELLORD2:def 1;

      hence thesis by A1, WELLORD1:def 7;

    end;

    theorem :: CARD_1:7

    

     Th6: X c= M implies ( card X) c= M

    proof

      defpred P[ Ordinal] means $1 c= M & (X,$1) are_equipotent ;

      reconsider m = M as Ordinal;

      assume X c= M;

      then

       A1: ( order_type_of ( RelIncl X)) c= m & ( RelIncl X) is well-ordering by WELLORD2: 8, WELLORD2: 14;

      ( field ( RelIncl X)) = X by WELLORD2:def 1;

      then

       A2: ex A st P[A] by A1, Th5;

      consider A such that

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

      A is cardinal

      proof

        take A;

        thus A = A;

        let B;

        assume

         A4: (B,A) are_equipotent ;

        assume

         A5: not A c= B;

        then m c= B by A3, A4, WELLORD2: 15;

        hence contradiction by A3, A5;

      end;

      then

      reconsider A as Cardinal;

      ( card X) = A by A3, Def2;

      hence thesis by A3;

    end;

    theorem :: CARD_1:8

    

     Th7: ( card A) c= A

    proof

      (ex B st ( card A) = B & for C st (C,B) are_equipotent holds B c= C) & (A,( card A)) are_equipotent by Def1, Def2;

      hence thesis;

    end;

    theorem :: CARD_1:9

    X in M implies ( card X) in M by Th7, ORDINAL1: 12;

    ::$Notion-Name

    theorem :: CARD_1:10

    

     Th9: ( card X) c= ( card Y) iff ex f st f is one-to-one & ( dom f) = X & ( rng f) c= Y

    proof

      thus ( card X) c= ( card Y) implies ex f st f is one-to-one & ( dom f) = X & ( rng f) c= Y

      proof

        consider f such that

         A1: f is one-to-one and

         A2: ( dom f) = X & ( rng f) = ( card X) by Def2, WELLORD2:def 4;

        assume

         A3: ( card X) c= ( card Y);

        consider g such that

         A4: g is one-to-one and

         A5: ( dom g) = Y & ( rng g) = ( card Y) by Def2, WELLORD2:def 4;

        take h = ((g " ) * f);

        thus h is one-to-one by A1, A4;

        ( rng g) = ( dom (g " )) & ( dom g) = ( rng (g " )) by A4, FUNCT_1: 33;

        hence thesis by A3, A2, A5, RELAT_1: 26, RELAT_1: 27;

      end;

      given f such that

       A6: f is one-to-one and

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

      consider g such that

       A8: g is one-to-one and

       A9: ( dom g) = Y and

       A10: ( rng g) = ( card Y) by Def2, WELLORD2:def 4;

      

       A11: (X,( rng (g * f))) are_equipotent

      proof

        take (g * f);

        thus (g * f) is one-to-one by A6, A8;

        thus ( dom (g * f)) = X by A7, A9, RELAT_1: 27;

        thus thesis;

      end;

      

       A12: (( rng (g * f)),( card ( rng (g * f)))) are_equipotent by Def2;

      ( card ( rng (g * f))) c= ( card Y) by A10, Th6, RELAT_1: 26;

      hence thesis by A12, Def2, A11, WELLORD2: 15;

    end;

    theorem :: CARD_1:11

    

     Th10: X c= Y implies ( card X) c= ( card Y)

    proof

      assume

       A1: X c= Y;

      ex f st f is one-to-one & ( dom f) = X & ( rng f) c= Y

      proof

        take ( id X);

        thus thesis by A1, RELAT_1: 45;

      end;

      hence thesis by Th9;

    end;

    theorem :: CARD_1:12

    

     Th11: ( card X) c= ( card Y) iff ex f st ( dom f) = Y & X c= ( rng f)

    proof

      thus ( card X) c= ( card Y) implies ex f st ( dom f) = Y & X c= ( rng f)

      proof

        assume ( card X) c= ( card Y);

        then

        consider f such that

         A1: f is one-to-one and

         A2: ( dom f) = X and

         A3: ( rng f) c= Y by Th9;

        defpred P[ object, object] means $1 in ( rng f) & $2 = ((f " ) . $1) or not $1 in ( rng f) & $2 = 0 ;

        

         A4: for x be object st x in Y holds ex y be object st P[x, y]

        proof

          let x be object such that x in Y;

           not x in ( rng f) implies thesis;

          hence thesis;

        end;

        

         A5: for x,y,z be object st x in Y & P[x, y] & P[x, z] holds y = z;

        consider g such that

         A6: ( dom g) = Y & for y be object st y in Y holds P[y, (g . y)] from FUNCT_1:sch 2( A5, A4);

        take g;

        thus ( dom g) = Y by A6;

        let x be object;

        assume

         A7: x in X;

        then

         A8: (f . x) in ( rng f) by A2, FUNCT_1:def 3;

        ((f " ) . (f . x)) = x by A1, A2, A7, FUNCT_1: 34;

        then x = (g . (f . x)) by A3, A6, A8;

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

      end;

      given f such that

       A9: ( dom f) = Y and

       A10: X c= ( rng f);

      deffunc f( object) = (f " {$1});

      consider g such that

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

      per cases ;

        suppose X <> {} ;

        then

        reconsider M = ( rng g) as non empty set by A11, RELAT_1: 42;

        for Z st Z in M holds Z <> {}

        proof

          let Z;

          assume Z in M;

          then

          consider x be object such that

           A12: x in ( dom g) & Z = (g . x) by FUNCT_1:def 3;

          

           A13: x in {x} by TARSKI:def 1;

          Z = (f " {x}) & ex y be object st y in ( dom f) & x = (f . y) by A10, A11, A12, FUNCT_1:def 3;

          hence thesis by A13, FUNCT_1:def 7;

        end;

        then

        consider F be Function such that

         A14: ( dom F) = M and

         A15: for Z st Z in M holds (F . Z) in Z by FUNCT_1: 111;

        

         A16: ( dom (F * g)) = X by A11, A14, RELAT_1: 27;

        

         A17: (F * g) is one-to-one

        proof

          let x,y be object;

          assume that

           A18: x in ( dom (F * g)) and

           A19: y in ( dom (F * g)) and

           A20: ((F * g) . x) = ((F * g) . y);

          

           A21: (g . y) = (f " {y}) by A11, A16, A19;

          then (f " {y}) in M by A11, A16, A19, FUNCT_1:def 3;

          then (F . (f " {y})) in (f " {y}) by A15;

          then

           A22: (f . (F . (f " {y}))) in {y} by FUNCT_1:def 7;

          

           A23: (g . x) = (f " {x}) by A11, A16, A18;

          then (f " {x}) in M by A11, A16, A18, FUNCT_1:def 3;

          then (F . (f " {x})) in (f " {x}) by A15;

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

          then

           A24: (f . (F . (f " {x}))) = x by TARSKI:def 1;

          ((F * g) . x) = (F . (g . x)) & ((F * g) . y) = (F . (g . y)) by A11, A16, A18, A19, FUNCT_1: 13;

          hence thesis by A20, A23, A21, A22, A24, TARSKI:def 1;

        end;

        ( rng (F * g)) c= Y

        proof

          let x be object;

          assume x in ( rng (F * g));

          then

          consider y be object such that

           A25: y in ( dom (F * g)) and

           A26: x = ((F * g) . y) by FUNCT_1:def 3;

          

           A27: x = (F . (g . y)) by A11, A16, A25, A26, FUNCT_1: 13;

          

           A28: (g . y) = (f " {y}) by A11, A16, A25;

          then (f " {y}) in M by A11, A16, A25, FUNCT_1:def 3;

          then x in (f " {y}) by A15, A28, A27;

          hence thesis by A9, FUNCT_1:def 7;

        end;

        hence thesis by A16, A17, Th9;

      end;

        suppose X = {} ;

        hence thesis;

      end;

    end;

    theorem :: CARD_1:13

    

     Th12: not (X,( bool X)) are_equipotent

    proof

      given f such that f is one-to-one and

       A1: ( dom f) = X & ( rng f) = ( bool X);

      defpred P[ object] means for Y st Y = (f . $1) holds not $1 in Y;

      consider Z such that

       A2: for a be object holds a in Z iff a in X & P[a] from XBOOLE_0:sch 1;

      Z c= X by A2;

      then

      consider a be object such that

       A3: a in X and

       A4: Z = (f . a) by A1, FUNCT_1:def 3;

      ex Y st Y = (f . a) & a in Y by A2, A3, A4;

      hence contradiction by A2, A4;

    end;

    ::$Notion-Name

    theorem :: CARD_1:14

    

     Th13: ( card X) in ( card ( bool X))

    proof

      deffunc f( object) = {$1};

      consider f such that

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

      

       A2: ( rng f) c= ( bool X)

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object such that

         A3: y in ( dom f) and

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

        

         A5: {y} c= X by A1, A3, TARSKI:def 1;

        (f . y) = {y} by A1, A3;

        hence thesis by A4, A5;

      end;

      

       A6: ( card X) <> ( card ( bool X)) by Th4, Th12;

      f is one-to-one

      proof

        let x,y be object;

        assume that

         A7: x in ( dom f) & y in ( dom f) and

         A8: (f . x) = (f . y);

        (f . x) = {x} & (f . y) = {y} by A1, A7;

        hence thesis by A8, ZFMISC_1: 3;

      end;

      then ( card X) c= ( card ( bool X)) by A1, A2, Th9;

      hence thesis by A6, ORDINAL1: 11, XBOOLE_0:def 8;

    end;

    definition

      let X;

      :: CARD_1:def3

      func nextcard X -> Cardinal means

      : Def3: ( card X) in it & for M st ( card X) in M holds it c= M;

      existence

      proof

        defpred P[ Ordinal] means ex M st $1 = M & ( card X) in M;

        ( card X) in ( card ( bool X)) by Th13;

        then

         A1: ex A st P[A];

        consider A such that

         A2: P[A] and

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

        consider M such that

         A4: A = M and

         A5: ( card X) in M by A2;

        take M;

        thus ( card X) in M by A5;

        let N;

        assume ( card X) in N;

        hence thesis by A3, A4;

      end;

      uniqueness ;

    end

    theorem :: CARD_1:15

     {} in ( nextcard X)

    proof

      ( card {} ) c= ( card X) & ( card X) in ( nextcard X) by Def3;

      hence thesis by ORDINAL1: 12;

    end;

    theorem :: CARD_1:16

    

     Th15: ( card X) = ( card Y) implies ( nextcard X) = ( nextcard Y)

    proof

      assume

       A1: ( card X) = ( card Y);

      ( card X) in ( nextcard X) & for N st ( card X) in N holds ( nextcard X) c= N by Def3;

      hence thesis by A1, Def3;

    end;

    theorem :: CARD_1:17

    

     Th16: (X,Y) are_equipotent implies ( nextcard X) = ( nextcard Y)

    proof

      assume (X,Y) are_equipotent ;

      then ( card X) = ( card Y) by Th4;

      hence thesis by Th15;

    end;

    theorem :: CARD_1:18

    

     Th17: A in ( nextcard A)

    proof

      assume not A in ( nextcard A);

      then

       A1: ( card ( nextcard A)) c= ( card A) by Th10, ORDINAL1: 16;

      

       A2: ( nextcard ( card A)) = ( nextcard A) by Def2, Th16;

      

       A3: ( card ( card A)) in ( nextcard ( card A)) by Def3;

      thus contradiction by A1, A2, A3, ORDINAL1: 5;

    end;

    reserve S for Sequence;

    definition

      let M;

      :: CARD_1:def4

      attr M is limit_cardinal means not ex N st M = ( nextcard N);

    end

    definition

      let A;

      :: CARD_1:def5

      func aleph A -> set means

      : Def5: ex S st it = ( last S) & ( dom S) = ( succ A) & (S . 0 ) = ( card omega ) & (for B st ( succ B) in ( succ A) holds (S . ( succ B)) = ( nextcard (S . B))) & for B st B in ( succ A) & B <> 0 & B is limit_ordinal holds (S . B) = ( card ( sup (S | B)));

      correctness

      proof

        set B = ( card omega );

        deffunc D( Ordinal, Sequence) = ( card ( sup $2));

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

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

        hence thesis;

      end;

    end

     Lm1:

    now

      deffunc D( Ordinal, Sequence) = ( card ( sup $2));

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

      deffunc F( Ordinal) = ( aleph $1);

      

       A1: for A, x holds x = F(A) iff ex S st x = ( last S) & ( dom S) = ( succ A) & (S . 0 ) = ( card omega ) & (for C st ( succ C) in ( succ A) holds (S . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (S . C) = D(C,|) by Def5;

       F(0) = ( card omega ) from ORDINAL2:sch 8( A1);

      hence ( aleph 0 ) = ( card omega );

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

      thus A <> 0 & A is limit_ordinal implies for S st ( dom S) = A & for B st B in A holds (S . B) = ( aleph B) holds ( aleph A) = ( card ( sup S))

      proof

        assume

         A2: A <> 0 & A is limit_ordinal;

        let S such that

         A3: ( dom S) = A and

         A4: for B st B in A holds (S . B) = F(B);

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

      end;

    end;

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

    registration

      let A;

      cluster ( aleph A) -> cardinal;

      coherence

      proof

         A1:

        now

          consider S such that

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

          assume that

           A3: A <> {} and

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

          ( aleph A) = ( card ( sup S)) by A3, A2, Lm1, A4, ORDINAL1: 29;

          hence ( aleph A) is Cardinal;

        end;

        now

          given B such that

           A5: A = ( succ B);

          ( aleph A) = ( nextcard ( aleph B)) by A5, Lm1;

          hence thesis;

        end;

        hence thesis by A1, Lm1;

      end;

    end

    theorem :: CARD_1:19

    ( aleph ( succ A)) = ( nextcard ( aleph A)) by Lm1;

    theorem :: CARD_1:20

    A <> {} & A is limit_ordinal implies for S st ( dom S) = A & for B st B in A holds (S . B) = ( aleph B) holds ( aleph A) = ( card ( sup S)) by Lm1;

    theorem :: CARD_1:21

    

     Th20: A in B iff ( aleph A) in ( aleph B)

    proof

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

      

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

      proof

        let B such that

         A2: P[B];

        let A;

        

         A3: ( aleph ( succ B)) = ( nextcard ( aleph B)) by Lm1;

         A4:

        now

          assume A in B;

          then

           A5: ( aleph A) in ( aleph B) by A2;

          ( aleph B) in ( nextcard ( aleph B)) by Th17;

          hence thesis by A3, A5, ORDINAL1: 10;

        end;

        

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

        assume A in ( succ B);

        hence thesis by A3, A6, A4, Th17, ORDINAL1: 11, ORDINAL1: 22;

      end;

      

       A7: 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

         A8: B <> 0 and

         A9: B is limit_ordinal and for C st C in B holds for A st A in C holds ( aleph A) in ( aleph C);

        let A;

        consider S such that

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

        assume A in B;

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

        then

         A11: (S . ( succ A)) in ( rng S) & (S . ( succ A)) = ( aleph ( succ A)) by A10, FUNCT_1:def 3;

        ( sup ( rng S)) = ( sup S) by ORDINAL2: 26;

        then

         A12: ( aleph ( succ A)) c= ( sup S) by A11, ORDINAL1:def 2, ORDINAL2: 19;

        

         A13: ( card ( aleph ( succ A))) = ( aleph ( succ A));

        

         A14: ( aleph ( succ A)) = ( nextcard ( aleph A)) & ( aleph A) in ( nextcard ( aleph A)) by Th17, Lm1;

        ( aleph B) = ( card ( sup S)) by A8, A9, A10, Lm1;

        then ( aleph ( succ A)) c= ( aleph B) by A12, A13, Th10;

        hence thesis by A14;

      end;

      

       A15: P[ 0 ];

      

       A16: for B holds P[B] from ORDINAL2:sch 1( A15, A1, A7);

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

      assume

       A17: ( aleph A) in ( aleph B);

      then

       A18: ( aleph A) <> ( aleph B);

       not B in A by A16, A17;

      hence thesis by A18, ORDINAL1: 14;

    end;

    theorem :: CARD_1:22

    

     Th21: ( aleph A) = ( aleph B) implies A = B

    proof

      assume

       A1: ( aleph A) = ( aleph B);

       A2:

      now

        assume B in A;

        then ( aleph B) in ( aleph A) by Th20;

        hence contradiction by A1;

      end;

      now

        assume A in B;

        then ( aleph A) in ( aleph B) by Th20;

        hence contradiction by A1;

      end;

      hence thesis by A2, ORDINAL1: 14;

    end;

    theorem :: CARD_1:23

    A c= B iff ( aleph A) c= ( aleph B)

    proof

      

       A1: ( aleph A) c< ( aleph B) iff ( aleph A) <> ( aleph B) & ( aleph A) c= ( aleph B);

      A in B iff ( aleph A) in ( aleph B) by Th20;

      hence thesis by A1, Th21, ORDINAL1: 11, XBOOLE_0:def 8;

    end;

    theorem :: CARD_1:24

    X c= Y & Y c= Z & (X,Z) are_equipotent implies (X,Y) are_equipotent & (Y,Z) are_equipotent

    proof

      assume that

       A1: X c= Y & Y c= Z and

       A2: (X,Z) are_equipotent ;

      

       A3: ( card X) = ( card Z) by A2, Th4;

      ( card X) c= ( card Y) & ( card Y) c= ( card Z) by A1, Th10;

      hence thesis by A3, Th4, XBOOLE_0:def 10;

    end;

    theorem :: CARD_1:25

    ( bool Y) c= X implies ( card Y) in ( card X) & not (Y,X) are_equipotent

    proof

      assume ( bool Y) c= X;

      then ( card ( bool Y)) c= ( card X) by Th10;

      hence ( card Y) in ( card X) by Th13;

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

      hence thesis by Th4;

    end;

    theorem :: CARD_1:26

    

     Th25: (X, {} ) are_equipotent implies X = {} by RELAT_1: 42;

    theorem :: CARD_1:27

    ( card {} ) = 0 ;

    theorem :: CARD_1:28

    

     Th27: for x be object holds (X, {x}) are_equipotent iff ex x be object st X = {x}

    proof

      let x be object;

      thus (X, {x}) are_equipotent implies ex x be object st X = {x}

      proof

        assume (X, {x}) are_equipotent ;

        then

        consider f such that f is one-to-one and

         A1: ( dom f) = {x} and

         A2: ( rng f) = X by WELLORD2:def 4;

        ( rng f) = {(f . x)} by A1, FUNCT_1: 4;

        hence thesis by A2;

      end;

      given y be object such that

       A3: X = {y};

      take f = (X --> x);

      

       A4: ( dom f) = X;

      thus f is one-to-one

      proof

        let a,b be object;

        assume that

         A5: a in ( dom f) and

         A6: b in ( dom f) and (f . a) = (f . b);

        a = y by A3, A5, TARSKI:def 1;

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

      end;

      thus ( dom f) = X;

      thus ( rng f) c= {x} by FUNCOP_1: 13;

      let a be object;

      assume a in {x};

      then

       A7: a = x by TARSKI:def 1;

      

       A8: y in {y} by TARSKI:def 1;

      then (f . y) = x by A3, FUNCOP_1: 7;

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

    end;

    theorem :: CARD_1:29

    for x be object holds ( card X) = ( card {x}) iff ex x be object st X = {x} by Th4, Th27;

    theorem :: CARD_1:30

    

     Th29: for x be object holds ( card {x}) = 1

    proof

      let x be object;

      

       A1: 1 = ( succ 0 );

      1 is cardinal

      proof

        take IT = 1;

        thus 1 = IT;

        let A;

        assume (A,IT) are_equipotent ;

        then ex y be object st A = {y} by A1, Th27;

        hence thesis by A1, ZFMISC_1: 33;

      end;

      then

      reconsider M = 1 as Cardinal;

      ( {x},M) are_equipotent by A1, Th27;

      hence thesis by Def2;

    end;

    theorem :: CARD_1:31

    

     Th30: X misses X1 & Y misses Y1 & (X,Y) are_equipotent & (X1,Y1) are_equipotent implies ((X \/ X1),(Y \/ Y1)) are_equipotent

    proof

      assume that

       A1: (X /\ X1) = {} and

       A2: (Y /\ Y1) = {} ;

      given f such that

       A3: f is one-to-one and

       A4: ( dom f) = X and

       A5: ( rng f) = Y;

      given g such that

       A6: g is one-to-one and

       A7: ( dom g) = X1 and

       A8: ( rng g) = Y1;

      defpred P[ object, object] means $1 in X & $2 = (f . $1) or $1 in X1 & $2 = (g . $1);

      

       A9: for x be object st x in (X \/ X1) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in (X \/ X1);

        then x in X or x in X1 by XBOOLE_0:def 3;

        hence thesis;

      end;

      

       A10: for x,y,z be object st x in (X \/ X1) & P[x, y] & P[x, z] holds y = z by A1, XBOOLE_0:def 4;

      consider h such that

       A11: ( dom h) = (X \/ X1) and

       A12: for x be object st x in (X \/ X1) holds P[x, (h . x)] from FUNCT_1:sch 2( A10, A9);

      take h;

      thus h is one-to-one

      proof

        let x,y be object;

        assume that

         A13: x in ( dom h) and

         A14: y in ( dom h) and

         A15: (h . x) = (h . y);

        

         A16: y in X & (h . y) = (f . y) or y in X1 & (h . y) = (g . y) by A11, A12, A14;

        

         A17: x in X & (h . x) = (f . x) or x in X1 & (h . x) = (g . x) by A11, A12, A13;

         A18:

        now

          assume

           A19: y in X & x in X1;

          then (f . y) in Y & (g . x) in Y1 by A4, A5, A7, A8, FUNCT_1:def 3;

          hence contradiction by A1, A2, A15, A17, A16, A19, XBOOLE_0:def 4;

        end;

        now

          assume

           A20: x in X & y in X1;

          then (f . x) in Y & (g . y) in Y1 by A4, A5, A7, A8, FUNCT_1:def 3;

          hence contradiction by A1, A2, A15, A17, A16, A20, XBOOLE_0:def 4;

        end;

        hence thesis by A3, A4, A6, A7, A15, A17, A16, A18;

      end;

      thus ( dom h) = (X \/ X1) by A11;

      thus ( rng h) c= (Y \/ Y1)

      proof

        let x be object;

        assume x in ( rng h);

        then

        consider y be object such that

         A21: y in ( dom h) and

         A22: x = (h . y) by FUNCT_1:def 3;

        

         A23: y in X & x = (f . y) or y in X1 & x = (g . y) by A11, A12, A21, A22;

         A24:

        now

          assume y in X1;

          then x in Y1 by A1, A7, A8, A23, FUNCT_1:def 3, XBOOLE_0:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

        now

          assume y in X;

          then x in Y by A1, A4, A5, A23, FUNCT_1:def 3, XBOOLE_0:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

        hence thesis by A11, A21, A24, XBOOLE_0:def 3;

      end;

      let x be object such that

       A25: x in (Y \/ Y1);

       A26:

      now

        assume x in Y1;

        then

        consider y be object such that

         A27: y in ( dom g) and

         A28: x = (g . y) by A8, FUNCT_1:def 3;

        

         A29: y in (X \/ X1) by A7, A27, XBOOLE_0:def 3;

        then P[y, (h . y)] by A12;

        hence thesis by A1, A7, A11, A27, A28, A29, FUNCT_1:def 3, XBOOLE_0:def 4;

      end;

      now

        assume x in Y;

        then

        consider y be object such that

         A30: y in ( dom f) and

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

        

         A32: y in (X \/ X1) by A4, A30, XBOOLE_0:def 3;

        then P[y, (h . y)] by A12;

        hence thesis by A1, A4, A11, A30, A31, A32, FUNCT_1:def 3, XBOOLE_0:def 4;

      end;

      hence thesis by A25, A26, XBOOLE_0:def 3;

    end;

    theorem :: CARD_1:32

    

     Th31: x in X & y in X implies ((X \ {x}),(X \ {y})) are_equipotent

    proof

      assume that

       A1: x in X and

       A2: y in X;

      defpred P[ object, object] means $1 = y & $2 = x or $1 <> y & $1 = $2;

      

       A3: for a be object st a in (X \ {x}) holds ex b be object st P[a, b]

      proof

        let a be object such that a in (X \ {x});

        a = y implies thesis;

        hence thesis;

      end;

      

       A4: for a,b1,b2 be object st a in (X \ {x}) & P[a, b1] & P[a, b2] holds b1 = b2;

      consider f such that

       A5: ( dom f) = (X \ {x}) & for a be object st a in (X \ {x}) holds P[a, (f . a)] from FUNCT_1:sch 2( A4, A3);

      take f;

      thus f is one-to-one

      proof

        let b1,b2 be object;

        assume that

         A6: b1 in ( dom f) & b2 in ( dom f) and

         A7: (f . b1) = (f . b2) & b1 <> b2;

        

         A8: ( not b1 in {x}) & not b2 in {x} by A5, A6, XBOOLE_0:def 5;

         P[b1, (f . b1)] & P[b2, (f . b2)] by A5, A6;

        hence thesis by A7, A8, TARSKI:def 1;

      end;

      thus ( dom f) = (X \ {x}) by A5;

      thus ( rng f) c= (X \ {y})

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider a be object such that

         A9: a in ( dom f) and

         A10: z = (f . a) by FUNCT_1:def 3;

         A11:

        now

          assume

           A12: a = y;

          then ( not y in {x}) & z = x by A5, A9, A10, XBOOLE_0:def 5;

          then y <> z by TARSKI:def 1;

          then

           A13: not z in {y} by TARSKI:def 1;

          z in X by A1, A5, A9, A10, A12;

          hence thesis by A13, XBOOLE_0:def 5;

        end;

        now

          assume a <> y;

          then ( not a in {y}) & a = z by A5, A9, A10, TARSKI:def 1;

          hence thesis by A5, A9, XBOOLE_0:def 5;

        end;

        hence thesis by A11;

      end;

      let z be object;

      assume

       A14: z in (X \ {y});

      then not z in {y} by XBOOLE_0:def 5;

      then

       A15: z <> y by TARSKI:def 1;

       A16:

      now

        assume z <> x;

        then not z in {x} by TARSKI:def 1;

        then

         A17: z in (X \ {x}) by A14, XBOOLE_0:def 5;

        then z = (f . z) by A5, A15;

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

      end;

      now

        assume

         A18: z = x;

        then not y in {x} by A15, TARSKI:def 1;

        then

         A19: y in ( dom f) by A2, A5, XBOOLE_0:def 5;

        then z = (f . y) by A5, A18;

        hence thesis by A19, FUNCT_1:def 3;

      end;

      hence thesis by A16;

    end;

    theorem :: CARD_1:33

    

     Th32: X c= ( dom f) & f is one-to-one implies (X,(f .: X)) are_equipotent

    proof

      assume that

       A1: X c= ( dom f) and

       A2: f is one-to-one;

      take g = (f | X);

      thus g is one-to-one by A2, FUNCT_1: 52;

      thus ( dom g) = X by A1, RELAT_1: 62;

      thus thesis by RELAT_1: 115;

    end;

    theorem :: CARD_1:34

    

     Th33: (X,Y) are_equipotent & x in X & y in Y implies ((X \ {x}),(Y \ {y})) are_equipotent

    proof

      given f such that

       A1: f is one-to-one and

       A2: ( dom f) = X and

       A3: ( rng f) = Y;

      

       A4: ((X \ {x}),(f .: (X \ {x}))) are_equipotent by A1, A2, Th32;

      assume that

       A5: x in X and

       A6: y in Y;

      (f . x) in Y by A2, A3, A5, FUNCT_1:def 3;

      then

       A7: ((Y \ {(f . x)}),(Y \ {y})) are_equipotent by A6, Th31;

      (f .: (X \ {x})) = ((f .: X) \ ( Im (f,x))) by A1, FUNCT_1: 64

      .= (Y \ ( Im (f,x))) by A2, A3, RELAT_1: 113

      .= (Y \ {(f . x)}) by A2, A5, FUNCT_1: 59;

      hence thesis by A4, A7, WELLORD2: 15;

    end;

    theorem :: CARD_1:35

    

     Th34: (( succ X),( succ Y)) are_equipotent implies (X,Y) are_equipotent

    proof

      

       A1: X in ( succ X) & Y in ( succ Y) by ORDINAL1: 6;

      X = (( succ X) \ {X}) & Y = (( succ Y) \ {Y}) by ORDINAL1: 37;

      hence thesis by A1, Th33;

    end;

    theorem :: CARD_1:36

    

     Th35: n = {} or ex m st n = ( succ m)

    proof

      defpred P[ Nat] means $1 = {} or ex m st $1 = ( succ m);

      

       A1: for a be Nat st P[a] holds P[( succ a)];

      

       A2: P[ 0 ];

      thus P[n] from ORDINAL2:sch 17( A2, A1);

    end;

    

     Lm2: (n,m) are_equipotent implies n = m

    proof

      defpred P[ Nat] means for n st (n,$1) are_equipotent holds n = $1;

      

       A1: for a be Nat st P[a] holds P[( succ a)]

      proof

        let a be Nat such that

         A2: P[a];

        let n;

        assume

         A3: (n,( succ a)) are_equipotent ;

        per cases ;

          suppose n = {} ;

          hence thesis by A3, RELAT_1: 42;

        end;

          suppose n <> {} ;

          then ex m st n = ( succ m) by Th35;

          hence thesis by A2, A3, Th34;

        end;

      end;

      

       A4: P[ 0 ] by Th25;

       P[m] from ORDINAL2:sch 17( A4, A1);

      hence thesis;

    end;

    theorem :: CARD_1:37

    

     Th36: x in omega implies x is cardinal

    proof

      assume that

       A1: x in omega and

       A2: for B st x = B holds ex C st (C,B) are_equipotent & not B c= C;

      reconsider A = x as Ordinal by A1;

      consider B such that

       A3: (B,A) are_equipotent and

       A4: not A c= B by A2;

      B in A by A4, ORDINAL1: 16;

      then B in omega by A1, ORDINAL1: 10;

      then

      reconsider n = A, m = B as Nat by A1;

      (n,m) are_equipotent by A3;

      hence contradiction by A4, Lm2;

    end;

    registration

      cluster natural -> cardinal for number;

      correctness by Th36;

    end

    theorem :: CARD_1:38

    

     Th37: (X,Y) are_equipotent & X is finite implies Y is finite

    proof

      assume (X,Y) are_equipotent ;

      then

      consider f such that f is one-to-one and

       A1: ( dom f) = X and

       A2: ( rng f) = Y;

      given p be Function such that

       A3: ( rng p) = X and

       A4: ( dom p) in omega ;

      take (f * p);

      thus ( rng (f * p)) = Y by A1, A2, A3, RELAT_1: 28;

      thus thesis by A1, A3, A4, RELAT_1: 27;

    end;

    theorem :: CARD_1:39

    

     Th38: n is finite & ( card n) is finite

    proof

      reconsider n as Element of omega by ORDINAL1:def 12;

      ( rng ( id n)) = n & ( dom ( id n)) = n by RELAT_1: 45;

      hence thesis;

    end;

    theorem :: CARD_1:40

    ( card n) = ( card m) implies n = m;

    theorem :: CARD_1:41

    ( card n) c= ( card m) iff n c= m;

    theorem :: CARD_1:42

    ( card n) in ( card m) iff n in m;

    

     Lm3: X is finite implies ex n st (X,n) are_equipotent

    proof

      defpred P[ set] means ex n st ($1,n) are_equipotent ;

      

       A1: P[ {} ];

      

       A2: for Z, Y st Z in X & Y c= X & P[Y] holds P[(Y \/ {Z})]

      proof

        let Z, Y such that Z in X and Y c= X;

        given n such that

         A3: (Y,n) are_equipotent ;

        

         A4: not Z in Y implies thesis

        proof

          assume

           A5: not Z in Y;

          now

            set x = the Element of (Y /\ {Z});

            assume (Y /\ {Z}) <> {} ;

            then x in Y & x in {Z} by XBOOLE_0:def 4;

            hence contradiction by A5, TARSKI:def 1;

          end;

          then

           A6: Y misses {Z};

           A7:

          now

            assume n meets {n};

            then

            consider x be object such that

             A8: x in n and

             A9: x in {n} by XBOOLE_0: 3;

            

             A: x = n by A9, TARSKI:def 1;

            reconsider xx = x as set by TARSKI: 1;

             not xx in xx;

            hence contradiction by A8, A;

          end;

          take ( succ n);

          ( {Z}, {n}) are_equipotent by Th27;

          hence thesis by A3, A7, A6, Th30;

        end;

        Z in Y implies thesis

        proof

          assume

           A10: Z in Y;

          take n;

          thus thesis by A3, A10, XBOOLE_1: 12, ZFMISC_1: 31;

        end;

        hence thesis by A4;

      end;

      assume

       A11: X is finite;

      thus P[X] from FINSET_1:sch 2( A11, A1, A2);

    end;

    ::$Canceled

    theorem :: CARD_1:44

    

     Th42: ( nextcard ( card n)) = ( card ( succ n))

    proof

      reconsider sn = ( succ n) as Nat;

      for M st ( card ( card n)) in M holds ( card ( succ n)) c= M by ORDINAL1: 21;

      hence thesis by Def3, ORDINAL1: 6;

    end;

    definition

      let X be finite set;

      :: original: card

      redefine

      func card X -> Element of omega ;

      coherence

      proof

        consider n such that

         A1: (X,n) are_equipotent by Lm3;

        reconsider n as Element of omega by ORDINAL1:def 12;

        (X,n) are_equipotent by A1;

        hence thesis by Def2;

      end;

    end

    theorem :: CARD_1:45

    X is finite implies ( nextcard X) is finite

    proof

      assume X is finite;

      then

      reconsider X as finite set;

      ( card X) = ( card ( card X));

      then

       A1: ( card ( succ ( card X))) = ( nextcard ( card X)) by Th42;

      ( nextcard ( card X)) = ( nextcard X) by Def2, Th16;

      hence thesis by A1, Th38;

    end;

    scheme :: CARD_1:sch1

    CardinalInd { Sigma[ set] } :

for M holds Sigma[M]

      provided

       A1: Sigma[ {} ]

       and

       A2: for M st Sigma[M] holds Sigma[( nextcard M)]

       and

       A3: for M st M <> {} & M is limit_cardinal & for N st N in M holds Sigma[N] holds Sigma[M];

      let M;

      defpred P[ Ordinal] means $1 is Cardinal implies Sigma[$1];

      

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

      proof

        let A such that

         A5: for B st B in A holds P[B] and

         A6: A is Cardinal;

        reconsider M = A as Cardinal by A6;

         A7:

        now

          assume not M is limit_cardinal;

          then

          consider N such that

           A8: M = ( nextcard N);

          N in M by A8, Th17;

          hence Sigma[M] by A2, A5, A8;

        end;

        now

          assume

           A9: M <> {} & M is limit_cardinal;

          for N st N in M holds Sigma[N] by A5;

          hence Sigma[M] by A3, A9;

        end;

        hence thesis by A1, A7;

      end;

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

      hence thesis;

    end;

    scheme :: CARD_1:sch2

    CardinalCompInd { Sigma[ set] } :

for M holds Sigma[M]

      provided

       A1: for M st for N st N in M holds Sigma[N] holds Sigma[M];

      let M;

      defpred P[ Ordinal] means $1 is Cardinal implies Sigma[$1];

      

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

      proof

        let A such that

         A3: for B st B in A holds B is Cardinal implies Sigma[B];

        assume A is Cardinal;

        then

        reconsider M = A as Cardinal;

        for N st N in M holds Sigma[N] by A3;

        hence thesis by A1;

      end;

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

      hence thesis;

    end;

    theorem :: CARD_1:46

    

     Th44: ( aleph 0 ) = omega

    proof

      thus ( aleph 0 ) c= omega by Lm1, Th7;

      thus omega c= ( aleph 0 )

      proof

        let x be object;

        assume

         A1: x in omega ;

        then

        reconsider A = x as Ordinal;

        consider n be Element of omega such that

         A2: A = n by A1;

        ( card ( succ n)) c= ( card omega ) by Th10, ORDINAL1: 21;

        hence thesis by A2, Lm1, ORDINAL1: 6;

      end;

    end;

    registration

      cluster omega -> cardinal;

      coherence by Th44;

    end

    theorem :: CARD_1:47

    ( card omega ) = omega ;

    registration

      cluster omega -> limit_cardinal;

      coherence

      proof

        given N such that

         A1: omega = ( nextcard N);

        N in omega by A1, Th17;

        then

         A2: ( succ N) in omega by ORDINAL1:def 12;

        reconsider n = N as Element of omega by A1, Th17;

        ( nextcard ( card n)) = ( card ( succ n)) & ( card n) = n by Th42;

        hence contradiction by A1, A2;

      end;

    end

    registration

      cluster -> finite for Element of omega ;

      coherence by Th38;

    end

    registration

      cluster finite for Cardinal;

      existence

      proof

        set n = the Element of omega ;

        take n;

        thus thesis;

      end;

    end

    theorem :: CARD_1:48

    for M be finite Cardinal holds ex n st M = ( card n)

    proof

      let M be finite Cardinal;

      ( card M) = M;

      hence thesis;

    end;

    registration

      let X be finite set;

      cluster ( card X) -> finite;

      coherence ;

    end

    

     Lm4: (A,n) are_equipotent implies A = n

    proof

      defpred P[ Nat] means for A st (A,$1) are_equipotent holds A = $1;

      

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

      proof

        let n such that

         A2: P[n];

        let A;

        

         A3: n in ( succ n) & (( succ n) \ {n}) = n by ORDINAL1: 6, ORDINAL1: 37;

        assume

         A4: (A,( succ n)) are_equipotent ;

        then A <> {} by RELAT_1: 42;

        then

         A5: {} in A by ORDINAL3: 8;

        now

          

           A6: ( succ n) in omega by ORDINAL1:def 12;

          assume A is limit_ordinal;

          then

           A7: omega c= A by A5, ORDINAL1:def 11;

          ( card A) = ( card ( succ n)) by A4, Th4;

          hence contradiction by A7, Lm1, Th10, ORDINAL1: 5, A6;

        end;

        then

        consider B such that

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

        B in A & (A \ {B}) = B by A8, ORDINAL1: 6, ORDINAL1: 37;

        hence thesis by A2, A4, A8, A3, Th33;

      end;

      

       A9: P[ 0 ] by Th25;

       P[n] from ORDINAL2:sch 17( A9, A1);

      hence thesis;

    end;

    

     Lm5: A is finite iff A in omega

    proof

      thus A is finite implies A in omega

      proof

        assume A is finite;

        then

        consider n such that

         A1: (A,n) are_equipotent by Lm3;

        A = n by A1, Lm4;

        hence thesis by ORDINAL1:def 12;

      end;

      assume A in omega ;

      hence thesis;

    end;

    registration

      cluster omega -> infinite;

      coherence

      proof

         not omega in omega ;

        hence thesis by Lm5;

      end;

    end

    registration

      cluster infinite for set;

      existence

      proof

        take omega ;

        thus thesis;

      end;

    end

    registration

      let X be infinite set;

      cluster ( card X) -> infinite;

      coherence

      proof

        (X,( card X)) are_equipotent by Def2;

        hence thesis by Th37;

      end;

    end

    begin

    theorem :: CARD_1:49

    

     Th47: 1 = { 0 }

    proof

      

      thus 1 = ( succ 0 )

      .= { 0 };

    end;

    theorem :: CARD_1:50

    

     Th48: 2 = { 0 , 1}

    proof

      

      thus 2 = ( succ 1)

      .= { 0 , 1} by Th47, ENUMSET1: 1;

    end;

    theorem :: CARD_1:51

    

     Th49: 3 = { 0 , 1, 2}

    proof

      

      thus 3 = ( succ 2)

      .= { 0 , 1, 2} by Th48, ENUMSET1: 3;

    end;

    theorem :: CARD_1:52

    

     Th50: 4 = { 0 , 1, 2, 3}

    proof

      

      thus 4 = ( succ 3)

      .= { 0 , 1, 2, 3} by Th49, ENUMSET1: 6;

    end;

    theorem :: CARD_1:53

    

     Th51: 5 = { 0 , 1, 2, 3, 4}

    proof

      

      thus 5 = ( succ 4)

      .= { 0 , 1, 2, 3, 4} by Th50, ENUMSET1: 10;

    end;

    theorem :: CARD_1:54

    

     Th52: 6 = { 0 , 1, 2, 3, 4, 5}

    proof

      

      thus 6 = ( succ 5)

      .= { 0 , 1, 2, 3, 4, 5} by Th51, ENUMSET1: 15;

    end;

    theorem :: CARD_1:55

    

     Th53: 7 = { 0 , 1, 2, 3, 4, 5, 6}

    proof

      

      thus 7 = ( succ 6)

      .= { 0 , 1, 2, 3, 4, 5, 6} by Th52, ENUMSET1: 21;

    end;

    theorem :: CARD_1:56

    

     Th54: 8 = { 0 , 1, 2, 3, 4, 5, 6, 7}

    proof

      

      thus 8 = ( succ 7)

      .= { 0 , 1, 2, 3, 4, 5, 6, 7} by Th53, ENUMSET1: 28;

    end;

    theorem :: CARD_1:57

    

     Th55: 9 = { 0 , 1, 2, 3, 4, 5, 6, 7, 8}

    proof

      

      thus 9 = ( succ 8)

      .= { 0 , 1, 2, 3, 4, 5, 6, 7, 8} by Th54, ENUMSET1: 84;

    end;

    theorem :: CARD_1:58

    10 = { 0 , 1, 2, 3, 4, 5, 6, 7, 8, 9}

    proof

      

      thus 10 = ( succ 9)

      .= { 0 , 1, 2, 3, 4, 5, 6, 7, 8, 9} by Th55, ENUMSET1: 85;

    end;

    theorem :: CARD_1:59

    for f be Function st ( dom f) is infinite & f is one-to-one holds ( rng f) is infinite

    proof

      let f be Function;

      assume that

       A1: ( dom f) is infinite and

       A2: f is one-to-one;

      (( dom f),( rng f)) are_equipotent by A2;

      hence thesis by A1, Th37;

    end;

    reserve k,n,m for Nat;

    registration

      cluster non zero natural for object;

      existence

      proof

        take 1;

        thus thesis;

      end;

      cluster non zero for Nat;

      existence

      proof

        take 1;

        thus thesis;

      end;

    end

    registration

      let n be non zero natural Number;

      cluster ( Segm n) -> non empty;

      coherence

      proof

        n <> 0 ;

        hence thesis;

      end;

    end

    reserve l for Element of omega ;

    definition

      let n be natural Number;

      :: original: Segm

      redefine

      func Segm n -> Subset of omega ;

      coherence

      proof

        reconsider n as Nat by TARSKI: 1;

        n in omega by ORDINAL1:def 12;

        hence thesis by ORDINAL1: 16;

      end;

    end

    theorem :: CARD_1:60

    (A,n) are_equipotent implies A = n by Lm4;

    theorem :: CARD_1:61

    A is finite iff A in omega by Lm5;

    registration

      cluster natural -> finite for set;

      coherence ;

    end

    registration

      let A be infinite set;

      cluster ( bool A) -> infinite;

      coherence

      proof

        defpred P[ object] means ex y be object st $1 = {y};

        consider X be set such that

         A1: for x be object holds x in X iff x in ( bool A) & P[x] from XBOOLE_0:sch 1;

        for x be object holds x in ( union X) iff x in A

        proof

          let x be object;

          thus x in ( union X) implies x in A

          proof

            assume x in ( union X);

            then

            consider B be set such that

             A2: x in B and

             A3: B in X by TARSKI:def 4;

            B in ( bool A) by A1, A3;

            hence thesis by A2;

          end;

          assume x in A;

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

          then

           A4: {x} in X by A1;

          x in {x} by TARSKI:def 1;

          hence thesis by A4, TARSKI:def 4;

        end;

        then

         A5: ( union X) = A by TARSKI: 2;

        

         A6: for B be set st B in X holds B is finite

        proof

          let B be set;

          assume B in X;

          then ex y be object st B = {y} by A1;

          hence thesis;

        end;

        

         A7: X c= ( bool A) by A1;

        assume ( bool A) is finite;

        hence thesis by A5, A6, A7, FINSET_1: 7;

      end;

      let B be non empty set;

      cluster [:A, B:] -> infinite;

      coherence

      proof

        deffunc F( object) = ($1 `1 );

        consider f such that

         A8: ( dom f) = [:A, B:] and

         A9: for x be object st x in [:A, B:] holds (f . x) = F(x) from FUNCT_1:sch 3;

        for x be object holds x in ( rng f) iff x in A

        proof

          let x be object;

          thus x in ( rng f) implies x in A

          proof

            assume x in ( rng f);

            then

            consider y be object such that

             A10: y in ( dom f) and

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

            x = (y `1 ) by A8, A9, A10, A11;

            hence thesis by A8, A10, MCART_1: 10;

          end;

          set y = the Element of B;

          assume

           A12: x in A;

          then

           A13: [x, y] in ( dom f) by A8, ZFMISC_1: 87;

          (f . [x, y]) = ( [x, y] `1 ) by A9, A12, ZFMISC_1: 87

          .= x;

          hence thesis by A13, FUNCT_1:def 3;

        end;

        then ( rng f) = A by TARSKI: 2;

        then

         A14: (f .: [:A, B:]) = A by A8, RELAT_1: 113;

        assume [:A, B:] is finite;

        hence contradiction by A14;

      end;

      cluster [:B, A:] -> infinite;

      coherence

      proof

        deffunc F( object) = ($1 `2 );

        consider f such that

         A15: ( dom f) = [:B, A:] and

         A16: for x be object st x in [:B, A:] holds (f . x) = F(x) from FUNCT_1:sch 3;

        for y be object holds y in ( rng f) iff y in A

        proof

          let y be object;

          thus y in ( rng f) implies y in A

          proof

            assume y in ( rng f);

            then

            consider x be object such that

             A17: x in ( dom f) and

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

            y = (x `2 ) by A15, A16, A17, A18;

            hence thesis by A15, A17, MCART_1: 10;

          end;

          set x = the Element of B;

          assume

           A19: y in A;

          then

           A20: [x, y] in ( dom f) by A15, ZFMISC_1: 87;

          ( [x, y] `2 ) = y;

          then (f . [x, y]) = y by A16, A19, ZFMISC_1: 87;

          hence thesis by A20, FUNCT_1:def 3;

        end;

        then ( rng f) = A by TARSKI: 2;

        then

         A21: (f .: [:B, A:]) = A by A15, RELAT_1: 113;

        assume [:B, A:] is finite;

        hence contradiction by A21;

      end;

    end

    registration

      let X be infinite set;

      cluster infinite for Subset of X;

      existence

      proof

        X c= X;

        hence thesis;

      end;

    end

    registration

      cluster finite ordinal -> natural for number;

      coherence by Lm5;

    end

    theorem :: CARD_1:62

    

     Th60: for f be Function holds ( card f) = ( card ( dom f))

    proof

      let f be Function;

      (( dom f),f) are_equipotent

      proof

        deffunc F( object) = [$1, (f . $1)];

        consider g be Function such that

         A1: ( dom g) = ( dom f) and

         A2: for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        take g;

        thus g is one-to-one

        proof

          let x,y be object;

          assume that

           A3: x in ( dom g) and

           A4: y in ( dom g);

          assume (g . x) = (g . y);

          

          then [x, (f . x)] = (g . y) by A1, A2, A3

          .= [y, (f . y)] by A1, A2, A4;

          hence thesis by XTUPLE_0: 1;

        end;

        thus ( dom g) = ( dom f) by A1;

        thus ( rng g) c= f

        proof

          let i be object;

          assume i in ( rng g);

          then

          consider x be object such that

           A5: x in ( dom g) and

           A6: (g . x) = i by FUNCT_1:def 3;

          (g . x) = [x, (f . x)] by A1, A2, A5;

          hence thesis by A1, A5, A6, FUNCT_1: 1;

        end;

        let x,y be object;

        assume

         A7: [x, y] in f;

        then

         A8: x in ( dom f) by FUNCT_1: 1;

        y = (f . x) by A7, FUNCT_1: 1;

        then (g . x) = [x, y] by A2, A7, FUNCT_1: 1;

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

      end;

      hence thesis by Th4;

    end;

    registration

      let X be finite set;

      cluster ( RelIncl X) -> finite;

      coherence

      proof

        ( RelIncl X) c= [:X, X:] by WELLORD2: 23;

        hence thesis;

      end;

    end

    theorem :: CARD_1:63

    ( RelIncl X) is finite implies X is finite

    proof

      set R = ( RelIncl X);

      assume R is finite;

      then

      reconsider A = R as finite Relation;

      ( field A) is finite;

      hence thesis by WELLORD2:def 1;

    end;

    theorem :: CARD_1:64

    ( card (k --> x)) = k

    proof

      ( dom (k --> x)) = k;

      

      hence ( card (k --> x)) = ( card k) by Th60

      .= k;

    end;

    begin

    definition

      ::$Canceled

      let N be object, X be set;

      :: CARD_1:def7

      attr X is N -element means

      : Def6: ( card X) = N;

    end

    registration

      let N be Cardinal;

      cluster N -element for set;

      existence

      proof

        take N;

        thus ( card N) = N;

      end;

    end

    registration

      cluster 0 -element -> empty for set;

      coherence ;

      cluster empty -> 0 -element for set;

      coherence ;

    end

    registration

      let x be object;

      cluster {x} -> 1 -element;

      coherence

      proof

        1 = ( succ 0 );

        hence ( card {x}) = 1 by Def2, Th27;

      end;

    end

    registration

      let N be Cardinal;

      cluster N -element for Function;

      existence

      proof

        take f = (N --> { {} });

        ( card ( dom f)) = N;

        hence ( card f) = N by Th60;

      end;

    end

    registration

      let N be Cardinal;

      let f be N -element Function;

      cluster ( dom f) -> N -element;

      coherence

      proof

        ( card f) = N by Def6;

        hence ( card ( dom f)) = N by Th60;

      end;

    end

    registration

      cluster 1 -element -> trivial non empty for set;

      coherence

      proof

        let X be set;

        assume X is 1 -element;

        

        then ( card X) = 1

        .= ( card { 0 }) by Th29;

        then ex x be object st X = {x} by Th4, Th27;

        hence thesis;

      end;

      cluster trivial non empty -> 1 -element for set;

      coherence

      proof

        let X be set;

        assume X is trivial non empty;

        then ex x be object st X = {x} by ZFMISC_1: 131;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster 1 -element for Subset of X;

      existence

      proof

        take the non empty trivial Subset of X;

        thus thesis;

      end;

    end

    definition

      let X be non empty set;

      mode Singleton of X is 1 -element Subset of X;

    end

    theorem :: CARD_1:65

    

     Th63: for X be non empty set, A be Singleton of X holds ex x be Element of X st A = {x}

    proof

      let X be non empty set, A be Singleton of X;

      consider x be object such that

       A1: A = {x} by ZFMISC_1: 131;

      x in A by A1, TARSKI:def 1;

      then

      reconsider x as Element of X;

      take x;

      thus thesis by A1;

    end;

    theorem :: CARD_1:66

    

     Th64: ( card X) c= ( card Y) iff ex f st X c= (f .: Y)

    proof

      deffunc G( object) = $1;

      thus ( card X) c= ( card Y) implies ex f st X c= (f .: Y)

      proof

        assume ( card X) c= ( card Y);

        then

        consider f such that

         A1: ( dom f) = Y & X c= ( rng f) by Th11;

        take f;

        thus thesis by A1, RELAT_1: 113;

      end;

      given f such that

       A2: X c= (f .: Y);

      defpred C[ object] means $1 in ( dom f);

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

      consider g such that

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

      X c= ( rng g)

      proof

        let x be object;

        assume x in X;

        then

        consider y be object such that

         A4: y in ( dom f) and

         A5: y in Y and

         A6: x = (f . y) by A2, FUNCT_1:def 6;

        x = (g . y) by A3, A4, A5, A6;

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

      end;

      hence thesis by A3, Th11;

    end;

    theorem :: CARD_1:67

    ( card (f .: X)) c= ( card X) by Th64;

    theorem :: CARD_1:68

    ( card X) in ( card Y) implies (Y \ X) <> {}

    proof

      assume that

       A1: ( card X) in ( card Y) and

       A2: (Y \ X) = {} ;

      Y c= X by A2, XBOOLE_1: 37;

      hence contradiction by A1, Th10, ORDINAL1: 5;

    end;

    theorem :: CARD_1:69

    for x be object holds (X, [:X, {x}:]) are_equipotent & ( card X) = ( card [:X, {x}:])

    proof

      let x be object;

      deffunc f( object) = [$1, x];

      consider f such that

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

      thus (X, [:X, {x}:]) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let y,z be object;

          assume that

           A2: y in ( dom f) & z in ( dom f) and

           A3: (f . y) = (f . z);

          

           A4: ( [y, x] `1 ) = y & ( [z, x] `1 ) = z;

          (f . y) = [y, x] & (f . z) = [z, x] by A1, A2;

          hence y = z by A3, A4;

        end;

        thus ( dom f) = X by A1;

        thus ( rng f) c= [:X, {x}:]

        proof

          let y be object;

          

           A5: x in {x} by TARSKI:def 1;

          assume y in ( rng f);

          then

          consider z be object such that

           A6: z in ( dom f) and

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

          y = [z, x] by A1, A6, A7;

          hence thesis by A1, A6, A5, ZFMISC_1: 87;

        end;

        let y be object;

        assume y in [:X, {x}:];

        then

        consider y1,y2 be object such that

         A8: y1 in X and

         A9: y2 in {x} and

         A10: y = [y1, y2] by ZFMISC_1: 84;

        y2 = x by A9, TARSKI:def 1;

        then y = (f . y1) by A1, A8, A10;

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

      end;

      hence thesis by Th4;

    end;

    theorem :: CARD_1:70

    for f be Function st f is one-to-one holds ( card ( dom f)) = ( card ( rng f))

    proof

      let f be Function;

      assume

       A1: f is one-to-one;

      (f .: ( dom f)) = ( rng f) by RELAT_1: 113;

      hence thesis by A1, Th4, Th32;

    end;

    registration

      let F be non trivial set;

      let A be Singleton of F;

      cluster (F \ A) -> non empty;

      coherence

      proof

        ex x be Element of F st A = {x} by Th63;

        hence thesis by ZFMISC_1: 139;

      end;

    end

    registration

      let k be non empty Cardinal;

      cluster k -element -> non empty for set;

      coherence ;

    end

    registration

      let k be natural Number;

      cluster ( Segm k) -> finite;

      coherence ;

    end

    theorem :: CARD_1:71

    for f be Function, x,y be object holds ( card (f +~ (x,y))) = ( card f)

    proof

      let f be Function, x,y be object;

      

      thus ( card (f +~ (x,y))) = ( card ( dom (f +~ (x,y)))) by Th60

      .= ( card ( dom f)) by FUNCT_4: 99

      .= ( card f) by Th60;

    end;

    registration

      let n be non zero natural Number;

      cluster ( Segm n) -> with_zero;

      coherence by ORDINAL3: 8;

    end