:: CARD_1 semantic presentation

begin


notation
synonym  0 for  {} ;
end;

definition
let IT be set ;
attrIT is cardinal  means :Def1: :: CARD_1:def 1
 ex B being Ordinal st
( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) );
end;

:: deftheorem Def1 defines cardinal CARD_1:def_1_:_
 for IT being set holds
( IT is cardinal iff ex B being Ordinal st
( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) );

registration
cluster cardinal for set ;
existence
 ex b1 being set st b1 is cardinal
proof
set A = the Ordinal;
defpred S1[ Ordinal] means c1, the Ordinal are_equipotent ;
A1: ex A being Ordinal st S1[A] ;
consider B being Ordinal such that
A2: ( S1[B] & ( for C being Ordinal st S1[C] holds
B c= C ) ) from ORDINAL1:sch_1(A1);
reconsider IT = B as set ;
take  IT ; ::_thesis: IT is cardinal
take  B ; :: according to CARD_1:def_1 ::_thesis: ( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) )
thus  IT = B ; ::_thesis: for A being Ordinal st A,B are_equipotent holds
B c= A
let C be Ordinal; ::_thesis: ( C,B are_equipotent implies B c= C )
assume  C,B are_equipotent ; ::_thesis: B c= C
hence  B c= C by A2, WELLORD2:15; ::_thesis: verum
end;
end;

definition
mode Cardinal is cardinal set ;
end;

registration
cluster cardinal  ->  ordinal for set ;
coherence
 for b1 being set st b1 is cardinal holds
b1 is ordinal
proof
let M be set ; ::_thesis: ( M is cardinal implies M is ordinal )
assume  M is cardinal ; ::_thesis: M is ordinal
then  ex B being Ordinal st
( M = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) by Def1;
hence  M is ordinal ; ::_thesis: verum
end;
end;


theorem Th1: :: CARD_1:1
for X being set ex A being Ordinal st X,A are_equipotent
proof
let X be set ; ::_thesis: ex A being Ordinal st X,A are_equipotent
consider R being Relation such that
A1: R well_orders X by WELLORD2:17;
set Q = R |_2 X;
take A = order_type_of (R |_2 X); ::_thesis: X,A are_equipotent
 R |_2 X is well-ordering by A1, WELLORD2:16;
then  R |_2 X, RelIncl A are_isomorphic by WELLORD2:def_2;
then consider f being Function such that
A2: f is_isomorphism_of R |_2 X, RelIncl A by WELLORD1:def_8;
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = A )
 ( dom f = field (R |_2 X) & rng f = field (RelIncl A) ) by A2, WELLORD1:def_7;
hence  ( f is one-to-one & dom f = X & rng f = A ) by A1, A2, WELLORD1:def_7, WELLORD2:16, WELLORD2:def_1; ::_thesis: verum
end;

theorem Th2: :: CARD_1:2
for M, N being Cardinal holds
( M = N iff M,N are_equipotent )
proof
let M, N be Cardinal; ::_thesis: ( M = N iff M,N are_equipotent )
thus  ( M = N implies M,N are_equipotent ) ; ::_thesis: ( M,N are_equipotent implies M = N )
consider A being Ordinal such that
A1: M = A and
A2: for C being Ordinal st C,A are_equipotent holds
A c= C by Def1;
consider B being Ordinal such that
A3: N = B and
A4: for C being Ordinal st C,B are_equipotent holds
B c= C by Def1;
assume  M,N are_equipotent ; ::_thesis: M = N
then  ( B c= A & A c= B ) by A1, A2, A3, A4;
hence  M = N by A1, A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CARD_1:3
for M, N being Cardinal holds
( M in N iff ( M c= N & M <> N ) )
proof
let M, N be Cardinal; ::_thesis: ( M in N iff ( M c= N & M <> N ) )
 ( M c< N iff ( M c= N & M <> N ) ) by XBOOLE_0:def_8;
hence  ( M in N iff ( M c= N & M <> N ) ) by ORDINAL1:11, ORDINAL1:def_2; ::_thesis: verum
end;

theorem :: CARD_1:4
for M, N being Cardinal holds
( M in N iff not N c= M ) by ORDINAL1:5, ORDINAL1:16;

definition
let X be set ;
func card X ->  Cardinal means :Def2: :: CARD_1:def 2
X,it are_equipotent ;
existence
 ex b1 being Cardinal st X,b1 are_equipotent
proof
defpred S1[ Ordinal] means $1,X are_equipotent ;
A1: ex A being Ordinal st S1[A] by Th1;
consider A being Ordinal such that
A2: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A1);
 A is cardinal
proof
take  A ; :: according to CARD_1:def_1 ::_thesis: ( A = A & ( for A being Ordinal st A,A are_equipotent holds
A c= A ) )
thus  A = A ; ::_thesis: for A being Ordinal st A,A are_equipotent holds
A c= A
let B be Ordinal; ::_thesis: ( B,A are_equipotent implies A c= B )
assume  B,A are_equipotent ; ::_thesis: A c= B
hence  A c= B by A2, WELLORD2:15; ::_thesis: verum
end;
then reconsider M = A as Cardinal ;
take  M ; ::_thesis: X,M are_equipotent
thus  X,M are_equipotent by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Cardinal st X,b1 are_equipotent & X,b2 are_equipotent holds
b1 = b2
proof
let M, N be Cardinal; ::_thesis: ( X,M are_equipotent & X,N are_equipotent implies M = N )
assume  ( X,M are_equipotent & X,N are_equipotent ) ; ::_thesis: M = N
then  M,N are_equipotent by WELLORD2:15;
hence  M = N by Th2; ::_thesis: verum
end;
projectivity
 for b1 being Cardinal
for b2 being set st b2,b1 are_equipotent holds
b1,b1 are_equipotent ;
end;

:: deftheorem Def2 defines card CARD_1:def_2_:_
 for X being set
for b2 being Cardinal holds
( b2 = card X iff X,b2 are_equipotent );

registration
cluster empty  ->  cardinal for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is cardinal
proof
let S be set ; ::_thesis: ( S is empty implies S is cardinal )
assume A1: S is empty ; ::_thesis: S is cardinal
take  {} ; :: according to CARD_1:def_1 ::_thesis: ( S = {} & ( for A being Ordinal st A, {} are_equipotent holds
{} c= A ) )
thus  S = {} by A1; ::_thesis: for A being Ordinal st A, {} are_equipotent holds
{} c= A
let A be Ordinal; ::_thesis: ( A, {} are_equipotent implies {} c= A )
assume  A, {} are_equipotent ; ::_thesis: {} c= A
thus  {} c= A ; ::_thesis: verum
end;
end;

registration
let X be empty set ;
cluster card X ->  empty ;
coherence
 card X is empty by Def2;
end;

registration
let X be non empty set ;
cluster card X ->  non empty ;
coherence
 not card X is empty
proof
assume  card X is empty ; ::_thesis: contradiction
then  X, {} are_equipotent by Def2;
then  ex f being Function st
( f is one-to-one & dom f = X & rng f = {} ) by WELLORD2:def_4;
hence  contradiction by RELAT_1:42; ::_thesis: verum
end;
end;

theorem Th5: :: CARD_1:5
for X, Y being set holds
( X,Y are_equipotent iff card X = card Y )
proof
let X, Y be set ; ::_thesis: ( X,Y are_equipotent iff card X = card Y )
A1: Y, card Y are_equipotent by Def2;
A2: X, card X are_equipotent by Def2;
thus  ( X,Y are_equipotent implies card X = card Y ) ::_thesis: ( card X = card Y implies X,Y are_equipotent )
proof
assume  X,Y are_equipotent ; ::_thesis: card X = card Y
then  card X,Y are_equipotent by A2, WELLORD2:15;
hence  card X = card Y by Def2; ::_thesis: verum
end;
assume  card X = card Y ; ::_thesis: X,Y are_equipotent
hence  X,Y are_equipotent by A2, A1, WELLORD2:15; ::_thesis: verum
end;

theorem Th6: :: CARD_1:6
for R being Relation st R is well-ordering holds
field R, order_type_of R are_equipotent
proof
let R be Relation; ::_thesis: ( R is well-ordering implies field R, order_type_of R are_equipotent )
assume  R is well-ordering ; ::_thesis: field R, order_type_of R are_equipotent
then  R, RelIncl (order_type_of R) are_isomorphic by WELLORD2:def_2;
then consider f being Function such that
A1: f is_isomorphism_of R, RelIncl (order_type_of R) by WELLORD1:def_8;
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = field R & rng f = order_type_of R )
 field (RelIncl (order_type_of R)) = order_type_of R by WELLORD2:def_1;
hence  ( f is one-to-one & dom f = field R & rng f = order_type_of R ) by A1, WELLORD1:def_7; ::_thesis: verum
end;

theorem Th7: :: CARD_1:7
for X being set
for M being Cardinal st X c= M holds
card X c= M
proof
let X be set ; ::_thesis: for M being Cardinal st X c= M holds
card X c= M
let M be Cardinal; ::_thesis: ( X c= M implies card X c= M )
defpred S1[ Ordinal] means ( $1 c= M & X,$1 are_equipotent );
reconsider m = M as Ordinal ;
assume  X c= M ; ::_thesis: card 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 being Ordinal st S1[A] by A1, Th6;
consider A being Ordinal such that
A3: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A2);
 A is cardinal
proof
take  A ; :: according to CARD_1:def_1 ::_thesis: ( A = A & ( for A being Ordinal st A,A are_equipotent holds
A c= A ) )
thus  A = A ; ::_thesis: for A being Ordinal st A,A are_equipotent holds
A c= A
let B be Ordinal; ::_thesis: ( B,A are_equipotent implies A c= B )
assume A4: B,A are_equipotent ; ::_thesis: A c= B
assume A5: not A c= B ; ::_thesis: contradiction
then  m c= B by A3, A4, WELLORD2:15;
hence  contradiction by A3, A5, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider A = A as Cardinal ;
 card X = A by A3, Def2;
hence  card X c= M by A3; ::_thesis: verum
end;

theorem Th8: :: CARD_1:8
for A being Ordinal holds card A c= A
proof
let A be Ordinal; ::_thesis: card A c= A
 ( ex B being Ordinal st
( card A = B & ( for C being Ordinal st C,B are_equipotent holds
B c= C ) ) & A, card A are_equipotent ) by Def1, Def2;
hence  card A c= A ; ::_thesis: verum
end;

theorem :: CARD_1:9
for X being set
for M being Cardinal st X in M holds
card X in M by Th8, ORDINAL1:12;

