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