:: CARD_4 semantic presentation
begin
theorem :: CARD_4:1
for X being set st X is finite holds
X is countable ;
theorem :: CARD_4:2
omega is countable ;
theorem Th3: :: CARD_4:3
for n being Nat
for r being Real holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
proof
let n be Nat; ::_thesis: for r being Real holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
let r be Real; ::_thesis: ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
defpred S1[ Nat] means ( ( r <> 0 or $1 = 0 ) iff r |^ $1 <> 0 );
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: r |^ (k + 1) = (r |^ k) * r by NEWTON:6;
assume S1[k] ; ::_thesis: S1[k + 1]
hence S1[k + 1] by A2; ::_thesis: verum
end;
A3: S1[ 0 ] by NEWTON:4;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 ) ; ::_thesis: verum
end;
Lm1: for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2
proof
let n1, m1, n2, m2 be Nat; ::_thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies n1 <= n2 )
assume A1: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; ::_thesis: n1 <= n2
assume A2: n1 > n2 ; ::_thesis: contradiction
then consider n being Nat such that
A3: n1 = n2 + n by NAT_1:10;
n <> 0 by A2, A3;
then consider k being Nat such that
A4: n = k + 1 by NAT_1:6;
A5: 2 |^ n2 <> 0 by Th3;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
2 |^ n1 = (2 |^ n2) * (2 |^ (k + 1)) by A3, A4, NEWTON:8;
then (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 |^ (k + 1)) * ((2 * m1) + 1)) ;
then (2 |^ (k + 1)) * ((2 * m1) + 1) = (2 * m2) + 1 by A1, A5, XCMPLX_1:5;
then (2 * m2) + 1 = ((2 |^ k) * (2 |^ 1)) * ((2 * m1) + 1) by NEWTON:8
.= (2 * (2 |^ k)) * ((2 * m1) + 1) by NEWTON:5
.= 2 * ((2 |^ k) * ((2 * m1) + 1)) ;
then A6: 2 divides (2 * m2) + 1 by NAT_D:def_3;
2 divides 2 * m2 by NAT_D:def_3;
hence contradiction by A6, NAT_D:7, NAT_D:10; ::_thesis: verum
end;
theorem Th4: :: CARD_4:4
for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
( n1 = n2 & m1 = m2 )
proof
let n1, m1, n2, m2 be Nat; ::_thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies ( n1 = n2 & m1 = m2 ) )
A1: 2 |^ n1 <> 0 by Th3;
assume A2: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; ::_thesis: ( n1 = n2 & m1 = m2 )
then ( n1 <= n2 & n2 <= n1 ) by Lm1;
hence n1 = n2 by XXREAL_0:1; ::_thesis: m1 = m2
then (2 * m1) + 1 = (2 * m2) + 1 by A2, A1, XCMPLX_1:5;
hence m1 = m2 ; ::_thesis: verum
end;
Lm2: for x being set st x in [:NAT,NAT:] holds
ex n1, n2 being Element of NAT st x = [n1,n2]
proof
let x be set ; ::_thesis: ( x in [:NAT,NAT:] implies ex n1, n2 being Element of NAT st x = [n1,n2] )
assume A1: x in [:NAT,NAT:] ; ::_thesis: ex n1, n2 being Element of NAT st x = [n1,n2]
then reconsider n1 = x `1 , n2 = x `2 as Element of NAT by MCART_1:10;
take n1 ; ::_thesis: ex n2 being Element of NAT st x = [n1,n2]
take n2 ; ::_thesis: x = [n1,n2]
thus x = [n1,n2] by A1, MCART_1:21; ::_thesis: verum
end;
theorem Th5: :: CARD_4:5
( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] )
proof
[:NAT,{0}:] c= [:NAT,NAT:] by ZFMISC_1:95;
then card [:NAT,{0}:] c= card [:NAT,NAT:] by CARD_1:11;
then A1: card NAT c= card [:NAT,NAT:] by CARD_1:69;
deffunc H1( Element of NAT , Element of NAT ) -> Element of NAT = (2 |^ $1) * ((2 * $2) + 1);
consider f being Function of [:NAT,NAT:],NAT such that
A2: for n, m being Element of NAT holds f . (n,m) = H1(n,m) from BINOP_1:sch_4();
A3: 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 x in dom f ; ::_thesis: ( not y in dom f or not f . x = f . y or x = y )
then consider n1, m1 being Element of NAT such that
A4: x = [n1,m1] by Lm2;
assume y in dom f ; ::_thesis: ( not f . x = f . y or x = y )
then consider n2, m2 being Element of NAT such that
A5: y = [n2,m2] by Lm2;
assume A6: f . x = f . y ; ::_thesis: x = y
A7: (2 |^ n1) * ((2 * m1) + 1) = f . (n1,m1) by A2
.= f . (n2,m2) by A4, A5, A6
.= (2 |^ n2) * ((2 * m2) + 1) by A2 ;
then n1 = n2 by Th4;
hence x = y by A4, A5, A7, Th4; ::_thesis: verum
end;
( dom f = [:NAT,NAT:] & rng f c= NAT ) by FUNCT_2:def_1;
then card [:NAT,NAT:] c= card NAT by A3, CARD_1:10;
then card NAT = card [:NAT,NAT:] by A1, XBOOLE_0:def_10;
hence ( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] ) by CARD_1:5; ::_thesis: verum
end;
theorem Th6: :: CARD_4:6
omega *` omega = omega by Th5, CARD_1:47, CARD_2:def_2;
theorem Th7: :: CARD_4:7
for X, Y being set st X is countable & Y is countable holds
[:X,Y:] is countable
proof
let X, Y be set ; ::_thesis: ( X is countable & Y is countable implies [:X,Y:] is countable )
assume ( card X c= omega & card Y c= omega ) ; :: according to CARD_3:def_14 ::_thesis: [:X,Y:] is countable
then [:(card X),(card Y):] c= [:omega,omega:] by ZFMISC_1:96;
then card [:(card X),(card Y):] c= card [:omega,omega:] by CARD_1:11;
then card [:(card X),(card Y):] c= omega *` omega by CARD_2:def_2;
hence card [:X,Y:] c= omega by Th6, CARD_2:7; :: according to CARD_3:def_14 ::_thesis: verum
end;
theorem Th8: :: CARD_4:8
for D being non empty set holds
( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D )
proof
let D be non empty set ; ::_thesis: ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D )
deffunc H1( set ) -> set = <*$1*>;
consider f being Function such that
A1: ( dom f = D & ( for x being set st x in D holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
D,1 -tuples_on D are_equipotent
proof
take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = D & rng f = 1 -tuples_on D )
thus f is one-to-one ::_thesis: ( dom f = D & rng f = 1 -tuples_on D )
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 ( x in dom f & y in dom f ) ; ::_thesis: ( not f . x = f . y or x = y )
then A2: ( f . x = <*x*> & f . y = <*y*> ) by A1;
<*x*> . 1 = x by FINSEQ_1:def_8;
hence ( not f . x = f . y or x = y ) by A2, FINSEQ_1:def_8; ::_thesis: verum
end;
thus dom f = D by A1; ::_thesis: rng f = 1 -tuples_on D
thus rng f c= 1 -tuples_on D :: according to XBOOLE_0:def_10 ::_thesis: 1 -tuples_on D c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in 1 -tuples_on D )
assume x in rng f ; ::_thesis: x in 1 -tuples_on D
then consider y being set such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of D by A1, A3;
x = <*y*> by A1, A4;
then x in { <*d*> where d is Element of D : verum } ;
hence x in 1 -tuples_on D by FINSEQ_2:96; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 1 -tuples_on D or x in rng f )
assume x in 1 -tuples_on D ; ::_thesis: x in rng f
then reconsider y = x as Element of 1 -tuples_on D ;
consider z being Element of D such that
A5: y = <*z*> by FINSEQ_2:97;
x = f . z by A1, A5;
hence x in rng f by A1, FUNCT_1:def_3; ::_thesis: verum
end;
hence ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D ) by CARD_1:5; ::_thesis: verum
end;
theorem Th9: :: CARD_4:9
for D being non empty set
for n, m being Element of NAT holds
( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )
proof
let D be non empty set ; ::_thesis: for n, m being Element of NAT holds
( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )
let n, m be Element of NAT ; ::_thesis: ( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )
defpred S1[ set , set ] means ex p being Element of n -tuples_on D ex q being Element of m -tuples_on D st
( $1 = [p,q] & $2 = p ^ q );
set A = [:(n -tuples_on D),(m -tuples_on D):];
set B = (n + m) -tuples_on D;
A1: for x being set st x in [:(n -tuples_on D),(m -tuples_on D):] holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in [:(n -tuples_on D),(m -tuples_on D):] implies ex y being set st S1[x,y] )
assume A2: x in [:(n -tuples_on D),(m -tuples_on D):] ; ::_thesis: ex y being set st S1[x,y]
then reconsider p = x `1 as Element of n -tuples_on D by MCART_1:10;
reconsider q = x `2 as Element of m -tuples_on D by A2, MCART_1:10;
reconsider y = p ^ q as set ;
take y ; ::_thesis: S1[x,y]
x = [(x `1),(x `2)] by A2, MCART_1:21;
hence S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = [:(n -tuples_on D),(m -tuples_on D):] & ( for x being set st x in [:(n -tuples_on D),(m -tuples_on D):] holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
thus [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent ::_thesis: card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D)
proof
take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = [:(n -tuples_on D),(m -tuples_on D):] & rng f = (n + m) -tuples_on D )
thus f is one-to-one ::_thesis: ( dom f = [:(n -tuples_on D),(m -tuples_on D):] & rng f = (n + m) -tuples_on D )
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 x in dom f ; ::_thesis: ( not y in dom f or not f . x = f . y or x = y )
then consider p1 being Element of n -tuples_on D, q1 being Element of m -tuples_on D such that
A4: x = [p1,q1] and
A5: f . x = p1 ^ q1 by A3;
assume y in dom f ; ::_thesis: ( not f . x = f . y or x = y )
then consider p2 being Element of n -tuples_on D, q2 being Element of m -tuples_on D such that
A6: y = [p2,q2] and
A7: f . y = p2 ^ q2 by A3;
assume A8: f . x = f . y ; ::_thesis: x = y
A9: ( len p1 = n & len p2 = n ) by CARD_1:def_7;
then consider p being FinSequence such that
A10: p1 ^ p = p2 by A5, A7, A8, FINSEQ_1:47;
consider q being FinSequence such that
A11: p2 ^ q = p1 by A5, A7, A8, A9, FINSEQ_1:47;
(len p1) + 0 = (len (p1 ^ p)) + (len q) by A10, A11, FINSEQ_1:22
.= ((len p1) + (len p)) + (len q) by FINSEQ_1:22
.= (len p1) + ((len p) + (len q)) ;
then p = {} ;
then p1 = p2 by A10, FINSEQ_1:34;
hence x = y by A4, A5, A6, A7, A8, FINSEQ_1:33; ::_thesis: verum
end;
thus dom f = [:(n -tuples_on D),(m -tuples_on D):] by A3; ::_thesis: rng f = (n + m) -tuples_on D
thus rng f c= (n + m) -tuples_on D :: according to XBOOLE_0:def_10 ::_thesis: (n + m) -tuples_on D c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in (n + m) -tuples_on D )
assume x in rng f ; ::_thesis: x in (n + m) -tuples_on D
then consider y being set such that
A12: ( y in dom f & x = f . y ) by FUNCT_1:def_3;
ex p being Element of n -tuples_on D ex q being Element of m -tuples_on D st
( y = [p,q] & x = p ^ q ) by A3, A12;
then x is Tuple of n + m,D ;
then x is Element of (n + m) -tuples_on D by FINSEQ_2:131;
hence x in (n + m) -tuples_on D ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (n + m) -tuples_on D or x in rng f )
assume x in (n + m) -tuples_on D ; ::_thesis: x in rng f
then reconsider x = x as Element of (n + m) -tuples_on D ;
consider p being Element of n -tuples_on D, q being Element of m -tuples_on D such that
A13: x = p ^ q by FINSEQ_2:106;
consider p1 being Element of n -tuples_on D, q1 being Element of m -tuples_on D such that
A14: [p,q] = [p1,q1] and
A15: f . [p,q] = p1 ^ q1 by A3;
( p1 = p & q1 = q ) by A14, XTUPLE_0:1;
hence x in rng f by A3, A13, A15, FUNCT_1:def_3; ::_thesis: verum
end;
hence card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) by CARD_1:5; ::_thesis: verum
end;
theorem Th10: :: CARD_4:10
for D being non empty set
for n being Element of NAT st D is countable holds
n -tuples_on D is countable
proof
let D be non empty set ; ::_thesis: for n being Element of NAT st D is countable holds
n -tuples_on D is countable
let n be Element of NAT ; ::_thesis: ( D is countable implies n -tuples_on D is countable )
defpred S1[ Nat] means $1 -tuples_on D is countable ;
assume card D c= omega ; :: according to CARD_3:def_14 ::_thesis: n -tuples_on D is countable
then card (1 -tuples_on D) c= omega by Th8;
then A1: 1 -tuples_on D is countable by CARD_3:def_14;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then [:(k -tuples_on D),(1 -tuples_on D):] is countable by A1, Th7;
then A3: card [:(k -tuples_on D),(1 -tuples_on D):] c= omega by CARD_3:def_14;
k in NAT by ORDINAL1:def_12;
then card [:(k -tuples_on D),(1 -tuples_on D):] = card ((k + 1) -tuples_on D) by Th9;
hence S1[k + 1] by A3, CARD_3:def_14; ::_thesis: verum
end;
{(<*> D)} is countable ;
then A4: S1[ 0 ] by FINSEQ_2:94;
for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2);
hence n -tuples_on D is countable ; ::_thesis: verum
end;
theorem Th11: :: CARD_4:11
for f being Function st dom f is countable & ( for x being set st x in dom f holds
f . x is countable ) holds
Union f is countable
proof
let f be Function; ::_thesis: ( dom f is countable & ( for x being set st x in dom f holds
f . x is countable ) implies Union f is countable )
assume that
A1: card (dom f) c= omega and
A2: for x being set st x in dom f holds
f . x is countable ; :: according to CARD_3:def_14 ::_thesis: Union f is countable
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
card_(f_._x)_c=_omega
let x be set ; ::_thesis: ( x in dom f implies card (f . x) c= omega )
assume x in dom f ; ::_thesis: card (f . x) c= omega
then f . x is countable by A2;
hence card (f . x) c= omega by CARD_3:def_14; ::_thesis: verum
end;
hence card (Union f) c= omega by A1, Th6, CARD_2:86; :: according to CARD_3:def_14 ::_thesis: verum
end;
theorem :: CARD_4:12
for X being set st X is countable & ( for Y being set st Y in X holds
Y is countable ) holds
union X is countable
proof
let X be set ; ::_thesis: ( X is countable & ( for Y being set st Y in X holds
Y is countable ) implies union X is countable )
assume that
A1: card X c= omega and
A2: for Y being set st Y in X holds
Y is countable ; :: according to CARD_3:def_14 ::_thesis: union X is countable
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
card_Y_c=_omega
let Y be set ; ::_thesis: ( Y in X implies card Y c= omega )
assume Y in X ; ::_thesis: card Y c= omega
then Y is countable by A2;
hence card Y c= omega by CARD_3:def_14; ::_thesis: verum
end;
hence card (union X) c= omega by A1, Th6, CARD_2:87; :: according to CARD_3:def_14 ::_thesis: verum
end;
theorem :: CARD_4:13
for D being non empty set st D is countable holds
D * is countable
proof
let D be non empty set ; ::_thesis: ( D is countable implies D * is countable )
defpred S1[ set , set ] means ex n being Element of NAT st
( $1 = n & $2 = n -tuples_on D );
A1: for x being set st x in NAT holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] )
assume x in NAT ; ::_thesis: ex y being set st S1[x,y]
then reconsider n = x as Element of NAT ;
reconsider y = n -tuples_on D as set ;
take y ; ::_thesis: S1[x,y]
take n ; ::_thesis: ( x = n & y = n -tuples_on D )
thus ( x = n & y = n -tuples_on D ) ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = NAT & ( for x being set st x in NAT holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
A3: D * = union { (k -tuples_on D) where k is Element of NAT : verum } by FINSEQ_2:108;
A4: Union f = D *
proof
thus Union f c= D * :: according to XBOOLE_0:def_10 ::_thesis: D * c= Union f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union f or x in D * )
assume x in Union f ; ::_thesis: x in D *
then consider X being set such that
A5: x in X and
A6: X in rng f by TARSKI:def_4;
consider y being set such that
A7: y in dom f and
A8: X = f . y by A6, FUNCT_1:def_3;
reconsider y = y as Element of NAT by A2, A7;
ex n being Element of NAT st
( y = n & X = n -tuples_on D ) by A2, A8;
then X in { (k -tuples_on D) where k is Element of NAT : verum } ;
hence x in D * by A3, A5, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D * or x in Union f )
assume x in D * ; ::_thesis: x in Union f
then consider X being set such that
A9: ( x in X & X in { (k -tuples_on D) where k is Element of NAT : verum } ) by A3, TARSKI:def_4;
consider n being Element of NAT such that
A10: X = n -tuples_on D by A9;
ex k being Element of NAT st
( n = k & f . n = k -tuples_on D ) by A2;
then X in rng f by A2, A10, FUNCT_1:def_3;
hence x in Union f by A9, TARSKI:def_4; ::_thesis: verum
end;
assume A11: D is countable ; ::_thesis: D * is countable
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_is_countable
let x be set ; ::_thesis: ( x in dom f implies f . x is countable )
assume x in dom f ; ::_thesis: f . x is countable
then ex n being Element of NAT st
( x = n & f . x = n -tuples_on D ) by A2;
hence f . x is countable by A11, Th10; ::_thesis: verum
end;
hence D * is countable by A2, A4, Th11; ::_thesis: verum
end;
theorem :: CARD_4:14
for D being non empty set holds omega c= card (D *)
proof
let D be non empty set ; ::_thesis: omega c= card (D *)
defpred S1[ set , set ] means ex p being FinSequence st
( $1 = p & $2 = len p );
A1: ( {} in D * & len {} = 0 ) by FINSEQ_1:49;
A2: for x being set st x in D * holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in D * implies ex y being set st S1[x,y] )
assume x in D * ; ::_thesis: ex y being set st S1[x,y]
then reconsider p = x as Element of D * ;
reconsider p = p as FinSequence ;
reconsider y = len p as set ;
take y ; ::_thesis: S1[x,y]
take p ; ::_thesis: ( x = p & y = len p )
thus ( x = p & y = len p ) ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = D * & ( for x being set st x in D * holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A2);
defpred S2[ Nat] means $1 in f .: (D *);
A4: for n being Nat st S2[n] holds
S2[n + 1]
proof
set y = the Element of D;
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume n in f .: (D *) ; ::_thesis: S2[n + 1]
then consider x being set such that
A5: x in dom f and
A6: x in D * and
A7: n = f . x by FUNCT_1:def_6;
consider p being FinSequence such that
A8: x = p and
A9: n = len p by A3, A5, A7;
reconsider p = p as FinSequence of D by A6, A8, FINSEQ_1:def_11;
A10: len (p ^ <* the Element of D*>) = n + (len <* the Element of D*>) by A9, FINSEQ_1:22
.= n + 1 by FINSEQ_1:40 ;
A11: p ^ <* the Element of D*> in D * by FINSEQ_1:def_11;
then ex q being FinSequence st
( p ^ <* the Element of D*> = q & f . (p ^ <* the Element of D*>) = len q ) by A3;
hence S2[n + 1] by A3, A11, A10, FUNCT_1:def_6; ::_thesis: verum
end;
ex p being FinSequence st
( {} = p & f . {} = len p ) by A3, FINSEQ_1:49;
then A12: S2[ 0 ] by A3, A1, FUNCT_1:def_6;
A13: for n being Nat holds S2[n] from NAT_1:sch_2(A12, A4);
NAT c= f .: (D *)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in f .: (D *) )
assume x in NAT ; ::_thesis: x in f .: (D *)
then reconsider n = x as Element of NAT ;
n in f .: (D *) by A13;
hence x in f .: (D *) ; ::_thesis: verum
end;
hence omega c= card (D *) by CARD_1:47, CARD_1:66; ::_thesis: verum
end;
scheme :: CARD_4:sch 1
FraenCoun1{ F1( set ) -> set , P1[ set ] } :
{ F1(n) where n is Element of NAT : P1[n] } is countable
proof
consider f being Function such that
A1: ( dom f = NAT & ( for x being set st x in NAT holds
f . x = F1(x) ) ) from FUNCT_1:sch_3();
{ F1(n) where n is Element of NAT : P1[n] } c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1(n) where n is Element of NAT : P1[n] } or x in rng f )
assume x in { F1(n) where n is Element of NAT : P1[n] } ; ::_thesis: x in rng f
then consider n being Element of NAT such that
A2: x = F1(n) and
P1[n] ;
f . n = x by A1, A2;
hence x in rng f by A1, FUNCT_1:def_3; ::_thesis: verum
end;
hence { F1(n) where n is Element of NAT : P1[n] } is countable by A1, CARD_3:93; ::_thesis: verum
end;
scheme :: CARD_4:sch 2
FraenCoun2{ F1( set , set ) -> set , P1[ set , set ] } :
{ F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } is countable
proof
consider N being Function such that
N is one-to-one and
A1: dom N = NAT and
A2: rng N = [:NAT,NAT:] by Th5, WELLORD2:def_4;
deffunc H1( set ) -> set = F1(((N . $1) `1),((N . $1) `2));
consider f being Function such that
A3: ( dom f = NAT & ( for x being set st x in NAT holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
{ F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } or x in rng f )
assume x in { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } ; ::_thesis: x in rng f
then consider n1, n2 being Element of NAT such that
A4: x = F1(n1,n2) and
P1[n1,n2] ;
consider y being set such that
A5: y in dom N and
A6: [n1,n2] = N . y by A2, FUNCT_1:def_3;
( [n1,n2] `1 = n1 & [n1,n2] `2 = n2 ) ;
then x = f . y by A1, A3, A4, A5, A6;
hence x in rng f by A1, A3, A5, FUNCT_1:def_3; ::_thesis: verum
end;
hence { F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2] } is countable by A3, CARD_3:93; ::_thesis: verum
end;
scheme :: CARD_4:sch 3
FraenCoun3{ F1( set , set , set ) -> set , P1[ set , set , set ] } :
{ F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } is countable
proof
[:NAT,NAT:],[:[:NAT,NAT:],NAT:] are_equipotent by Th5, CARD_2:8;
then A1: NAT ,[:[:NAT,NAT:],NAT:] are_equipotent by Th5, WELLORD2:15;
[:[:NAT,NAT:],NAT:] = [:NAT,NAT,NAT:] by ZFMISC_1:def_3;
then consider N being Function such that
N is one-to-one and
A2: dom N = NAT and
A3: rng N = [:NAT,NAT,NAT:] by A1, WELLORD2:def_4;
deffunc H1( set ) -> set = F1((((N . $1) `1) `1),(((N . $1) `1) `2),((N . $1) `2));
consider f being Function such that
A4: ( dom f = NAT & ( for x being set st x in NAT holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
{ F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } c= rng f
proof
reconsider NAT9 = NAT as non empty set ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } or x in rng f )
assume x in { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } ; ::_thesis: x in rng f
then consider n1, n2, n3 being Element of NAT such that
A5: x = F1(n1,n2,n3) and
P1[n1,n2,n3] ;
reconsider n1 = n1, n2 = n2, n3 = n3 as Element of NAT9 ;
A6: ( [n1,n2,n3] `3_3 = n3 & [n1,n2,n3] `1_3 = ([n1,n2,n3] `1) `1 ) ;
consider y being set such that
A8: y in dom N and
A9: [n1,n2,n3] = N . y by A3, FUNCT_1:def_3;
( [n1,n2,n3] `1_3 = n1 & [n1,n2,n3] `2_3 = n2 ) ;
then x = f . y by A2, A4, A5, A8, A9, A6;
hence x in rng f by A2, A4, A8, FUNCT_1:def_3; ::_thesis: verum
end;
hence { F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3] } is countable by A4, CARD_3:93; ::_thesis: verum
end;
theorem Th15: :: CARD_4:15
for M being Cardinal st not M is finite holds
M *` M = M
proof
let M be Cardinal; ::_thesis: ( not M is finite implies M *` M = M )
defpred S1[ set ] means ex f being Function st
( f = $1 & f is one-to-one & dom f = [:(rng f),(rng f):] );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in PFuncs ([:M,M:],M) & S1[x] ) ) from XBOOLE_0:sch_1();
A2: for x being set st x in X holds
x is Function
proof
let x be set ; ::_thesis: ( x in X implies x is Function )
assume x in X ; ::_thesis: x is Function
then ex f being Function st
( f = x & f is one-to-one & dom f = [:(rng f),(rng f):] ) by A1;
hence x is Function ; ::_thesis: verum
end;
A3: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X
proof
let Z be set ; ::_thesis: ( Z <> {} & Z c= X & Z is c=-linear implies union Z in X )
assume that
Z <> {} and
A4: Z c= X and
A5: Z is c=-linear ; ::_thesis: union Z in X
( union Z is Relation-like & union Z is Function-like )
proof
set F = union Z;
thus for x being set st x in union Z holds
ex y1, y2 being set st [y1,y2] = x :: according to RELAT_1:def_1 ::_thesis: union Z is Function-like
proof
let x be set ; ::_thesis: ( x in union Z implies ex y1, y2 being set st [y1,y2] = x )
assume x in union Z ; ::_thesis: ex y1, y2 being set st [y1,y2] = x
then consider Y being set such that
A6: x in Y and
A7: Y in Z by TARSKI:def_4;
reconsider f = Y as Function by A2, A4, A7;
for x being set st x in f holds
ex y1, y2 being set st [y1,y2] = x by RELAT_1:def_1;
hence ex y1, y2 being set st [y1,y2] = x by A6; ::_thesis: verum
end;
let x be set ; :: according to FUNCT_1:def_1 ::_thesis: for b1, b2 being set holds
( not [x,b1] in union Z or not [x,b2] in union Z or b1 = b2 )
let y1, y2 be set ; ::_thesis: ( not [x,y1] in union Z or not [x,y2] in union Z or y1 = y2 )
assume [x,y1] in union Z ; ::_thesis: ( not [x,y2] in union Z or y1 = y2 )
then consider X1 being set such that
A8: [x,y1] in X1 and
A9: X1 in Z by TARSKI:def_4;
assume [x,y2] in union Z ; ::_thesis: y1 = y2
then consider X2 being set such that
A10: [x,y2] in X2 and
A11: X2 in Z by TARSKI:def_4;
reconsider f1 = X1, f2 = X2 as Function by A2, A4, A9, A11;
X1,X2 are_c=-comparable by A5, A9, A11, ORDINAL1:def_8;
then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
then ( ( [x,y2] in X1 & ( for x, y1, y2 being set st [x,y1] in f1 & [x,y2] in f1 holds
y1 = y2 ) ) or ( [x,y1] in X2 & ( for x, y1, y2 being set st [x,y1] in f2 & [x,y2] in f2 holds
y1 = y2 ) ) ) by A8, A10, FUNCT_1:def_1;
hence y1 = y2 by A8, A10; ::_thesis: verum
end;
then reconsider f = union Z as Function ;
A12: f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A13: x1 in dom f and
A14: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
[x1,(f . x1)] in f by A13, FUNCT_1:1;
then consider X1 being set such that
A15: [x1,(f . x1)] in X1 and
A16: X1 in Z by TARSKI:def_4;
[x2,(f . x2)] in f by A14, FUNCT_1:1;
then consider X2 being set such that
A17: [x2,(f . x2)] in X2 and
A18: X2 in Z by TARSKI:def_4;
consider f2 being Function such that
A19: f2 = X2 and
A20: f2 is one-to-one and
dom f2 = [:(rng f2),(rng f2):] by A1, A4, A18;
consider f1 being Function such that
A21: f1 = X1 and
A22: f1 is one-to-one and
dom f1 = [:(rng f1),(rng f1):] by A1, A4, A16;
X1,X2 are_c=-comparable by A5, A16, A18, ORDINAL1:def_8;
then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
then ( ( x1 in dom f1 & x2 in dom f1 & f . x1 = f1 . x1 & f . x2 = f1 . x2 ) or ( x1 in dom f2 & x2 in dom f2 & f . x1 = f2 . x1 & f . x2 = f2 . x2 ) ) by A15, A17, A21, A19, FUNCT_1:1;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A22, A20, FUNCT_1:def_4; ::_thesis: verum
end;
A23: dom f = [:(rng f),(rng f):]
proof
thus dom f c= [:(rng f),(rng f):] :: according to XBOOLE_0:def_10 ::_thesis: [:(rng f),(rng f):] c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in [:(rng f),(rng f):] )
assume x in dom f ; ::_thesis: x in [:(rng f),(rng f):]
then [x,(f . x)] in f by FUNCT_1:def_2;
then consider Y being set such that
A24: [x,(f . x)] in Y and
A25: Y in Z by TARSKI:def_4;
consider g being Function such that
A26: g = Y and
g is one-to-one and
A27: dom g = [:(rng g),(rng g):] by A1, A4, A25;
g c= f by A25, A26, ZFMISC_1:74;
then rng g c= rng f by RELAT_1:11;
then A28: dom g c= [:(rng f),(rng f):] by A27, ZFMISC_1:96;
x in dom g by A24, A26, FUNCT_1:1;
hence x in [:(rng f),(rng f):] by A28; ::_thesis: verum
end;
let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in [:(rng f),(rng f):] or [x1,x2] in dom f )
assume A29: [x1,x2] in [:(rng f),(rng f):] ; ::_thesis: [x1,x2] in dom f
[x1,x2] `1 in rng f by A29, MCART_1:10;
then consider y1 being set such that
A31: ( y1 in dom f & [x1,x2] `1 = f . y1 ) by FUNCT_1:def_3;
[x1,x2] `2 in rng f by A29, MCART_1:10;
then consider y2 being set such that
A32: ( y2 in dom f & [x1,x2] `2 = f . y2 ) by FUNCT_1:def_3;
[y2,([x1,x2] `2)] in f by A32, FUNCT_1:1;
then consider X2 being set such that
A33: [y2,([x1,x2] `2)] in X2 and
A34: X2 in Z by TARSKI:def_4;
consider f2 being Function such that
A35: f2 = X2 and
f2 is one-to-one and
A36: dom f2 = [:(rng f2),(rng f2):] by A1, A4, A34;
f2 c= f by A34, A35, ZFMISC_1:74;
then A37: dom f2 c= dom f by RELAT_1:11;
[y1,([x1,x2] `1)] in f by A31, FUNCT_1:1;
then consider X1 being set such that
A38: [y1,([x1,x2] `1)] in X1 and
A39: X1 in Z by TARSKI:def_4;
consider f1 being Function such that
A40: f1 = X1 and
f1 is one-to-one and
A41: dom f1 = [:(rng f1),(rng f1):] by A1, A4, A39;
X1,X2 are_c=-comparable by A5, A39, A34, ORDINAL1:def_8;
then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
then ( ( y1 in dom f1 & y2 in dom f1 & f1 . y1 = [x1,x2] `1 & f1 . y2 = [x1,x2] `2 ) or ( y1 in dom f2 & y2 in dom f2 & f2 . y1 = [x1,x2] `1 & f2 . y2 = [x1,x2] `2 ) ) by A38, A33, A40, A35, FUNCT_1:1;
then ( ( [x1,x2] `1 in rng f1 & [x1,x2] `2 in rng f1 ) or ( [x1,x2] `1 in rng f2 & [x1,x2] `2 in rng f2 ) ) by FUNCT_1:def_3;
then A42: ( [x1,x2] in dom f1 or [x1,x2] in dom f2 ) by A41, A36, ZFMISC_1:87;
f1 c= f by A39, A40, ZFMISC_1:74;
then dom f1 c= dom f by RELAT_1:11;
hence [x1,x2] in dom f by A42, A37; ::_thesis: verum
end;
A43: rng f c= M
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in M )
assume y in rng f ; ::_thesis: y in M
then consider x being set such that
A44: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
[x,y] in union Z by A44, FUNCT_1:def_2;
then consider Y being set such that
A45: [x,y] in Y and
A46: Y in Z by TARSKI:def_4;
Y in PFuncs ([:M,M:],M) by A1, A4, A46;
then consider g being Function such that
A47: Y = g and
dom g c= [:M,M:] and
A48: rng g c= M by PARTFUN1:def_3;
( x in dom g & g . x = y ) by A45, A47, FUNCT_1:1;
then y in rng g by FUNCT_1:def_3;
hence y in M by A48; ::_thesis: verum
end;
dom f c= [:M,M:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in [:M,M:] )
assume x in dom f ; ::_thesis: x in [:M,M:]
then [x,(f . x)] in union Z by FUNCT_1:def_2;
then consider Y being set such that
A49: [x,(f . x)] in Y and
A50: Y in Z by TARSKI:def_4;
Y in PFuncs ([:M,M:],M) by A1, A4, A50;
then consider g being Function such that
A51: Y = g and
A52: dom g c= [:M,M:] and
rng g c= M by PARTFUN1:def_3;
x in dom g by A49, A51, FUNCT_1:1;
hence x in [:M,M:] by A52; ::_thesis: verum
end;
then f in PFuncs ([:M,M:],M) by A43, PARTFUN1:def_3;
hence union Z in X by A1, A12, A23; ::_thesis: verum
end;
consider f being Function such that
A53: f is one-to-one and
A54: ( dom f = [:omega,omega:] & rng f = omega ) by Th5, WELLORD2:def_4;
assume A55: not M is finite ; ::_thesis: M *` M = M
then not M in omega ;
then A56: omega c= M by CARD_1:4;
then [:omega,omega:] c= [:M,M:] by ZFMISC_1:96;
then f in PFuncs ([:M,M:],M) by A54, A56, PARTFUN1:def_3;
then X <> {} by A1, A53, A54;
then consider Y being set such that
A57: Y in X and
A58: for Z being set st Z in X & Z <> Y holds
not Y c= Z by A3, ORDERS_1:67;
consider f being Function such that
A59: f = Y and
A60: f is one-to-one and
A61: dom f = [:(rng f),(rng f):] by A1, A57;
set A = rng f;
A62: [:(rng f),(rng f):], rng f are_equipotent by A60, A61, WELLORD2:def_4;
Y in PFuncs ([:M,M:],M) by A1, A57;
then A63: ex f being Function st
( Y = f & dom f c= [:M,M:] & rng f c= M ) by PARTFUN1:def_3;
set N = card (rng f);
A64: card M = M by CARD_1:def_2;
then A65: card (rng f) c= M by A59, A63, CARD_1:11;
A66: now__::_thesis:_not_rng_f_is_finite
omega \ (rng f) misses rng f by XBOOLE_1:79;
then A67: (omega \ (rng f)) /\ (rng f) = {} by XBOOLE_0:def_7;
then [:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (omega \ (rng f))):] = {} by ZFMISC_1:90;
then A68: [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100;
[:((omega \ (rng f)) /\ (omega \ (rng f))),((omega \ (rng f)) /\ (rng f)):] = {} by A67, ZFMISC_1:90;
then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(omega \ (rng f)),(rng f):] = {} by ZFMISC_1:100;
then A69: [:(omega \ (rng f)),(omega \ (rng f)):] misses [:(omega \ (rng f)),(rng f):] by XBOOLE_0:def_7;
[:((rng f) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A67, ZFMISC_1:90;
then A70: [:(rng f),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100;
[:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (rng f)):] = {} by A67, ZFMISC_1:90;
then A71: ( {} \/ {} = {} & [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(rng f):] = {} ) by ZFMISC_1:100;
[:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A67, ZFMISC_1:90;
then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100;
then A72: ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(rng f):] = {} by A71, XBOOLE_1:23;
A73: ( omega c= omega +` (card (rng f)) & omega +` omega = omega ) by CARD_2:75, CARD_2:94;
assume A74: rng f is finite ; ::_thesis: contradiction
then card (rng f) in omega by CARD_1:47, CARD_3:42;
then omega +` (card (rng f)) c= omega +` omega by CARD_2:83;
then A75: omega = omega +` (card (rng f)) by A73, XBOOLE_0:def_10;
card (rng f) = card (card (rng f)) ;
then omega *` (card (rng f)) c= omega by A74, CARD_2:89;
then A76: omega +` (omega *` (card (rng f))) = omega by CARD_2:76;
card omega = omega by CARD_1:def_2;
then A77: omega = card (omega \ (rng f)) by A74, A75, CARD_2:98, CARD_3:42;
[:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (omega \ (rng f))):] = {} by A67, ZFMISC_1:90;
then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100;
then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(omega \ (rng f)):] = {} \/ {} by A68, XBOOLE_1:23
.= {} ;
then [:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):] misses [:(rng f),(omega \ (rng f)):] by XBOOLE_0:def_7;
then card (([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):]) = (card ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by CARD_2:35
.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by A69, CARD_2:35
.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A77, CARD_2:7
.= ((card [:omega,omega:]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A77, CARD_2:7
.= (omega +` (card [:omega,(card (rng f)):])) +` (card [:(card (rng f)),omega:]) by A77, Th5, CARD_2:7
.= (omega +` (omega *` (card (rng f)))) +` (card [:(card (rng f)),omega:]) by CARD_2:def_2
.= (omega +` (omega *` (card (rng f)))) +` ((card (rng f)) *` omega) by CARD_2:def_2 ;
then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):],omega \ (rng f) are_equipotent by A77, A76, CARD_1:5;
then consider g being Function such that
A78: g is one-to-one and
A79: dom g = ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):] and
A80: rng g = omega \ (rng f) by WELLORD2:def_4;
A81: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1;
then A82: dom (g +* f) = ([:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),(omega \ (rng f)):]) \/ [:(rng f),(rng f):] by A61, A79, ZFMISC_1:97
.= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ ([:(rng f),(omega \ (rng f)):] \/ [:(rng f),(rng f):]) by XBOOLE_1:4
.= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97
.= [:((omega \ (rng f)) \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97
.= [:(omega \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by XBOOLE_1:39
.= [:(omega \/ (rng f)),(omega \/ (rng f)):] by XBOOLE_1:39 ;
{} \/ {} = {} ;
then (dom g) /\ (dom f) = {} by A61, A79, A72, A70, XBOOLE_1:23;
then A83: dom g misses dom f by XBOOLE_0:def_7;
then g c= g +* f by FUNCT_4:32;
then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11;
then ( rng (g +* f) c= (rng g) \/ (rng f) & (rng g) \/ (rng f) c= rng (g +* f) ) by FUNCT_4:17, XBOOLE_1:8;
then A84: rng (g +* f) = (rng g) \/ (rng f) by XBOOLE_0:def_10
.= omega \/ (rng f) by A80, XBOOLE_1:39 ;
A85: g +* f is one-to-one
proof
rng f misses rng g by A80, XBOOLE_1:79;
then A86: (rng f) /\ (rng g) = {} by XBOOLE_0:def_7;
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom (g +* f) or not b1 in dom (g +* f) or not (g +* f) . x = (g +* f) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom (g +* f) or not y in dom (g +* f) or not (g +* f) . x = (g +* f) . y or x = y )
assume that
A87: x in dom (g +* f) and
A88: y in dom (g +* f) ; ::_thesis: ( not (g +* f) . x = (g +* f) . y or x = y )
A89: ( y in dom g or y in dom f ) by A81, A88, XBOOLE_0:def_3;
( x in dom f or x in dom g ) by A81, A87, XBOOLE_0:def_3;
then ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A60, A78, A83, A89, FUNCT_1:def_3, FUNCT_1:def_4, FUNCT_4:13, FUNCT_4:16;
hence ( not (g +* f) . x = (g +* f) . y or x = y ) by A86, XBOOLE_0:def_4; ::_thesis: verum
end;
set x = the Element of omega \ (rng f);
omega \ (rng f) <> {} by A74, A75, CARD_1:68, CARD_3:42;
then A90: ( the Element of omega \ (rng f) in omega & not the Element of omega \ (rng f) in rng f ) by XBOOLE_0:def_5;
A91: omega \/ (rng f) c= M by A56, A59, A63, XBOOLE_1:8;
then [:(omega \/ (rng f)),(omega \/ (rng f)):] c= [:M,M:] by ZFMISC_1:96;
then g +* f in PFuncs ([:M,M:],M) by A84, A82, A91, PARTFUN1:def_3;
then g +* f in X by A1, A84, A82, A85;
then g +* f = f by A58, A59, FUNCT_4:25;
hence contradiction by A84, A90, XBOOLE_0:def_3; ::_thesis: verum
end;
A92: now__::_thesis:_not_card_(rng_f)_<>_M
(card (rng f)) *` (card (rng f)) = card [:(card (rng f)),(card (rng f)):] by CARD_2:def_2;
then A93: (card (rng f)) *` (card (rng f)) = card [:(rng f),(rng f):] by CARD_2:7;
[:(rng f),(rng f):], rng f are_equipotent by A60, A61, WELLORD2:def_4;
then A94: (card (rng f)) *` (card (rng f)) = card (rng f) by A93, CARD_1:5;
assume card (rng f) <> M ; ::_thesis: contradiction
then A95: card (rng f) in M by A65, CARD_1:3;
M +` (card (rng f)) = M by A55, A65, CARD_2:76;
then card (M \ (rng f)) = M by A64, A95, CARD_2:98;
then consider h being Function such that
A96: ( h is one-to-one & dom h = rng f ) and
A97: rng h c= M \ (rng f) by A65, CARD_1:10;
set B = rng h;
rng f, rng h are_equipotent by A96, WELLORD2:def_4;
then A98: card (rng f) = card (rng h) by CARD_1:5;
( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A97, XBOOLE_1:26, XBOOLE_1:79;
then (rng f) /\ (rng h) c= {} by XBOOLE_0:def_7;
then (rng f) /\ (rng h) = {} ;
then A99: rng f misses rng h by XBOOLE_0:def_7;
((rng f) \/ (rng h)) \ (rng f) = (rng h) \ (rng f) by XBOOLE_1:40
.= rng h by A99, XBOOLE_1:83 ;
then A100: [:(rng h),(rng h):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] by ZFMISC_1:96;
( [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] & [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] = [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] ) by XBOOLE_1:7, ZFMISC_1:103;
then A101: [:(rng h),(rng h):] c= [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] by A100, XBOOLE_1:1;
(card (rng f)) +` (card (rng f)) = card (rng f) by A66, CARD_2:75;
then card ((rng f) \/ (rng h)) = card (rng f) by A98, A99, CARD_2:35;
then card [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] = card [:(card (rng f)),(card (rng f)):] by CARD_2:7
.= card (rng f) by A94, CARD_2:def_2 ;
then A102: card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) c= card (rng f) by CARD_1:11;
card (rng f) = card [:(card (rng f)),(card (rng f)):] by A94, CARD_2:def_2;
then card (rng f) = card [:(rng h),(rng h):] by A98, CARD_2:7;
then card (rng f) c= card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) by A101, CARD_1:11;
then card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) = card (rng f) by A102, XBOOLE_0:def_10;
then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):], rng h are_equipotent by A98, CARD_1:5;
then consider g being Function such that
A103: g is one-to-one and
A104: dom g = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] and
A105: rng g = rng h by WELLORD2:def_4;
A106: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1;
then ( rng f c= (rng f) \/ (rng h) & dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \/ [:(rng f),(rng f):] ) by A61, A104, XBOOLE_1:7, XBOOLE_1:39;
then A107: dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] by XBOOLE_1:12, ZFMISC_1:96;
A108: [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] misses [:(rng f),(rng f):] by XBOOLE_1:79;
A109: g +* 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 (g +* f) or not b1 in dom (g +* f) or not (g +* f) . x = (g +* f) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom (g +* f) or not y in dom (g +* f) or not (g +* f) . x = (g +* f) . y or x = y )
assume that
A110: x in dom (g +* f) and
A111: y in dom (g +* f) ; ::_thesis: ( not (g +* f) . x = (g +* f) . y or x = y )
A112: ( y in dom g or y in dom f ) by A106, A111, XBOOLE_0:def_3;
( x in dom f or x in dom g ) by A106, A110, XBOOLE_0:def_3;
then A113: ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A60, A61, A103, A104, A108, A112, FUNCT_1:def_3, FUNCT_1:def_4, FUNCT_4:13, FUNCT_4:16;
( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A97, XBOOLE_1:26, XBOOLE_1:79;
then A114: (rng f) /\ (rng g) c= {} by A105, XBOOLE_0:def_7;
assume (g +* f) . x = (g +* f) . y ; ::_thesis: x = y
hence x = y by A114, A113, XBOOLE_0:def_4; ::_thesis: verum
end;
set x = the Element of rng h;
A115: rng h <> {} by A66, A98;
then the Element of rng h in M \ (rng f) by A97, TARSKI:def_3;
then A116: not the Element of rng h in rng f by XBOOLE_0:def_5;
g c= g +* f by A61, A104, FUNCT_4:32, XBOOLE_1:79;
then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11;
then A117: (rng g) \/ (rng f) c= rng (g +* f) by XBOOLE_1:8;
rng (g +* f) c= (rng g) \/ (rng f) by FUNCT_4:17;
then A118: rng (g +* f) = (rng g) \/ (rng f) by A117, XBOOLE_0:def_10;
rng h c= M by A97, XBOOLE_1:1;
then A119: (rng f) \/ (rng h) c= M by A59, A63, XBOOLE_1:8;
then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] c= [:M,M:] by ZFMISC_1:96;
then g +* f in PFuncs ([:M,M:],M) by A105, A118, A107, A119, PARTFUN1:def_3;
then A120: g +* f in X by A1, A105, A118, A107, A109;
the Element of rng h in rng (g +* f) by A105, A118, A115, XBOOLE_0:def_3;
hence contradiction by A58, A59, A120, A116, FUNCT_4:25; ::_thesis: verum
end;
then M *` M = card [:(card (rng f)),(card (rng f)):] by CARD_2:def_2
.= card [:(rng f),(rng f):] by CARD_2:7 ;
hence M *` M = M by A92, A62, CARD_1:5; ::_thesis: verum
end;
theorem Th16: :: CARD_4:16
for M, N being Cardinal st not M is finite & 0 in N & ( N c= M or N in M ) holds
( M *` N = M & N *` M = M )
proof
let M, N be Cardinal; ::_thesis: ( not M is finite & 0 in N & ( N c= M or N in M ) implies ( M *` N = M & N *` M = M ) )
A1: 1 *` M = M by CARD_2:21;
assume not M is finite ; ::_thesis: ( not 0 in N or ( not N c= M & not N in M ) or ( M *` N = M & N *` M = M ) )
then A2: M *` M = M by Th15;
assume 0 in N ; ::_thesis: ( ( not N c= M & not N in M ) or ( M *` N = M & N *` M = M ) )
then 1 c= N by CARD_2:68;
then A3: 1 *` M c= N *` M by CARD_2:90;
assume ( N c= M or N in M ) ; ::_thesis: ( M *` N = M & N *` M = M )
then N *` M c= M *` M by CARD_2:90;
hence ( M *` N = M & N *` M = M ) by A2, A3, A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th17: :: CARD_4:17
for M, N being Cardinal st not M is finite & ( N c= M or N in M ) holds
( M *` N c= M & N *` M c= M )
proof
let M, N be Cardinal; ::_thesis: ( not M is finite & ( N c= M or N in M ) implies ( M *` N c= M & N *` M c= M ) )
assume ( not M is finite & ( N c= M or N in M ) ) ; ::_thesis: ( M *` N c= M & N *` M c= M )
then ( M *` N = M or not 0 in N ) by Th16;
then ( M *` N c= M or ( N = 0 & M *` 0 = 0 & 0 c= M ) ) by CARD_2:20, ORDINAL3:8, XBOOLE_1:2;
hence ( M *` N c= M & N *` M c= M ) ; ::_thesis: verum
end;
theorem :: CARD_4:18
for X being set st not X is finite holds
( [:X,X:],X are_equipotent & card [:X,X:] = card X )
proof
let X be set ; ::_thesis: ( not X is finite implies ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) )
assume not X is finite ; ::_thesis: ( [:X,X:],X are_equipotent & card [:X,X:] = card X )
then (card X) *` (card X) = card X by Th15;
then card [:(card X),(card X):] = card X by CARD_2:def_2;
then card [:X,X:] = card X by CARD_2:7;
hence ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) by CARD_1:5; ::_thesis: verum
end;
theorem :: CARD_4:19
for X, Y being set st not X is finite & Y is finite & Y <> {} holds
( [:X,Y:],X are_equipotent & card [:X,Y:] = card X )
proof
let X, Y be set ; ::_thesis: ( not X is finite & Y is finite & Y <> {} implies ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) )
assume that
A1: not X is finite and
A2: ( Y is finite & Y <> {} ) ; ::_thesis: ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X )
( card Y c= card X & 0 in card Y ) by A1, A2, ORDINAL3:8;
then (card X) *` (card Y) = card X by A1, Th16;
then card [:(card X),(card Y):] = card X by CARD_2:def_2;
then card [:X,Y:] = card X by CARD_2:7;
hence ( [:X,Y:],X are_equipotent & card [:X,Y:] = card X ) by CARD_1:5; ::_thesis: verum
end;
theorem :: CARD_4:20
for K, L, M, N being Cardinal st K in L & M in N holds
( K *` M in L *` N & M *` K in L *` N )
proof
let K, L, M, N be Cardinal; ::_thesis: ( K in L & M in N implies ( K *` M in L *` N & M *` K in L *` N ) )
A1: for K, L, M, N being Cardinal st K in L & M in N & L c= N holds
K *` M in L *` N
proof
let K, L, M, N be Cardinal; ::_thesis: ( K in L & M in N & L c= N implies K *` M in L *` N )
assume that
A2: K in L and
A3: M in N and
A4: L c= N ; ::_thesis: K *` M in L *` N
A5: now__::_thesis:_(_N_is_finite_implies_K_*`_M_in_L_*`_N_)
assume A6: N is finite ; ::_thesis: K *` M in L *` N
then reconsider N = N as finite Cardinal ;
reconsider L = L, M = M, K = K as finite Cardinal by A2, A3, A4, A6, CARD_3:92;
A7: card N = N by CARD_1:def_2;
A8: card M = M by CARD_1:def_2;
then card M < card N by A3, A7, NAT_1:41;
then A9: (card K) * (card M) <= (card K) * (card N) by XREAL_1:64;
A10: card L = L by CARD_1:def_2;
then A11: L *` N = card ((card L) * (card N)) by A7, CARD_2:39;
A12: card K = K by CARD_1:def_2;
then card K < card L by A2, A10, NAT_1:41;
then (card K) * (card N) < (card L) * (card N) by A3, XREAL_1:68;
then A13: (card K) * (card M) < (card L) * (card N) by A9, XXREAL_0:2;
K *` M = card ((card K) * (card M)) by A12, A8, CARD_2:39;
hence K *` M in L *` N by A11, A13, NAT_1:41; ::_thesis: verum
end;
A14: 0 in L by A2, ORDINAL3:8;
now__::_thesis:_(_not_N_is_finite_implies_K_*`_M_in_L_*`_N_)
assume A15: not N is finite ; ::_thesis: K *` M in L *` N
then A16: L *` N = N by A4, A14, Th16;
A17: omega c= N by A15, CARD_3:85;
A18: now__::_thesis:_(_K_is_finite_&_M_is_finite_implies_K_*`_M_in_L_*`_N_)
assume ( K is finite & M is finite ) ; ::_thesis: K *` M in L *` N
then reconsider K = K, M = M as finite Cardinal ;
( card K = K & card M = M ) by CARD_1:def_2;
then K *` M = card ((card K) * (card M)) by CARD_2:39
.= (card K) * (card M) by CARD_1:def_2 ;
hence K *` M in L *` N by A16, A17, TARSKI:def_3; ::_thesis: verum
end;
( ( K c= M & ( M is finite or not M is finite ) ) or ( M c= K & ( K is finite or not K is finite ) ) ) ;
then ( ( K is finite & M is finite ) or K *` M c= M or ( K *` M c= K & K in N ) ) by A2, A4, Th17;
hence K *` M in L *` N by A3, A16, A18, ORDINAL1:12; ::_thesis: verum
end;
hence K *` M in L *` N by A5; ::_thesis: verum
end;
( L c= N or N c= L ) ;
hence ( K in L & M in N implies ( K *` M in L *` N & M *` K in L *` N ) ) by A1; ::_thesis: verum
end;
theorem Th21: :: CARD_4:21
for X being set st not X is finite holds
card X = omega *` (card X)
proof
let X be set ; ::_thesis: ( not X is finite implies card X = omega *` (card X) )
assume A1: not X is finite ; ::_thesis: card X = omega *` (card X)
then omega c= card X by CARD_3:85;
hence card X = omega *` (card X) by A1, Th16; ::_thesis: verum
end;
theorem :: CARD_4:22
for X, Y being set st X <> {} & X is finite & not Y is finite holds
(card Y) *` (card X) = card Y
proof
let X, Y be set ; ::_thesis: ( X <> {} & X is finite & not Y is finite implies (card Y) *` (card X) = card Y )
assume that
A1: ( X <> {} & X is finite ) and
A2: not Y is finite ; ::_thesis: (card Y) *` (card X) = card Y
( card X in card Y & 0 in card X ) by A1, A2, CARD_3:86, ORDINAL3:8;
hence (card Y) *` (card X) = card Y by A2, Th16; ::_thesis: verum
end;
theorem Th23: :: CARD_4:23
for D being non empty set
for n being Element of NAT st not D is finite & n <> 0 holds
( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D )
proof
let D be non empty set ; ::_thesis: for n being Element of NAT st not D is finite & n <> 0 holds
( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D )
let n be Element of NAT ; ::_thesis: ( not D is finite & n <> 0 implies ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) )
assume that
A1: not D is finite and
A2: n <> 0 ; ::_thesis: ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D )
defpred S1[ Nat] means ( $1 <> 0 implies card ($1 -tuples_on D) = card D );
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
0 -tuples_on D = {(<*> D)} by FINSEQ_2:94;
then A4: ( 0 in card (0 -tuples_on D) & card (0 -tuples_on D) c= card D ) by A1, ORDINAL3:8;
k in NAT by ORDINAL1:def_12;
then A5: card ((k + 1) -tuples_on D) = card [:(k -tuples_on D),(1 -tuples_on D):] by Th9
.= card [:(card (k -tuples_on D)),(card (1 -tuples_on D)):] by CARD_2:7
.= card [:(card (k -tuples_on D)),(card D):] by Th8
.= (card (k -tuples_on D)) *` (card D) by CARD_2:def_2 ;
assume S1[k] ; ::_thesis: S1[k + 1]
hence S1[k + 1] by A1, A5, A4, Th16; ::_thesis: verum
end;
A6: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A6, A3);
then card (n -tuples_on D) = card D by A2;
hence ( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D ) by CARD_1:5; ::_thesis: verum
end;
theorem :: CARD_4:24
for D being non empty set st not D is finite holds
card D = card (D *)
proof
let D be non empty set ; ::_thesis: ( not D is finite implies card D = card (D *) )
defpred S1[ set ] means verum;
deffunc H1( Element of NAT ) -> FinSequenceSet of D = $1 -tuples_on D;
A1: D * = union { (k -tuples_on D) where k is Element of NAT : verum } by FINSEQ_2:108;
assume A2: not D is finite ; ::_thesis: card D = card (D *)
A3: for X being set st X in { (k -tuples_on D) where k is Element of NAT : verum } holds
card X c= card D
proof
let X be set ; ::_thesis: ( X in { (k -tuples_on D) where k is Element of NAT : verum } implies card X c= card D )
assume X in { (k -tuples_on D) where k is Element of NAT : verum } ; ::_thesis: card X c= card D
then consider k being Element of NAT such that
A4: X = k -tuples_on D ;
0 -tuples_on D = {(<*> D)} by FINSEQ_2:94;
then ( ( card (0 -tuples_on D) c= card D & k = 0 ) or k <> 0 ) by A2;
hence card X c= card D by A2, A4, Th23; ::_thesis: verum
end;
1 -tuples_on D in { (k -tuples_on D) where k is Element of NAT : verum } ;
then card (1 -tuples_on D) c= card (D *) by A1, CARD_1:11, ZFMISC_1:74;
then A5: card D c= card (D *) by Th8;
{ H1(k) where k is Element of NAT : S1[k] } is countable from CARD_4:sch_1();
then card { (k -tuples_on D) where k is Element of NAT : verum } c= omega by CARD_3:def_14;
then card (union { (k -tuples_on D) where k is Element of NAT : verum } ) c= omega *` (card D) by A3, CARD_2:87;
then card (D *) c= card D by A2, A1, Th21;
hence card D = card (D *) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;