theorem Th10: :: CARD_1:10
for X, Y being set holds
( card X c= card Y iff ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) )
proof
let X, Y be set ; ::_thesis: ( card X c= card Y iff ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) )
thus  ( card X c= card Y implies ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) ) ::_thesis: ( ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) implies card X c= card Y )
proof
 X, card X are_equipotent by Def2;
then consider f being Function such that
A1: f is one-to-one and
A2: ( dom f = X & rng f = card X ) by WELLORD2:def_4;
assume A3: card X c= card Y ; ::_thesis: ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y )
 Y, card Y are_equipotent by Def2;
then consider g being Function such that
A4: g is one-to-one and
A5: ( dom g = Y & rng g = card Y ) by WELLORD2:def_4;
take h = (g ") * f; ::_thesis: ( h is one-to-one & dom h = X & rng h c= Y )
thus  h is one-to-one by A1, A4; ::_thesis: ( dom h = X & rng h c= Y )
 ( rng g = dom (g ") & dom g = rng (g ") ) by A4, FUNCT_1:33;
hence  ( dom h = X & rng h c= Y ) by A3, A2, A5, RELAT_1:26, RELAT_1:27; ::_thesis: verum
end;
given f being Function such that A6: f is one-to-one and
A7: ( dom f = X & rng f c= Y ) ; ::_thesis: card X c= card Y
 Y, card Y are_equipotent by Def2;
then consider g being Function such that
A8: g is one-to-one and
A9: dom g = Y and
A10: rng g = card Y by WELLORD2:def_4;
A11: X, rng (g * f) are_equipotent
proof
take  g * f ; :: according to WELLORD2:def_4 ::_thesis: ( g * f is one-to-one & dom (g * f) = X & rng (g * f) = rng (g * f) )
thus  g * f is one-to-one by A6, A8; ::_thesis: ( dom (g * f) = X & rng (g * f) = rng (g * f) )
thus  dom (g * f) = X by A7, A9, RELAT_1:27; ::_thesis: rng (g * f) = rng (g * f)
thus  rng (g * f) = rng (g * f) ; ::_thesis: verum
end;
 rng (g * f), card (rng (g * f)) are_equipotent by Def2;
then A12: X, card (rng (g * f)) are_equipotent by A11, WELLORD2:15;
 card (rng (g * f)) c= card Y by A10, Th7, RELAT_1:26;
hence  card X c= card Y by A12, Def2; ::_thesis: verum
end;

theorem Th11: :: CARD_1:11
for X, Y being set st X c= Y holds
card X c= card Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies card X c= card Y )
assume A1: X c= Y ; ::_thesis: card X c= card Y
 ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y )
proof
take  id X ; ::_thesis: ( id X is one-to-one & dom (id X) = X & rng (id X) c= Y )
thus  ( id X is one-to-one & dom (id X) = X & rng (id X) c= Y ) by A1, RELAT_1:45; ::_thesis: verum
end;
hence  card X c= card Y by Th10; ::_thesis: verum
end;

theorem Th12: :: CARD_1:12
for X, Y being set holds
( card X c= card Y iff ex f being Function st
( dom f = Y & X c= rng f ) )
proof
let X, Y be set ; ::_thesis: ( card X c= card Y iff ex f being Function st
( dom f = Y & X c= rng f ) )
thus  ( card X c= card Y implies ex f being Function st
( dom f = Y & X c= rng f ) ) ::_thesis: ( ex f being Function st
( dom f = Y & X c= rng f ) implies card X c= card Y )
proof
assume  card X c= card Y ; ::_thesis: ex f being Function st
( dom f = Y & X c= rng f )
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f c= Y by Th10;
defpred S1[ set , set ] means ( ( $1 in rng f & $2 = (f ") . $1 ) or ( not $1 in rng f & $2 = 0 ) );
A4: for x being set st x in Y holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in Y implies ex y being set st S1[x,y] )
assume  x in Y ; ::_thesis: ex y being set st S1[x,y]
 ( not x in rng f implies ex y being set st S1[x,y] ) ;
hence  ex y being set st S1[x,y] ; ::_thesis: verum
end;
A5: for x, y, z being set st x in Y & S1[x,y] & S1[x,z] holds
y = z ;
consider g being Function such that
A6: ( dom g = Y & ( for y being set st y in Y holds
S1[y,g . y] ) ) from FUNCT_1:sch_2(A5, A4);
take  g ; ::_thesis: ( dom g = Y & X c= rng g )
thus  dom g = Y by A6; ::_thesis: X c= rng g
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng g )
assume A7: x in X ; ::_thesis: x in rng g
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  x in rng g by A3, A6, A8, FUNCT_1:def_3; ::_thesis: verum
end;
given f being Function such that A9: dom f = Y and
A10: X c= rng f ; ::_thesis: card X c= card Y
deffunc H1( set ) ->  set = f " {$1};
consider g being Function such that
A11: ( dom g = X & ( for x being set st x in X holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
 ( X <> {} implies card X c= card Y )
proof
assume  X <> {} ; ::_thesis: card X c= card Y
then reconsider M = rng g as non empty set by A11, RELAT_1:42;
 for Z being set st Z in M holds
Z <> {}
proof
let Z be set ; ::_thesis: ( Z in M implies Z <> {} )
assume  Z in M ; ::_thesis: Z <> {}
then consider x being set  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 being set st
( y in dom f & x = f . y ) ) by A10, A11, A12, FUNCT_1:def_3;
hence  Z <> {} by A13, FUNCT_1:def_7; ::_thesis: verum
end;
then consider F being Function such that
A14: dom F = M and
A15: for Z being set 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 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom (F * g) or not b1 in dom (F * g) or not (F * g) . x = (F * g) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom (F * g) or not y in dom (F * g) or not (F * g) . x = (F * g) . y or x = y )
assume that
A18: x in dom (F * g) and
A19: y in dom (F * g) and
A20: (F * g) . x = (F * g) . y ; ::_thesis: x = 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  x = y by A20, A23, A21, A22, A24, TARSKI:def_1; ::_thesis: verum
end;
 rng (F * g) c= Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (F * g) or x in Y )
assume  x in rng (F * g) ; ::_thesis: x in Y
then consider y being set  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  x in Y by A9, FUNCT_1:def_7; ::_thesis: verum
end;
hence  card X c= card Y by A16, A17, Th10; ::_thesis: verum
end;
hence  card X c= card Y ; ::_thesis: verum
end;

theorem Th13: :: CARD_1:13
for X being set holds not X, bool X are_equipotent
proof
let X be set ; ::_thesis: not X, bool X are_equipotent
given f being Function such that  f is one-to-one and
A1: ( dom f = X & rng f = bool X ) ; :: according to WELLORD2:def_4 ::_thesis: contradiction
defpred S1[ set ] means  for Y being set st Y = f . $1 holds
not $1 in Y;
consider Z being set  such that
A2: for a being set holds
( a in Z iff ( a in X & S1[a] ) ) from XBOOLE_0:sch_1();
 Z c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Z or a in X )
thus  ( not a in Z or a in X ) by A2; ::_thesis: verum
end;
then consider a being set  such that
A3: a in X and
A4: Z = f . a by A1, FUNCT_1:def_3;
 not a in Z by A2, A4;
then  ex Y being set st
( Y = f . a & a in Y ) by A2, A3;
hence  contradiction by A2, A4; ::_thesis: verum
end;

theorem Th14: :: CARD_1:14
for X being set holds card X in card (bool X)
proof
let X be set ; ::_thesis: card X in card (bool X)
deffunc H1( set ) ->  set = {$1};
consider f being Function such that
A1: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
A2: rng f c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in bool X )
assume  x in rng f ; ::_thesis: x in bool X
then consider y being set  such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def_3;
A5: {y} c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {y} or z in X )
assume  z in {y} ; ::_thesis: z in X
hence  z in X by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
 f . y = {y} by A1, A3;
hence  x in bool X by A4, A5; ::_thesis: verum
end;
 not X, bool X are_equipotent by Th13;
then A6: card X <> card (bool X) by Th5;
 f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A7: ( x in dom f & y in dom f ) and
A8: f . x = f . y ; ::_thesis: x = y
 ( f . x = {x} & f . y = {y} ) by A1, A7;
hence  x = y by A8, ZFMISC_1:3; ::_thesis: verum
end;
then  card X c= card (bool X) by A1, A2, Th10;
then  card X c< card (bool X) by A6, XBOOLE_0:def_8;
hence  card X in card (bool X) by ORDINAL1:11; ::_thesis: verum
end;

definition
let X be set ;
func nextcard X ->  Cardinal means :Def3: :: CARD_1:def 3
( card X in it & ( for M being Cardinal st card X in M holds
it c= M ) );
existence
 ex b1 being Cardinal st
( card X in b1 & ( for M being Cardinal st card X in M holds
b1 c= M ) )
proof
defpred S1[ Ordinal] means  ex M being Cardinal st
( $1 = M & card X in M );
 card X in card (bool X) by Th14;
then A1: ex A being Ordinal st S1[A] ;
consider A being Ordinal such that
A2: S1[A] and
A3: for B being Ordinal st S1[B] holds
A c= B from ORDINAL1:sch_1(A1);
consider M being Cardinal such that
A4: A = M and
A5: card X in M by A2;
take  M ; ::_thesis: ( card X in M & ( for M being Cardinal st card X in M holds
M c= M ) )
thus  card X in M by A5; ::_thesis: for M being Cardinal st card X in M holds
M c= M
let N be Cardinal; ::_thesis: ( card X in N implies M c= N )
assume  card X in N ; ::_thesis: M c= N
hence  M c= N by A3, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Cardinal st card X in b1 & ( for M being Cardinal st card X in M holds
b1 c= M ) & card X in b2 & ( for M being Cardinal st card X in M holds
b2 c= M ) holds
b1 = b2
proof
let M1, M2 be Cardinal; ::_thesis: ( card X in M1 & ( for M being Cardinal st card X in M holds
M1 c= M ) & card X in M2 & ( for M being Cardinal st card X in M holds
M2 c= M ) implies M1 = M2 )
assume  ( card X in M1 & ( for M being Cardinal st card X in M holds
M1 c= M ) & card X in M2 & ( for M being Cardinal st card X in M holds
M2 c= M ) ) ; ::_thesis: M1 = M2
then  ( M1 c= M2 & M2 c= M1 ) ;
hence  M1 = M2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines nextcard CARD_1:def_3_:_
 for X being set
for b2 being Cardinal holds
( b2 = nextcard X iff ( card X in b2 & ( for M being Cardinal st card X in M holds
b2 c= M ) ) );

theorem :: CARD_1:15
for X being set holds {} in nextcard X
proof
let X be set ; ::_thesis: {} in nextcard X
 ( card {} c= card X & card X in nextcard X ) by Def3;
hence  {} in nextcard X by ORDINAL1:12; ::_thesis: verum
end;

theorem Th16: :: CARD_1:16
for X, Y being set st card X = card Y holds
nextcard X = nextcard Y
proof
let X, Y be set ; ::_thesis: ( card X = card Y implies nextcard X = nextcard Y )
assume A1: card X = card Y ; ::_thesis: nextcard X = nextcard Y
 ( card X in nextcard X & ( for N being Cardinal st card X in N holds
nextcard X c= N ) ) by Def3;
hence  nextcard X = nextcard Y by A1, Def3; ::_thesis: verum
end;

theorem Th17: :: CARD_1:17
for X, Y being set st X,Y are_equipotent holds
nextcard X = nextcard Y
proof
let X, Y be set ; ::_thesis: ( X,Y are_equipotent implies nextcard X = nextcard Y )
assume  X,Y are_equipotent ; ::_thesis: nextcard X = nextcard Y
then  card X = card Y by Th5;
hence  nextcard X = nextcard Y by Th16; ::_thesis: verum
end;

theorem Th18: :: CARD_1:18
for A being Ordinal holds A in nextcard A
proof
let A be Ordinal; ::_thesis: A in nextcard A
assume  not A in nextcard A ; ::_thesis: contradiction
then A1: card (nextcard A) c= card A by Th11, ORDINAL1:16;
 A, card A are_equipotent by Def2;
then A2: nextcard (card A) = nextcard A by Th17;
A3: card (card A) in nextcard (card A) by Def3;
 card (nextcard A) = nextcard A by Def2;
hence  contradiction by A1, A2, A3, ORDINAL1:5; ::_thesis: verum
end;

definition
let M be Cardinal;
attrM is limit_cardinal  means :Def4: :: CARD_1:def 4
 for N being Cardinal holds not M = nextcard N;
end;

:: deftheorem Def4 defines limit_cardinal CARD_1:def_4_:_
 for M being Cardinal holds
( M is limit_cardinal iff for N being Cardinal holds not M = nextcard N );

definition
let A be Ordinal;
func alef A ->  set  means :Def5: :: CARD_1:def 5
 ex S being T-Sequence st
( it = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds
S . B = card (sup (S | B)) ) );
correctness
existence
ex b1 being set ex S being T-Sequence st
( b1 = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds
S . B = card (sup (S | B)) ) );
uniqueness
for b1, b2 being set st ex S being T-Sequence st
( b1 = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) & ex S being T-Sequence st
( b2 = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) holds
b1 = b2;
proof
set B = card omega;
deffunc H1( Ordinal, T-Sequence) ->  Cardinal = card (sup $2);
deffunc H2( Ordinal, set ) ->  Cardinal = nextcard (union {$2});
thus  ( ex x being set ex S being T-Sequence st
( x = last S & dom S = succ A & S . {} = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H2(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
S . C = H1(C,S | C) ) ) & ( for x1, x2 being set st ex S being T-Sequence st
( x1 = last S & dom S = succ A & S . {} = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H2(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
S . C = H1(C,S | C) ) ) & ex S being T-Sequence st
( x2 = last S & dom S = succ A & S . {} = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H2(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
S . C = H1(C,S | C) ) ) holds
x1 = x2 ) ) from ORDINAL2:sch_7(); ::_thesis: verum
end;
end;

:: deftheorem Def5 defines alef CARD_1:def_5_:_
 for A being Ordinal
for b2 being set holds
( b2 = alef A iff ex S being T-Sequence st
( b2 = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) );

Lm1: now__::_thesis:_(_alef_0_=_card_omega_&_(_for_A_being_Ordinal_holds_H3(_succ_A)_=_H2(A,H3(A))_)_&_(_for_A_being_Ordinal_st_A_<>_{}_&_A_is_limit_ordinal_holds_
for_S_being_T-Sequence_st_dom_S_=_A_&_(_for_B_being_Ordinal_st_B_in_A_holds_
S_._B_=_alef_B_)_holds_
alef_A_=_card_(sup_S)_)_)
deffunc H1( Ordinal, T-Sequence) ->  Cardinal = card (sup $2);
deffunc H2( Ordinal, set ) ->  Cardinal = nextcard (union {$2});
deffunc H3( Ordinal) ->  set = alef $1;
A1: for A being Ordinal
for x being set holds
( x = H3(A) iff ex S being T-Sequence st
( x = last S & dom S = succ A & S . {} = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H2(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
S . C = H1(C,S | C) ) ) ) by Def5;
 H3( {} ) = card omega from ORDINAL2:sch_8(A1);
hence  alef 0 = card omega ; ::_thesis: ( ( for A being Ordinal holds H3( succ A) = H2(A,H3(A)) ) & ( for A being Ordinal st A <> {} & A is limit_ordinal holds
for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = alef B ) holds
alef A = card (sup S) ) )
thus  for A being Ordinal holds H3( succ A) = H2(A,H3(A)) from ORDINAL2:sch_9(A1); ::_thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = alef B ) holds
alef A = card (sup S)
thus  for A being Ordinal st A <> {} & A is limit_ordinal holds
for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = alef B ) holds
alef A = card (sup S) ::_thesis: verum
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = alef B ) holds
alef A = card (sup S) )
assume A2: ( A <> {} & A is limit_ordinal ) ; ::_thesis: for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = alef B ) holds
alef A = card (sup S)
let S be T-Sequence; ::_thesis: ( dom S = A & ( for B being Ordinal st B in A holds
S . B = alef B ) implies alef A = card (sup S) )
assume that
A3: dom S = A and
A4: for B being Ordinal st B in A holds
S . B = H3(B) ; ::_thesis: alef A = card (sup S)
thus  H3(A) = H1(A,S) from ORDINAL2:sch_10(A1, A2, A3, A4); ::_thesis: verum
end;
end;

deffunc H1( Ordinal) ->  set = alef $1;

registration
let A be Ordinal;
cluster alef A ->  cardinal ;
coherence
 alef A is cardinal
proof
A1: now__::_thesis:_(_A_<>_{}_&_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_alef_A_is_Cardinal_)
consider S being T-Sequence such that
A2: ( dom S = A & ( for B being Ordinal st B in A holds
S . B = H1(B) ) ) from ORDINAL2:sch_2();
assume that
A3: A <> {} and
A4: for B being Ordinal holds A <> succ B ; ::_thesis: alef A is Cardinal
 A is limit_ordinal by A4, ORDINAL1:29;
then  alef A = card (sup S) by A3, A2, Lm1;
hence  alef A is Cardinal ; ::_thesis: verum
end;
now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_alef_A_is_cardinal_)
given B being Ordinal such that A5: A = succ B ; ::_thesis: alef A is cardinal
 alef A = nextcard (union {(alef B)}) by A5, Lm1;
hence  alef A is cardinal ; ::_thesis: verum
end;
hence  alef A is cardinal by A1, Lm1; ::_thesis: verum
end;
end;

theorem Th19: :: CARD_1:19
for A being Ordinal holds alef (succ A) = nextcard (alef A)
proof
let A be Ordinal; ::_thesis: alef (succ A) = nextcard (alef A)
thus  alef (succ A) = nextcard (union {(alef A)}) by Lm1
.= nextcard (alef A) by ZFMISC_1:25 ; ::_thesis: verum
end;

theorem :: CARD_1:20
for A being Ordinal st A <> {} & A is limit_ordinal holds
for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = alef B ) holds
alef A = card (sup S) by Lm1;

theorem Th21: :: CARD_1:21
for A, B being Ordinal holds
( A in B iff alef A in alef B )
proof
let A, B be Ordinal; ::_thesis: ( A in B iff alef A in alef B )
defpred S1[ Ordinal] means  for A being Ordinal st A in $1 holds
alef A in alef $1;
A1: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume A2: S1[B] ; ::_thesis: S1[ succ B]
let A be Ordinal; ::_thesis: ( A in succ B implies alef A in alef (succ B) )
A3: alef (succ B) = nextcard (alef B) by Th19;
A4: now__::_thesis:_(_A_in_B_&_A_in_succ_B_implies_alef_A_in_alef_(succ_B)_)
assume  A in B ; ::_thesis: ( A in succ B implies alef A in alef (succ B) )
then A5: alef A in alef B by A2;
 alef B in nextcard (alef B) by Th18;
hence  ( A in succ B implies alef A in alef (succ B) ) by A3, A5, ORDINAL1:10; ::_thesis: verum
end;
A6: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def_8;
assume  A in succ B ; ::_thesis: alef A in alef (succ B)
hence  alef A in alef (succ B) by A3, A6, A4, Th18, ORDINAL1:11, ORDINAL1:22; ::_thesis: verum
end;
A7: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume that
A8: B <> {} and
A9: B is limit_ordinal and
 for C being Ordinal st C in B holds
for A being Ordinal st A in C holds
alef A in alef C ; ::_thesis: S1[B]
let A be Ordinal; ::_thesis: ( A in B implies alef A in alef B )
consider S being T-Sequence such that
A10: ( dom S = B & ( for C being Ordinal st C in B holds
S . C = H1(C) ) ) from ORDINAL2:sch_2();
assume  A in B ; ::_thesis: alef A in alef B
then  succ A in B by A9, ORDINAL1:28;
then  ( S . (succ A) in rng S & S . (succ A) = alef (succ A) ) by A10, FUNCT_1:def_3;
then A11: alef (succ A) in sup (rng S) by ORDINAL2:19;
 sup (rng S) = sup S by ORDINAL2:26;
then A12: alef (succ A) c= sup S by A11, ORDINAL1:def_2;
A13: card (alef (succ A)) = alef (succ A) by Def2;
A14: ( alef (succ A) = nextcard (alef A) & alef A in nextcard (alef A) ) by Th18, Th19;
 alef B = card (sup S) by A8, A9, A10, Lm1;
then  alef (succ A) c= alef B by A12, A13, Th11;
hence  alef A in alef B by A14; ::_thesis: verum
end;
A15: S1[ {} ] ;
A16: for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A15, A1, A7);
hence  ( A in B implies alef A in alef B ) ; ::_thesis: ( alef A in alef B implies A in B )
assume A17: alef A in alef B ; ::_thesis: A in B
then A18: alef A <> alef B ;
 not B in A by A16, A17;
hence  A in B by A18, ORDINAL1:14; ::_thesis: verum
end;

theorem Th22: :: CARD_1:22
for A, B being Ordinal st alef A = alef B holds
A = B
proof
let A, B be Ordinal; ::_thesis: ( alef A = alef B implies A = B )
assume A1: alef A = alef B ; ::_thesis: A = B
A2: now__::_thesis:_not_B_in_A
assume  B in A ; ::_thesis: contradiction
then  alef B in alef A by Th21;
hence  contradiction by A1; ::_thesis: verum
end;
now__::_thesis:_not_A_in_B
assume  A in B ; ::_thesis: contradiction
then  alef A in alef B by Th21;
hence  contradiction by A1; ::_thesis: verum
end;
hence  A = B by A2, ORDINAL1:14; ::_thesis: verum
end;

theorem :: CARD_1:23
for A, B being Ordinal holds
( A c= B iff alef A c= alef B )
proof
let A, B be Ordinal; ::_thesis: ( A c= B iff alef A c= alef B )
A1: ( A c< B iff ( A <> B & A c= B ) ) by XBOOLE_0:def_8;
A2: ( alef A c< alef B iff ( alef A <> alef B & alef A c= alef B ) ) by XBOOLE_0:def_8;
 ( A in B iff alef A in alef B ) by Th21;
hence  ( A c= B iff alef A c= alef B ) by A1, A2, Th22, ORDINAL1:11, ORDINAL1:def_2; ::_thesis: verum
end;

theorem :: CARD_1:24
for X, Y, Z being set st X c= Y & Y c= Z & X,Z are_equipotent holds
( X,Y are_equipotent & Y,Z are_equipotent )
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y & Y c= Z & X,Z are_equipotent implies ( X,Y are_equipotent & Y,Z are_equipotent ) )
assume that
A1: ( X c= Y & Y c= Z ) and
A2: X,Z are_equipotent ; ::_thesis: ( X,Y are_equipotent & Y,Z are_equipotent )
A3: card X = card Z by A2, Th5;
 ( card X c= card Y & card Y c= card Z ) by A1, Th11;
then  card X = card Y by A3, XBOOLE_0:def_10;
hence  ( X,Y are_equipotent & Y,Z are_equipotent ) by A3, Th5; ::_thesis: verum
end;

theorem :: CARD_1:25
for Y, X being set st bool Y c= X holds
( card Y in card X & not Y,X are_equipotent )
proof
let Y, X be set ; ::_thesis: ( bool Y c= X implies ( card Y in card X & not Y,X are_equipotent ) )
assume  bool Y c= X ; ::_thesis: ( card Y in card X & not Y,X are_equipotent )
then A1: card (bool Y) c= card X by Th11;
 card Y in card (bool Y) by Th14;
hence  card Y in card X by A1; ::_thesis: not Y,X are_equipotent
then  card Y <> card X ;
hence  not Y,X are_equipotent by Th5; ::_thesis: verum
end;

theorem Th26: :: CARD_1:26
for X being set st X, {} are_equipotent holds
X = {}
proof
let X be set ; ::_thesis: ( X, {} are_equipotent implies X = {} )
given f being Function such that  f is one-to-one and
A1: ( dom f = X & rng f = {} ) ; :: according to WELLORD2:def_4 ::_thesis: X = {}
thus  X = {} by A1, RELAT_1:42; ::_thesis: verum
end;

theorem :: CARD_1:27
card {} = {} ;

theorem Th28: :: CARD_1:28
for X, x being set holds
( X,{x} are_equipotent iff ex x being set st X = {x} )
proof
let X, x be set ; ::_thesis: ( X,{x} are_equipotent iff ex x being set st X = {x} )
thus  ( X,{x} are_equipotent implies ex x being set st X = {x} ) ::_thesis: ( ex x being set st X = {x} implies X,{x} are_equipotent )
proof
assume  X,{x} are_equipotent ; ::_thesis: ex x being set st X = {x}
then consider f being Function 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  ex x being set st X = {x} by A2; ::_thesis: verum
end;
given y being set  such that A3: X = {y} ; ::_thesis: X,{x} are_equipotent
take f = X --> x; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = {x} )
A4: dom f = X by FUNCOP_1:13;
thus  f is one-to-one ::_thesis: ( dom f = X & rng f = {x} )
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in dom f or not b1 in dom f or not f . a = f . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A5: a in dom f and
A6: b in dom f and
 f . a = f . b ; ::_thesis: a = b
 a = y by A3, A4, A5, TARSKI:def_1;
hence  a = b by A3, A4, A6, TARSKI:def_1; ::_thesis: verum
end;
thus  dom f = X by FUNCOP_1:13; ::_thesis: rng f = {x}
thus  rng f c= {x} by FUNCOP_1:13; :: according to XBOOLE_0:def_10 ::_thesis: {x} c= rng f
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in rng f )
assume  a in {x} ; ::_thesis: a in rng f
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  a in rng f by A3, A4, A7, A8, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th29: :: CARD_1:29
for X, x being set holds
( card X = card {x} iff ex x being set st X = {x} )
proof
let X, x be set ; ::_thesis: ( card X = card {x} iff ex x being set st X = {x} )
 ( card X = card {x} iff X,{x} are_equipotent ) by Th5;
hence  ( card X = card {x} iff ex x being set st X = {x} ) by Th28; ::_thesis: verum
end;

theorem Th30: :: CARD_1:30
for x being set holds card {x} = 1
proof
let x be set ; ::_thesis: card {x} = 1
A1: 1 = succ 0 ;
 1 is cardinal
proof
take IT = 1; :: according to CARD_1:def_1 ::_thesis: ( 1 = IT & ( for A being Ordinal st A,IT are_equipotent holds
IT c= A ) )
thus  1 = IT ; ::_thesis: for A being Ordinal st A,IT are_equipotent holds
IT c= A
let A be Ordinal; ::_thesis: ( A,IT are_equipotent implies IT c= A )
assume  A,IT are_equipotent ; ::_thesis: IT c= A
then  ex y being set st A = {y} by A1, Th28;
hence  IT c= A by A1, ZFMISC_1:33; ::_thesis: verum
end;
then reconsider M = 1 as Cardinal ;
 {x},M are_equipotent by A1, Th28;
hence  card {x} = 1 by Def2; ::_thesis: verum
end;

theorem Th31: :: CARD_1:31
for X, X1, Y, Y1 being set st X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1 are_equipotent holds
X \/ X1,Y \/ Y1 are_equipotent
proof
let X, X1, Y, Y1 be set ; ::_thesis: ( X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1 are_equipotent implies X \/ X1,Y \/ Y1 are_equipotent )
assume that
A1: X /\ X1 = {} and
A2: Y /\ Y1 = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( not X,Y are_equipotent or not X1,Y1 are_equipotent or X \/ X1,Y \/ Y1 are_equipotent )
given f being Function such that A3: f is one-to-one and
A4: dom f = X and
A5: rng f = Y ; :: according to WELLORD2:def_4 ::_thesis: ( not X1,Y1 are_equipotent or X \/ X1,Y \/ Y1 are_equipotent )
given g being Function such that A6: g is one-to-one and
A7: dom g = X1 and
A8: rng g = Y1 ; :: according to WELLORD2:def_4 ::_thesis: X \/ X1,Y \/ Y1 are_equipotent
defpred S1[ set , set ] means ( ( $1 in X & $2 = f . $1 ) or ( $1 in X1 & $2 = g . $1 ) );
A9: for x being set st x in X \/ X1 holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in X \/ X1 implies ex y being set st S1[x,y] )
assume  x in X \/ X1 ; ::_thesis: ex y being set st S1[x,y]
then  ( x in X or x in X1 ) by XBOOLE_0:def_3;
hence  ex y being set st S1[x,y] ; ::_thesis: verum
end;
A10: for x, y, z being set st x in X \/ X1 & S1[x,y] & S1[x,z] holds
y = z by A1, XBOOLE_0:def_4;
consider h being Function such that
A11: dom h = X \/ X1 and
A12: for x being set st x in X \/ X1 holds
S1[x,h . x] from FUNCT_1:sch_2(A10, A9);
take  h ; :: according to WELLORD2:def_4 ::_thesis: ( h is one-to-one & dom h = X \/ X1 & rng h = Y \/ Y1 )
thus  h is one-to-one ::_thesis: ( dom h = X \/ X1 & rng h = Y \/ Y1 )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom h or not b1 in dom h or not h . x = h . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom h or not y in dom h or not h . x = h . y or x = y )
assume that
A13: x in dom h and
A14: y in dom h and
A15: h . x = h . y ; ::_thesis: x = 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__::_thesis:_(_y_in_X_implies_not_x_in_X1_)
assume A19: ( y in X & x in X1 ) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
now__::_thesis:_(_x_in_X_implies_not_y_in_X1_)
assume A20: ( x in X & y in X1 ) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  x = y by A3, A4, A6, A7, A15, A17, A16, A18, FUNCT_1:def_4; ::_thesis: verum
end;
thus  dom h = X \/ X1 by A11; ::_thesis: rng h = Y \/ Y1
thus  rng h c= Y \/ Y1 :: according to XBOOLE_0:def_10 ::_thesis: Y \/ Y1 c= rng h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng h or x in Y \/ Y1 )
assume  x in rng h ; ::_thesis: x in Y \/ Y1
then consider y being set  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__::_thesis:_(_y_in_X1_implies_x_in_Y_\/_Y1_)
assume  y in X1 ; ::_thesis: x in Y \/ Y1
then  x in Y1 by A1, A7, A8, A23, FUNCT_1:def_3, XBOOLE_0:def_4;
hence  x in Y \/ Y1 by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_y_in_X_implies_x_in_Y_\/_Y1_)
assume  y in X ; ::_thesis: x in Y \/ Y1
then  x in Y by A1, A4, A5, A23, FUNCT_1:def_3, XBOOLE_0:def_4;
hence  x in Y \/ Y1 by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in Y \/ Y1 by A11, A21, A24, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y \/ Y1 or x in rng h )
assume A25: x in Y \/ Y1 ; ::_thesis: x in rng h
A26: now__::_thesis:_(_x_in_Y1_implies_x_in_rng_h_)
assume  x in Y1 ; ::_thesis: x in rng h
then consider y being set  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  S1[y,h . y] by A12;
hence  x in rng h by A1, A7, A11, A27, A28, A29, FUNCT_1:def_3, XBOOLE_0:def_4; ::_thesis: verum
end;
now__::_thesis:_(_x_in_Y_implies_x_in_rng_h_)
assume  x in Y ; ::_thesis: x in rng h
then consider y being set  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  S1[y,h . y] by A12;
hence  x in rng h by A1, A4, A11, A30, A31, A32, FUNCT_1:def_3, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  x in rng h by A25, A26, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th32: :: CARD_1:32
for x, X, y being set st x in X & y in X holds
X \ {x},X \ {y} are_equipotent
proof
let x, X, y be set ; ::_thesis: ( x in X & y in X implies X \ {x},X \ {y} are_equipotent )
assume that
A1: x in X and
A2: y in X ; ::_thesis: X \ {x},X \ {y} are_equipotent
defpred S1[ set , set ] means ( ( $1 = y & $2 = x ) or ( $1 <> y & $1 = $2 ) );
A3: for a being set st a in X \ {x} holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in X \ {x} implies ex b being set st S1[a,b] )
assume  a in X \ {x} ; ::_thesis: ex b being set st S1[a,b]
 ( a = y implies ex b being set st S1[a,b] ) ;
hence  ex b being set st S1[a,b] ; ::_thesis: verum
end;
A4: for a, b1, b2 being set st a in X \ {x} & S1[a,b1] & S1[a,b2] holds
b1 = b2 ;
consider f being Function such that
A5: ( dom f = X \ {x} & ( for a being set st a in X \ {x} holds
S1[a,f . a] ) ) from FUNCT_1:sch_2(A4, A3);
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X \ {x} & rng f = X \ {y} )
thus  f is one-to-one ::_thesis: ( dom f = X \ {x} & rng f = X \ {y} )
proof
let b1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not b1 in dom f or not b1 in dom f or not f . b1 = f . b1 or b1 = b1 )
let b2 be set ; ::_thesis: ( not b1 in dom f or not b2 in dom f or not f . b1 = f . b2 or b1 = b2 )
assume that
A6: ( b1 in dom f & b2 in dom f ) and
A7: ( f . b1 = f . b2 & b1 <> b2 ) ; ::_thesis: contradiction
A8: ( not b1 in {x} & not b2 in {x} ) by A5, A6, XBOOLE_0:def_5;
 ( S1[b1,f . b1] & S1[b2,f . b2] ) by A5, A6;
hence  contradiction by A7, A8, TARSKI:def_1; ::_thesis: verum
end;
thus  dom f = X \ {x} by A5; ::_thesis: rng f = X \ {y}
thus  rng f c= X \ {y} :: according to XBOOLE_0:def_10 ::_thesis: X \ {y} c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in X \ {y} )
assume  z in rng f ; ::_thesis: z in X \ {y}
then consider a being set  such that
A9: a in dom f and
A10: z = f . a by FUNCT_1:def_3;
A11: now__::_thesis:_(_a_=_y_implies_z_in_X_\_{y}_)
assume A12: a = y ; ::_thesis: z in X \ {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  z in X \ {y} by A13, XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_(_a_<>_y_implies_z_in_X_\_{y}_)
assume  a <> y ; ::_thesis: z in X \ {y}
then  ( not a in {y} & a = z ) by A5, A9, A10, TARSKI:def_1;
hence  z in X \ {y} by A5, A9, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  z in X \ {y} by A11; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X \ {y} or z in rng f )
assume A14: z in X \ {y} ; ::_thesis: z in rng f
then  not z in {y} by XBOOLE_0:def_5;
then A15: z <> y by TARSKI:def_1;
A16: now__::_thesis:_(_z_<>_x_implies_z_in_rng_f_)
assume  z <> x ; ::_thesis: z in rng f
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  z in rng f by A5, A17, FUNCT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_z_=_x_implies_z_in_rng_f_)
assume A18: z = x ; ::_thesis: z in rng f
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  z in rng f by A19, FUNCT_1:def_3; ::_thesis: verum
end;
hence  z in rng f by A16; ::_thesis: verum
end;

theorem Th33: :: CARD_1:33
for X being set
for f being Function st X c= dom f & f is one-to-one holds
X,f .: X are_equipotent
proof
let X be set ; ::_thesis: for f being Function st X c= dom f & f is one-to-one holds
X,f .: X are_equipotent
let f be Function; ::_thesis: ( X c= dom f & f is one-to-one implies X,f .: X are_equipotent )
assume that
A1: X c= dom f and
A2: f is one-to-one ; ::_thesis: X,f .: X are_equipotent
take g = f | X; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & dom g = X & rng g = f .: X )
thus  g is one-to-one by A2, FUNCT_1:52; ::_thesis: ( dom g = X & rng g = f .: X )
thus  dom g = X by A1, RELAT_1:62; ::_thesis: rng g = f .: X
thus  rng g = f .: X by RELAT_1:115; ::_thesis: verum
end;

theorem Th34: :: CARD_1:34
for X, Y, x, y being set st X,Y are_equipotent & x in X & y in Y holds
X \ {x},Y \ {y} are_equipotent
proof
let X, Y, x, y be set ; ::_thesis: ( X,Y are_equipotent & x in X & y in Y implies X \ {x},Y \ {y} are_equipotent )
given f being Function such that A1: f is one-to-one and
A2: dom f = X and
A3: rng f = Y ; :: according to WELLORD2:def_4 ::_thesis: ( not x in X or not y in Y or X \ {x},Y \ {y} are_equipotent )
A4: X \ {x},f .: (X \ {x}) are_equipotent by A1, A2, Th33;
assume that
A5: x in X and
A6: y in Y ; ::_thesis: X \ {x},Y \ {y} are_equipotent
 f . x in Y by A2, A3, A5, FUNCT_1:def_3;
then A7: Y \ {(f . x)},Y \ {y} are_equipotent by A6, Th32;
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  X \ {x},Y \ {y} are_equipotent by A4, A7, WELLORD2:15; ::_thesis: verum
end;

theorem Th35: :: CARD_1:35
for X, Y being set st succ X, succ Y are_equipotent holds
X,Y are_equipotent
proof
let X, Y be set ; ::_thesis: ( succ X, succ Y are_equipotent implies X,Y are_equipotent )
A1: ( X in succ X & Y in succ Y ) by ORDINAL1:6;
 ( X = (succ X) \ {X} & Y = (succ Y) \ {Y} ) by ORDINAL1:37;
hence  ( succ X, succ Y are_equipotent implies X,Y are_equipotent ) by A1, Th34; ::_thesis: verum
end;

theorem Th36: :: CARD_1:36
for n being Nat holds
( n = {} or ex m being Nat st n = succ m )
proof
let n be Nat; ::_thesis: ( n = {} or ex m being Nat st n = succ m )
defpred S1[ Nat] means ( $1 = {} or ex m being Nat st $1 = succ m );
A1: for a being Nat st S1[a] holds
S1[ succ a] ;
A2: S1[ {} ] ;
thus  S1[n] from ORDINAL2:sch_17(A2, A1); ::_thesis: verum
end;

Lm2:  for n, m being Nat st n,m are_equipotent holds
n = m
proof
let n, m be Nat; ::_thesis: ( n,m are_equipotent implies n = m )
defpred S1[ Nat] means  for n being Nat st n,$1 are_equipotent holds
n = $1;
A1: for a being Nat st S1[a] holds
S1[ succ a]
proof
let a be Nat; ::_thesis: ( S1[a] implies S1[ succ a] )
assume A2: S1[a] ; ::_thesis: S1[ succ a]
let n be Nat; ::_thesis: ( n, succ a are_equipotent implies n = succ a )
assume A3: n, succ a are_equipotent ; ::_thesis: n = succ a
percases ( n = {} or n <> {} ) ;
suppose n = {} ; ::_thesis: n = succ a
hence  n = succ a by A3, Th26; ::_thesis: verum
end;
suppose n <> {} ; ::_thesis: n = succ a
then  ex m being Nat st n = succ m by Th36;
hence  n = succ a by A2, A3, Th35; ::_thesis: verum
end;
end;
end;
A4: S1[ {} ] by Th26;
 S1[m] from ORDINAL2:sch_17(A4, A1);
hence  ( n,m are_equipotent implies n = m ) ; ::_thesis: verum
end;

theorem Th37: :: CARD_1:37
for x being set st x in omega holds
x is cardinal
proof
let x be set ; ::_thesis: ( x in omega implies x is cardinal )
assume that
A1: x in omega and
A2: for B being Ordinal st x = B holds
ex C being Ordinal st
( C,B are_equipotent & not B c= C ) ; :: according to CARD_1:def_1 ::_thesis: contradiction
reconsider A = x as Ordinal by A1;
consider B being Ordinal 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; ::_thesis: verum
end;

registration
cluster natural  ->  cardinal for set ;
correctness
coherence
for b1 being number st b1 is natural holds
b1 is cardinal ;
proof
let n be number ; ::_thesis: ( n is natural implies n is cardinal )
assume  n is natural ; ::_thesis: n is cardinal
then  n in omega by ORDINAL1:def_12;
hence  n is cardinal by Th37; ::_thesis: verum
end;
end;

theorem Th38: :: CARD_1:38
for X, Y being set st X,Y are_equipotent & X is finite holds
Y is finite
proof
let X, Y be set ; ::_thesis: ( X,Y are_equipotent & X is finite implies Y is finite )
assume  X,Y are_equipotent ; ::_thesis: ( not X is finite or Y is finite )
then consider f being Function such that
 f is one-to-one and
A1: dom f = X and
A2: rng f = Y by WELLORD2:def_4;
given p being Function such that A3: rng p = X and
A4: dom p in omega ; :: according to FINSET_1:def_1 ::_thesis: Y is finite
take  f * p ; :: according to FINSET_1:def_1 ::_thesis: ( rng (f * p) = Y & dom (f * p) in omega )
thus  rng (f * p) = Y by A1, A2, A3, RELAT_1:28; ::_thesis: dom (f * p) in omega
thus  dom (f * p) in omega by A1, A3, A4, RELAT_1:27; ::_thesis: verum
end;

theorem Th39: :: CARD_1:39
for n being Nat holds
( n is finite & card n is finite )
proof
let n be Nat; ::_thesis: ( n is finite & card n is finite )
reconsider n = n as Element of omega by ORDINAL1:def_12;
 ( rng (id n) = n & dom (id n) = n ) by RELAT_1:45;
then  n is finite by FINSET_1:def_1;
hence  ( n is finite & card n is finite ) by Def2; ::_thesis: verum
end;

theorem :: CARD_1:40
for n, m being Nat st card n = card m holds
n = m
proof
let n, m be Nat; ::_thesis: ( card n = card m implies n = m )
assume A1: card n = card m ; ::_thesis: n = m
reconsider n = n as Element of omega by ORDINAL1:def_12;
 card n = n by Def2;
hence  n = m by A1, Def2; ::_thesis: verum
end;

theorem :: CARD_1:41
for n, m being Nat holds
( card n c= card m iff n c= m )
proof
let n, m be Nat; ::_thesis: ( card n c= card m iff n c= m )
 card n = n by Def2;
hence  ( card n c= card m iff n c= m ) by Def2; ::_thesis: verum
end;

theorem Th42: :: CARD_1:42
for n, m being Nat holds
( card n in card m iff n in m )
proof
let n, m be Nat; ::_thesis: ( card n in card m iff n in m )
 card n = n by Def2;
hence  ( card n in card m iff n in m ) by Def2; ::_thesis: verum
end;

theorem Th43: :: CARD_1:43
for X being set st X is finite holds
ex n being Nat st X,n are_equipotent
proof
let X be set ; ::_thesis: ( X is finite implies ex n being Nat st X,n are_equipotent )
defpred S1[ set ] means  ex n being Nat st $1,n are_equipotent ;
A1: S1[ {} ] ;
A2: for Z, Y being set st Z in X & Y c= X & S1[Y] holds
S1[Y \/ {Z}]
proof
let Z, Y be set ; ::_thesis: ( Z in X & Y c= X & S1[Y] implies S1[Y \/ {Z}] )
assume that
 Z in X and
 Y c= X ; ::_thesis: ( not S1[Y] or S1[Y \/ {Z}] )
given n being Nat such that A3: Y,n are_equipotent ; ::_thesis: S1[Y \/ {Z}]
A4: ( not Z in Y implies S1[Y \/ {Z}] )
proof
assume A5: not Z in Y ; ::_thesis: S1[Y \/ {Z}]
now__::_thesis:_not_Y_/\_{Z}_<>_{}
set x = the Element of Y /\ {Z};
assume  Y /\ {Z} <> {} ; ::_thesis: contradiction
then  ( the Element of Y /\ {Z} in Y & the Element of Y /\ {Z} in {Z} ) by XBOOLE_0:def_4;
hence  contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
then A6: Y misses {Z} by XBOOLE_0:def_7;
A7: now__::_thesis:_not_n_meets_{n}
assume  n meets {n} ; ::_thesis: contradiction
then consider x being set  such that
A8: x in n and
A9: x in {n} by XBOOLE_0:3;
 x = n by A9, TARSKI:def_1;
hence  contradiction by A8; ::_thesis: verum
end;
take  succ n ; ::_thesis: Y \/ {Z}, succ n are_equipotent
 {Z},{n} are_equipotent by Th28;
hence  Y \/ {Z}, succ n are_equipotent by A3, A7, A6, Th31; ::_thesis: verum
end;
 ( Z in Y implies S1[Y \/ {Z}] )
proof
assume A10: Z in Y ; ::_thesis: S1[Y \/ {Z}]
take  n ; ::_thesis: Y \/ {Z},n are_equipotent
 {Z} c= Y by A10, ZFMISC_1:31;
hence  Y \/ {Z},n are_equipotent by A3, XBOOLE_1:12; ::_thesis: verum
end;
hence  S1[Y \/ {Z}] by A4; ::_thesis: verum
end;
assume A11: X is finite ; ::_thesis: ex n being Nat st X,n are_equipotent
thus  S1[X] from FINSET_1:sch_2(A11, A1, A2); ::_thesis: verum
end;

theorem Th44: :: CARD_1:44
for n being Nat holds nextcard (card n) = card (succ n)
proof
let n be Nat; ::_thesis: nextcard (card n) = card (succ n)
reconsider sn = succ n as Nat ;
A1: for M being Cardinal st card (card n) in M holds
card (succ n) c= M
proof
A2: card n = n by Def2;
let M be Cardinal; ::_thesis: ( card (card n) in M implies card (succ n) c= M )
assume  card (card n) in M ; ::_thesis: card (succ n) c= M
then  succ n c= M by A2, ORDINAL1:21;
hence  card (succ n) c= M by Def2; ::_thesis: verum
end;
 n in succ n by ORDINAL1:6;
then  card n in card sn by Th42;
hence  nextcard (card n) = card (succ n) by A1, Def3; ::_thesis: verum
end;

definition
let n be Nat;
:: original: succ
redefine func succ n ->  Element of omega ;
coherence
 succ n is Element of omega by ORDINAL1:def_12;
end;

definition
let X be finite set ;
:: original: card
redefine func card X ->  Element of omega ;
coherence
 card X is Element of omega
proof
consider n being Nat such that
A1: X,n are_equipotent by Th43;
reconsider n = n as Element of omega by ORDINAL1:def_12;
 X,n are_equipotent by A1;
hence  card X is Element of omega by Def2; ::_thesis: verum
end;
end;

theorem :: CARD_1:45
for X being set st X is finite holds
nextcard X is finite
proof
let X be set ; ::_thesis: ( X is finite implies nextcard X is finite )
assume  X is finite ; ::_thesis: nextcard X is finite
then reconsider X = X as finite set ;
 card X = card (card X) ;
then A1: card (succ (card X)) = nextcard (card X) by Th44;
 X, card X are_equipotent by Def2;
then  nextcard (card X) = nextcard X by Th17;
hence  nextcard X is finite by A1, Th39; ::_thesis: verum
end;

scheme :: CARD_1:sch 1
CardinalInd{ P1[ set ] } :
 for M being Cardinal holds P1[M]
provided
A1: P1[ {} ] and
A2: for M being Cardinal st P1[M] holds
P1[ nextcard M] and
A3: for M being Cardinal st M <> {} & M is limit_cardinal & ( for N being Cardinal st N in M holds
P1[N] ) holds
P1[M]
proof
let M be Cardinal; ::_thesis: P1[M]
defpred S1[ Ordinal] means ( $1 is Cardinal implies P1[$1] );
A4: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A5: for B being Ordinal st B in A holds
S1[B] and
A6: A is Cardinal ; ::_thesis: P1[A]
reconsider M = A as Cardinal by A6;
A7: now__::_thesis:_(_not_M_is_limit_cardinal_implies_P1[M]_)
assume  not M is limit_cardinal ; ::_thesis: P1[M]
then consider N being Cardinal such that
A8: M = nextcard N by Def4;
 N in M by A8, Th18;
hence  P1[M] by A2, A5, A8; ::_thesis: verum
end;
now__::_thesis:_(_M_<>_{}_&_M_is_limit_cardinal_implies_P1[M]_)
assume A9: ( M <> {} & M is limit_cardinal ) ; ::_thesis: P1[M]
 for N being Cardinal st N in M holds
P1[N] by A5;
hence  P1[M] by A3, A9; ::_thesis: verum
end;
hence  P1[A] by A1, A7; ::_thesis: verum
end;
 for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A4);
hence  P1[M] ; ::_thesis: verum
end;

scheme :: CARD_1:sch 2
CardinalCompInd{ P1[ set ] } :
 for M being Cardinal holds P1[M]
provided
A1: for M being Cardinal st ( for N being Cardinal st N in M holds
P1[N] ) holds
P1[M]
proof
let M be Cardinal; ::_thesis: P1[M]
defpred S1[ Ordinal] means ( $1 is Cardinal implies P1[$1] );
A2: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A3: for B being Ordinal st B in A & B is Cardinal holds
P1[B] ; ::_thesis: S1[A]
assume  A is Cardinal ; ::_thesis: P1[A]
then reconsider M = A as Cardinal ;
 for N being Cardinal st N in M holds
P1[N] by A3;
hence  P1[A] by A1; ::_thesis: verum
end;
 for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A2);
hence  P1[M] ; ::_thesis: verum
end;

theorem Th46: :: CARD_1:46
alef 0 = omega
proof
thus  alef 0 c= omega by Lm1, Th8; :: according to XBOOLE_0:def_10 ::_thesis: omega c= alef 0
thus  omega c= alef 0 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in omega or x in alef 0 )
assume A1: x in omega ; ::_thesis: x in alef 0
then reconsider A = x as Ordinal ;
consider n being Element of omega  such that
A2: A = n by A1;
 succ n c= omega by ORDINAL1:21;
then A3: card (succ n) c= card omega by Th11;
 ( n in succ n & card (succ n) = succ n ) by Def2, ORDINAL1:6;
hence  x in alef 0 by A2, A3, Lm1; ::_thesis: verum
end;
end;

registration
cluster omega  ->  cardinal for number ;
coherence
 for b1 being number st b1 = omega holds
b1 is cardinal by Th46;
end;

theorem :: CARD_1:47
card omega = omega by Lm1, Th46;

registration
cluster omega  ->  limit_cardinal ;
coherence
 omega is limit_cardinal
proof
given N being Cardinal such that A1: omega = nextcard N ; :: according to CARD_1:def_4 ::_thesis: contradiction
 N in omega by A1, Th18;
then A2: succ N in omega by ORDINAL1:def_12;
reconsider n = N as Element of omega by A1, Th18;
A3: card (succ n) = succ n by Def2;
 ( nextcard (card n) = card (succ n) & card n = n ) by Def2, Th44;
hence  contradiction by A1, A2, A3; ::_thesis: verum
end;
end;

registration
cluster  ->  finite for Element of omega ;
coherence
 for b1 being Element of omega holds b1 is finite by Th39;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal finite cardinal for set ;
existence
 ex b1 being Cardinal st b1 is finite
proof
set n = the Element of omega ;
take  the Element of omega ; ::_thesis: the Element of omega is finite
thus  the Element of omega is finite ; ::_thesis: verum
end;
end;

theorem :: CARD_1:48
for M being finite Cardinal ex n being Nat st M = card n
proof
let M be finite Cardinal; ::_thesis: ex n being Nat st M = card n
 card M = M by Def2;
hence  ex n being Nat st M = card n ; ::_thesis: verum
end;

registration
let X be finite set ;
cluster card X ->  finite ;
coherence
 card X is finite ;
end;

Lm3:  for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n
proof
let A be Ordinal; ::_thesis: for n being Nat st A,n are_equipotent holds
A = n
let n be Nat; ::_thesis: ( A,n are_equipotent implies A = n )
defpred S1[ Nat] means  for A being Ordinal st A,$1 are_equipotent holds
A = $1;
A1: for n being Nat st S1[n] holds
S1[ succ n]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[ succ n] )
assume A2: S1[n] ; ::_thesis: S1[ succ n]
let A be Ordinal; ::_thesis: ( A, succ n are_equipotent implies A = succ n )
A3: ( n in succ n & (succ n) \ {n} = n ) by ORDINAL1:6, ORDINAL1:37;
assume A4: A, succ n are_equipotent ; ::_thesis: A = succ n
then  A <> {} by Th26;
then A5: {} in A by ORDINAL3:8;
now__::_thesis:_not_A_is_limit_ordinal
assume  A is limit_ordinal ; ::_thesis: contradiction
then A6: omega c= A by A5, ORDINAL1:def_11;
 card A = card (succ n) by A4, Th5;
hence  contradiction by A6, Lm1, Th11, Th46, ORDINAL1:5; ::_thesis: verum
end;
then consider B being Ordinal such that
A7: A = succ B by ORDINAL1:29;
 ( B in A & A \ {B} = B ) by A7, ORDINAL1:6, ORDINAL1:37;
hence  A = succ n by A2, A4, A7, A3, Th34; ::_thesis: verum
end;
A8: S1[ {} ] by Th26;
 S1[n] from ORDINAL2:sch_17(A8, A1);
hence  ( A,n are_equipotent implies A = n ) ; ::_thesis: verum
end;

Lm4:  for A being Ordinal holds
( A is finite iff A in omega )
proof
let A be Ordinal; ::_thesis: ( A is finite iff A in omega )
thus  ( A is finite implies A in omega ) ::_thesis: ( A in omega implies A is finite )
proof
assume  A is finite ; ::_thesis: A in omega
then consider n being Nat such that
A1: A,n are_equipotent by Th43;
 A = n by A1, Lm3;
hence  A in omega by ORDINAL1:def_12; ::_thesis: verum
end;
assume  A in omega ; ::_thesis: A is finite
hence  A is finite ; ::_thesis: verum
end;

registration
cluster omega  ->  infinite ;
coherence
 not omega is finite
proof
 not omega in omega ;
hence  not omega is finite by Lm4; ::_thesis: verum
end;
end;

registration
cluster infinite for set ;
existence
 ex b1 being set st b1 is infinite
proof
take  omega ; ::_thesis: omega is infinite
thus  omega is infinite ; ::_thesis: verum
end;
end;

registration
let X be infinite set ;
cluster card X ->  infinite ;
coherence
 not card X is finite
proof
 X, card X are_equipotent by Def2;
hence  not card X is finite by Th38; ::_thesis: verum
end;
end;

begin

theorem Th49: :: CARD_1:49
1 = {0}
proof
thus 1 = succ 0
.= {0} ; ::_thesis: verum
end;

theorem Th50: :: CARD_1:50
2 = {0,1}
proof
thus 2 = succ 1
.= {0,1} by Th49, ENUMSET1:1 ; ::_thesis: verum
end;

theorem Th51: :: CARD_1:51
3 = {0,1,2}
proof
thus 3 = succ 2
.= {0,1,2} by Th50, ENUMSET1:3 ; ::_thesis: verum
end;

theorem Th52: :: CARD_1:52
4 = {0,1,2,3}
proof
thus 4 = succ 3
.= {0,1,2,3} by Th51, ENUMSET1:6 ; ::_thesis: verum
end;

theorem Th53: :: CARD_1:53
5 = {0,1,2,3,4}
proof
thus 5 = succ 4
.= {0,1,2,3,4} by Th52, ENUMSET1:10 ; ::_thesis: verum
end;

theorem Th54: :: CARD_1:54
6 = {0,1,2,3,4,5}
proof
thus 6 = succ 5
.= {0,1,2,3,4,5} by Th53, ENUMSET1:15 ; ::_thesis: verum
end;

theorem Th55: :: CARD_1:55
7 = {0,1,2,3,4,5,6}
proof
thus 7 = succ 6
.= {0,1,2,3,4,5,6} by Th54, ENUMSET1:21 ; ::_thesis: verum
end;

theorem Th56: :: CARD_1:56
8 = {0,1,2,3,4,5,6,7}
proof
thus 8 = succ 7
.= {0,1,2,3,4,5,6,7} by Th55, ENUMSET1:28 ; ::_thesis: verum
end;

theorem Th57: :: CARD_1:57
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 Th56, ENUMSET1:84 ; ::_thesis: verum
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 Th57, ENUMSET1:85 ; ::_thesis: verum
end;

theorem :: CARD_1:59
for f being Function st dom f is infinite & f is one-to-one holds
rng f is infinite
proof
let f be Function; ::_thesis: ( dom f is infinite & f is one-to-one implies rng f is infinite )
assume that
A1: dom f is infinite and
A2: f is one-to-one ; ::_thesis: rng f is infinite
 dom f, rng f are_equipotent by A2, WELLORD2:def_4;
hence  rng f is infinite by A1, Th38; ::_thesis: verum
end;


definition
let n be Nat;
func Segm n ->  set  equals :: CARD_1:def 6
n;
coherence
 n is set ;
end;

:: deftheorem  defines Segm CARD_1:def_6_:_
 for n being Nat holds Segm n = n;

definition
let n be Nat;
:: original: Segm
redefine func Segm n ->  Subset of omega;
coherence
 Segm n is Subset of omega
proof
 n in omega by ORDINAL1:def_12;
hence  Segm n is Subset of omega by ORDINAL1:16; ::_thesis: verum
end;
end;

theorem :: CARD_1:60
for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n by Lm3;

theorem :: CARD_1:61
for A being Ordinal holds
( A is finite iff A in omega ) by Lm4;

registration
cluster natural  ->  finite for set ;
coherence
 for b1 being set st b1 is natural holds
b1 is finite
proof
let a be set ; ::_thesis: ( a is natural implies a is finite )
assume  a in omega ; :: according to ORDINAL1:def_12 ::_thesis: a is finite
hence  a is finite ; ::_thesis: verum
end;
end;

registration
let A be infinite set ;
cluster bool A ->  infinite ;
coherence
 not bool A is finite
proof
defpred S1[ set ] means  ex y being set st A = {y};
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool A & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set holds
( x in union X iff x in A )
proof
let x be set ; ::_thesis: ( x in union X iff x in A )
thus  ( x in union X implies x in A ) ::_thesis: ( x in A implies x in union X )
proof
assume  x in union X ; ::_thesis: x in A
then consider B being set  such that
A2: x in B and
A3: B in X by TARSKI:def_4;
 B in bool A by A1, A3;
hence  x in A by A2; ::_thesis: verum
end;
assume  x in A ; ::_thesis: x in union X
then  {x} c= A by ZFMISC_1:31;
then A4: {x} in X by A1;
 x in {x} by TARSKI:def_1;
hence  x in union X by A4, TARSKI:def_4; ::_thesis: verum
end;
then A5: union X = A by TARSKI:1;
A6: for B being set st B in X holds
B is finite
proof
let B be set ; ::_thesis: ( B in X implies B is finite )
assume  B in X ; ::_thesis: B is finite
then  ex y being set st B = {y} by A1;
hence  B is finite ; ::_thesis: verum
end;
A7: X c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool A )
assume  x in X ; ::_thesis: x in bool A
hence  x in bool A by A1; ::_thesis: verum
end;
assume  bool A is finite ; ::_thesis: contradiction
hence  contradiction by A5, A6, A7, FINSET_1:7; ::_thesis: verum
end;
let B be non empty set ;
cluster[:A,B:] ->  infinite ;
coherence
 not [:A,B:] is finite
proof
deffunc H2( set ) ->  set = A `1 ;
consider f being Function such that
A8: dom f = [:A,B:] and
A9: for x being set st x in [:A,B:] holds
f . x = H2(x) from FUNCT_1:sch_3();
 for x being set holds
( x in rng f iff x in A )
proof
let x be set ; ::_thesis: ( x in rng f iff x in A )
thus  ( x in rng f implies x in A ) ::_thesis: ( x in A implies x in rng f )
proof
assume  x in rng f ; ::_thesis: x in A
then consider y being set  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  x in A by A8, A10, MCART_1:10; ::_thesis: verum
end;
set y = the Element of B;
assume  x in A ; ::_thesis: x in rng f
then A12: [x, the Element of B] in dom f by A8, ZFMISC_1:87;
then f . [x, the Element of B] = [x, the Element of B] `1 by A8, A9
.= x ;
hence  x in rng f by A12, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng f = A by TARSKI:1;
then A13: f .: [:A,B:] = A by A8, RELAT_1:113;
assume  [:A,B:] is finite ; ::_thesis: contradiction
hence  contradiction by A13; ::_thesis: verum
end;
cluster[:B,A:] ->  infinite ;
coherence
 not [:B,A:] is finite
proof
deffunc H2( set ) ->  set = A `2 ;
consider f being Function such that
A14: dom f = [:B,A:] and
A15: for x being set st x in [:B,A:] holds
f . x = H2(x) from FUNCT_1:sch_3();
 for y being set holds
( y in rng f iff y in A )
proof
let y be set ; ::_thesis: ( y in rng f iff y in A )
thus  ( y in rng f implies y in A ) ::_thesis: ( y in A implies y in rng f )
proof
assume  y in rng f ; ::_thesis: y in A
then consider x being set  such that
A16: x in dom f and
A17: f . x = y by FUNCT_1:def_3;
 y = x `2 by A14, A15, A16, A17;
hence  y in A by A14, A16, MCART_1:10; ::_thesis: verum
end;
set x = the Element of B;
assume  y in A ; ::_thesis: y in rng f
then A18: [ the Element of B,y] in dom f by A14, ZFMISC_1:87;
 [ the Element of B,y] `2 = y ;
then  f . [ the Element of B,y] = y by A14, A15, A18;
hence  y in rng f by A18, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng f = A by TARSKI:1;
then A19: f .: [:B,A:] = A by A14, RELAT_1:113;
assume  [:B,A:] is finite ; ::_thesis: contradiction
hence  contradiction by A19; ::_thesis: verum
end;
end;

registration
let X be infinite set ;
cluster infinite for Element of bool X;
existence
 ex b1 being Subset of X st b1 is infinite
proof
 X c= X ;
hence  ex b1 being Subset of X st b1 is infinite ; ::_thesis: verum
end;
end;

registration
cluster ordinal finite  ->  natural for set ;
coherence
 for b1 being number st b1 is finite & b1 is ordinal holds
b1 is natural
proof
let n be number ; ::_thesis: ( n is finite & n is ordinal implies n is natural )
assume  ( n is finite & n is ordinal ) ; ::_thesis: n is natural
then  n in omega by Lm4;
hence  n is natural ; ::_thesis: verum
end;
end;

theorem Th62: :: CARD_1:62
for f being Function holds card f = card (dom f)
proof
let f be Function; ::_thesis: card f = card (dom f)
 dom f,f are_equipotent
proof
deffunc H2( set ) ->  set = [$1,(f . $1)];
consider g being Function such that
A1: dom g = dom f and
A2: for x being set st x in dom f holds
g . x = H2(x) from FUNCT_1:sch_3();
take  g ; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & dom g = dom f & rng g = f )
thus  g is one-to-one ::_thesis: ( dom g = dom f & rng g = f )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom g or not b1 in dom g or not g . x = g . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume that
A3: x in dom g and
A4: y in dom g ; ::_thesis: ( not g . x = g . y or x = y )
assume  g . x = g . y ; ::_thesis: x = y
then [x,(f . x)] = g . y by A1, A2, A3
.= [y,(f . y)] by A1, A2, A4 ;
hence  x = y by XTUPLE_0:1; ::_thesis: verum
end;
thus  dom g = dom f by A1; ::_thesis: rng g = f
thus  rng g c= f :: according to XBOOLE_0:def_10 ::_thesis: f c= rng g
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng g or i in f )
assume  i in rng g ; ::_thesis: i in f
then consider x being set  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  i in f by A1, A5, A6, FUNCT_1:1; ::_thesis: verum
end;
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in f or [x,b1] in rng g )
let y be set ; ::_thesis: ( not [x,y] in f or [x,y] in rng g )
assume A7: [x,y] in f ; ::_thesis: [x,y] in rng g
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, A8;
hence  [x,y] in rng g by A1, A8, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card f = card (dom f) by Th5; ::_thesis: verum
end;

registration
let X be finite set ;
cluster RelIncl X ->  finite ;
coherence
 RelIncl X is finite
proof
 RelIncl X c= [:X,X:] by WELLORD2:23;
hence  RelIncl X is finite ; ::_thesis: verum
end;
end;

theorem :: CARD_1:63
for X being set st RelIncl X is finite holds
X is finite
proof
let X be set ; ::_thesis: ( RelIncl X is finite implies X is finite )
set R = RelIncl X;
assume  RelIncl X is finite ; ::_thesis: X is finite
then reconsider A = RelIncl X as finite Relation ;
 field A is finite ;
hence  X is finite by WELLORD2:def_1; ::_thesis: verum
end;

theorem :: CARD_1:64
for x being set
for k being Nat holds card (k --> x) = k
proof
let x be set ; ::_thesis: for k being Nat holds card (k --> x) = k
let k be Nat; ::_thesis: card (k --> x) = k
 dom (k --> x) = k by FUNCOP_1:13;
hence  card (k --> x) = card k by Th62
.= k by Def2 ;
::_thesis: verum
end;

begin

definition
let N, X be set ;
attrX is N -element  means :Def7: :: CARD_1:def 7
 card X = N;
end;

:: deftheorem Def7 defines -element CARD_1:def_7_:_
 for N, X being set holds
( X is N -element iff card X = N );

registration
let N be Cardinal;
clusterN -element for set ;
existence
 ex b1 being set st b1 is N -element
proof
take  N ; ::_thesis: N is N -element
thus  card N = N by Def2; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;

registration
cluster 0 -element  ->  empty for set ;
coherence
 for b1 being set st b1 is 0 -element holds
b1 is empty
proof
let X be set ; ::_thesis: ( X is 0 -element implies X is empty )
assume  X is 0 -element ; ::_thesis: X is empty
then  card X = 0 by Def7;
hence  X is empty ; ::_thesis: verum
end;
cluster empty  ->  0 -element for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is 0 -element
proof
let X be set ; ::_thesis: ( X is empty implies X is 0 -element )
assume  X is empty ; ::_thesis: X is 0 -element
then  card X = {} ;
hence  X is 0 -element by Def7; ::_thesis: verum
end;
end;

registration
let x be set ;
cluster{x} -> 1 -element ;
coherence
 {x} is 1 -element
proof
 1 = succ 0 ;
then  {x},1 are_equipotent by Th28;
hence  card {x} = 1 by Def2; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;

registration
let N be Cardinal;
cluster Relation-like Function-like N -element for set ;
existence
 ex b1 being Function st b1 is N -element
proof
take f = N --> {{}}; ::_thesis: f is N -element
 dom f = N by FUNCOP_1:13;
then  card (dom f) = N by Def2;
hence  card f = N by Th62; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;

registration
let N be Cardinal;
let f be N -element Function;
cluster dom f -> N -element ;
coherence
 dom f is N -element
proof
 card f = N by Def7;
hence  card (dom f) = N by Th62; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;

registration
cluster1 -element  ->  non empty trivial for set ;
coherence
 for b1 being set st b1 is 1 -element holds
( b1 is trivial & not b1 is empty )
proof
let X be set ; ::_thesis: ( X is 1 -element implies ( X is trivial & not X is empty ) )
assume  X is 1 -element ; ::_thesis: ( X is trivial & not X is empty )
then  card X = 1 by Def7
.= card {0} by Th30 ;
then  ex x being set st X = {x} by Th29;
hence  ( X is trivial & not X is empty ) ; ::_thesis: verum
end;
cluster non empty trivial  -> 1 -element for set ;
coherence
 for b1 being set st b1 is trivial & not b1 is empty holds
b1 is 1 -element
proof
let X be set ; ::_thesis: ( X is trivial & not X is empty implies X is 1 -element )
assume  ( X is trivial & not X is empty ) ; ::_thesis: X is 1 -element
then  ex x being set st X = {x} by ZFMISC_1:131;
hence  X is 1 -element ; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
cluster1 -element for Element of bool X;
existence
 ex b1 being Subset of X st b1 is 1 -element
proof
take  the non empty trivial Subset of X ; ::_thesis: the non empty trivial Subset of X is 1 -element
thus  the non empty trivial Subset of X is 1 -element ; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
mode Singleton of X is 1 -element Subset of X;
end;

theorem :: CARD_1:65
for X being non empty set
for A being Singleton of X ex x being Element of X st A = {x}
proof
let X be non empty set ; ::_thesis: for A being Singleton of X ex x being Element of X st A = {x}
let A be Singleton of X; ::_thesis: ex x being Element of X st A = {x}
consider x being set  such that
A1: A = {x} by ZFMISC_1:131;
 x in A by A1, TARSKI:def_1;
then reconsider x = x as Element of X ;
take  x ; ::_thesis: A = {x}
thus  A = {x} by A1; ::_thesis: verum
end;

theorem Th66: :: CARD_1:66
for X, Y being set holds
( card X c= card Y iff ex f being Function st X c= f .: Y )
proof
let X, Y be set ; ::_thesis: ( card X c= card Y iff ex f being Function st X c= f .: Y )
deffunc H2( set ) ->  set = $1;
thus  ( card X c= card Y implies ex f being Function st X c= f .: Y ) ::_thesis: ( ex f being Function st X c= f .: Y implies card X c= card Y )
proof
assume  card X c= card Y ; ::_thesis: ex f being Function st X c= f .: Y
then consider f being Function such that
A1: ( dom f = Y & X c= rng f ) by Th12;
take  f ; ::_thesis: X c= f .: Y
thus  X c= f .: Y by A1, RELAT_1:113; ::_thesis: verum
end;
given f being Function such that A2: X c= f .: Y ; ::_thesis: card X c= card Y
defpred S1[ set ] means $1 in dom f;
deffunc H3( set ) ->  set = f . $1;
consider g being Function such that
A3: ( dom g = Y & ( for x being set st x in Y holds
( ( S1[x] implies g . x = H3(x) ) & ( not S1[x] implies g . x = H2(x) ) ) ) ) from PARTFUN1:sch_1();
 X c= rng g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng g )
assume  x in X ; ::_thesis: x in rng g
then consider y being set  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  x in rng g by A3, A5, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card X c= card Y by A3, Th12; ::_thesis: verum
end;

theorem :: CARD_1:67
for X being set
for f being Function holds card (f .: X) c= card X by Th66;

theorem :: CARD_1:68
for X, Y being set st card X in card Y holds
Y \ X <> {}
proof
let X, Y be set ; ::_thesis: ( card X in card Y implies Y \ X <> {} )
assume that
A1: card X in card Y and
A2: Y \ X = {} ; ::_thesis: contradiction
 Y c= X by A2, XBOOLE_1:37;
then  card Y c= card X by Th11;
hence  contradiction by A1, ORDINAL1:5; ::_thesis: verum
end;

theorem :: CARD_1:69
for X, x being set holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
proof
let X, x be set ; ::_thesis: ( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
deffunc H2( set ) ->  set = [$1,x];
consider f being Function such that
A1: ( dom f = X & ( for y being set st y in X holds
f . y = H2(y) ) ) from FUNCT_1:sch_3();
thus  X,[:X,{x}:] are_equipotent ::_thesis: card X = card [:X,{x}:]
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = [:X,{x}:] )
thus  f is one-to-one ::_thesis: ( dom f = X & rng f = [:X,{x}:] )
proof
let y be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y in dom f or not b1 in dom f or not f . y = f . b1 or y = b1 )
let z be set ; ::_thesis: ( not y in dom f or not z in dom f or not f . y = f . z or y = z )
assume that
A2: ( y in dom f & z in dom f ) and
A3: f . y = f . z ; ::_thesis: y = z
A4: [y,x] `1 = y ;
 ( f . y = [y,x] & f . z = [z,x] ) by A1, A2;
hence  y = z by A3, A4, MCART_1:7; ::_thesis: verum
end;
thus  dom f = X by A1; ::_thesis: rng f = [:X,{x}:]
thus  rng f c= [:X,{x}:] :: according to XBOOLE_0:def_10 ::_thesis: [:X,{x}:] c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [:X,{x}:] )
A5: x in {x} by TARSKI:def_1;
assume  y in rng f ; ::_thesis: y in [:X,{x}:]
then consider z being set  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  y in [:X,{x}:] by A1, A6, A5, ZFMISC_1:87; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:X,{x}:] or y in rng f )
assume  y in [:X,{x}:] ; ::_thesis: y in rng f
then consider y1, y2 being set  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  y in rng f by A1, A8, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card X = card [:X,{x}:] by Th5; ::_thesis: verum
end;

theorem :: CARD_1:70
for f being Function st f is one-to-one holds
card (dom f) = card (rng f)
proof
let f be Function; ::_thesis: ( f is one-to-one implies card (dom f) = card (rng f) )
assume  f is one-to-one ; ::_thesis: card (dom f) = card (rng f)
then A1: dom f,f .: (dom f) are_equipotent by Th33;
 f .: (dom f) = rng f by RELAT_1:113;
hence  card (dom f) = card (rng f) by A1, Th5; ::_thesis: verum
end;