:: CARD_5 semantic presentation
begin
Lm1: 1 = card 1
by CARD_1:def_2;
Lm2: 2 = card 2
by CARD_1:def_2;
begin
theorem Th1: :: CARD_5:1
for X being set holds nextcard (card X) = nextcard X
proof
let X be set ; ::_thesis: nextcard (card X) = nextcard X
( card (card X) in nextcard X & ( for M being Cardinal st card (card X) in M holds
nextcard X c= M ) ) by CARD_1:def_3;
hence nextcard (card X) = nextcard X by CARD_1:def_3; ::_thesis: verum
end;
theorem Th2: :: CARD_5:2
for y being set
for f being Function holds
( y in Union f iff ex x being set st
( x in dom f & y in f . x ) )
proof
let y be set ; ::_thesis: for f being Function holds
( y in Union f iff ex x being set st
( x in dom f & y in f . x ) )
let f be Function; ::_thesis: ( y in Union f iff ex x being set st
( x in dom f & y in f . x ) )
thus ( y in Union f implies ex x being set st
( x in dom f & y in f . x ) ) ::_thesis: ( ex x being set st
( x in dom f & y in f . x ) implies y in Union f )
proof
assume y in Union f ; ::_thesis: ex x being set st
( x in dom f & y in f . x )
then consider X being set such that
A1: y in X and
A2: X in rng f by TARSKI:def_4;
consider x being set such that
A3: ( x in dom f & X = f . x ) by A2, FUNCT_1:def_3;
take x ; ::_thesis: ( x in dom f & y in f . x )
thus ( x in dom f & y in f . x ) by A1, A3; ::_thesis: verum
end;
given x being set such that A4: x in dom f and
A5: y in f . x ; ::_thesis: y in Union f
f . x in rng f by A4, FUNCT_1:def_3;
hence y in Union f by A5, TARSKI:def_4; ::_thesis: verum
end;
theorem Th3: :: CARD_5:3
for A being Ordinal holds alef A is infinite
proof
let A be Ordinal; ::_thesis: alef A is infinite
{} c= A by XBOOLE_1:2;
then omega c= alef A by CARD_1:23, CARD_1:46;
hence alef A is infinite ; ::_thesis: verum
end;
theorem Th4: :: CARD_5:4
for M being Cardinal st M is infinite holds
ex A being Ordinal st M = alef A
proof
let M be Cardinal; ::_thesis: ( M is infinite implies ex A being Ordinal st M = alef A )
defpred S1[ set ] means ( $1 is infinite implies ex A being Ordinal st $1 = alef A );
A1: for K being Cardinal st S1[K] holds
S1[ nextcard K]
proof
let K be Cardinal; ::_thesis: ( S1[K] implies S1[ nextcard K] )
assume that
A2: S1[K] and
A3: not nextcard K is finite ; ::_thesis: ex A being Ordinal st nextcard K = alef A
now__::_thesis:_not_K_is_finite
assume K is finite ; ::_thesis: contradiction
then reconsider K9 = K as finite set ;
card K = K by CARD_1:def_2;
then nextcard K = card ((card K9) + 1) by NAT_1:42;
hence contradiction by A3; ::_thesis: verum
end;
then consider A being Ordinal such that
A4: K = alef A by A2;
take succ A ; ::_thesis: nextcard K = alef (succ A)
thus nextcard K = alef (succ A) by A4, CARD_1:19; ::_thesis: verum
end;
A5: for K being Cardinal st K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds
S1[N] ) holds
S1[K]
proof
let K be Cardinal; ::_thesis: ( K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds
S1[N] ) implies S1[K] )
deffunc H1( Ordinal) -> set = alef $1;
defpred S2[ set , set ] means ex A being Ordinal st
( $1 = alef A & $2 = A );
assume that
K <> {} and
A6: K is limit_cardinal and
A7: for N being Cardinal st N in K holds
S1[N] and
A8: not K is finite ; ::_thesis: ex A being Ordinal st K = alef A
defpred S3[ set ] means ex N being Cardinal st
( N = $1 & not N is finite );
consider X being set such that
A9: for x being set holds
( x in X iff ( x in K & S3[x] ) ) from XBOOLE_0:sch_1();
A10: for x being set st x in X holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st S2[x,y] )
assume A11: x in X ; ::_thesis: ex y being set st S2[x,y]
then consider N being Cardinal such that
A12: N = x and
A13: not N is finite by A9;
N in K by A9, A11, A12;
then ex A being Ordinal st x = alef A by A7, A12, A13;
hence ex y being set st S2[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A14: ( dom f = X & ( for x being set st x in X holds
S2[x,f . x] ) ) from CLASSES1:sch_1(A10);
now__::_thesis:_for_x_being_set_st_x_in_rng_f_holds_
(_x_is_Ordinal_&_x_c=_rng_f_)
let x be set ; ::_thesis: ( x in rng f implies ( x is Ordinal & x c= rng f ) )
assume x in rng f ; ::_thesis: ( x is Ordinal & x c= rng f )
then consider y being set such that
A15: y in X and
A16: x = f . y by A14, FUNCT_1:def_3;
consider A being Ordinal such that
A17: y = alef A and
A18: x = A by A14, A15, A16;
thus x is Ordinal by A18; ::_thesis: x c= rng f
thus x c= rng f ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x or z in rng f )
assume A19: z in x ; ::_thesis: z in rng f
then reconsider z9 = z as Ordinal by A18;
A20: alef z9 in alef A by A18, A19, CARD_1:21;
alef A in K by A9, A15, A17;
then A21: alef z9 in K by A20, ORDINAL1:10;
not alef z9 is finite by Th3;
then A22: alef z9 in X by A9, A21;
then ex A being Ordinal st
( alef z9 = alef A & f . (alef z9) = A ) by A14;
then z9 = f . (alef z9) by CARD_1:22;
hence z in rng f by A14, A22, FUNCT_1:def_3; ::_thesis: verum
end;
end;
then reconsider A = rng f as Ordinal by ORDINAL1:19;
consider L being T-Sequence such that
A23: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H1(B) ) ) from ORDINAL2:sch_2();
now__::_thesis:_for_B_being_Ordinal_st_B_in_A_holds_
succ_B_in_A
let B be Ordinal; ::_thesis: ( B in A implies succ B in A )
assume B in A ; ::_thesis: succ B in A
then consider x being set such that
A24: x in X and
A25: B = f . x by A14, FUNCT_1:def_3;
consider C being Ordinal such that
A26: x = alef C and
A27: B = C by A14, A24, A25;
A28: alef (succ C) = nextcard (alef C) by CARD_1:19;
alef C in K by A9, A24, A26;
then A29: alef (succ C) c= K by A28, CARD_3:90;
alef (succ C) <> K by A6, A28, CARD_1:def_4;
then A30: alef (succ C) in K by A29, CARD_1:3;
not alef (succ C) is finite by Th3;
then A31: alef (succ C) in X by A9, A30;
then consider D being Ordinal such that
A32: alef (succ C) = alef D and
A33: f . (alef (succ C)) = D by A14;
succ C = D by A32, CARD_1:22;
hence succ B in A by A14, A27, A31, A33, FUNCT_1:def_3; ::_thesis: verum
end;
then A is limit_ordinal by ORDINAL1:28;
then A34: ( A = {} or alef A = card (sup L) ) by A23, CARD_1:20;
take A ; ::_thesis: K = alef A
sup L c= K
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup L or x in K )
assume A35: x in sup L ; ::_thesis: x in K
then reconsider x9 = x as Ordinal ;
consider C being Ordinal such that
A36: C in rng L and
A37: x9 c= C by A35, ORDINAL2:21;
consider y being set such that
A38: y in dom L and
A39: C = L . y by A36, FUNCT_1:def_3;
reconsider y = y as Ordinal by A38;
A40: C = alef y by A23, A38, A39;
consider z being set such that
A41: z in dom f and
A42: y = f . z by A23, A38, FUNCT_1:def_3;
ex D being Ordinal st
( z = alef D & y = D ) by A14, A41, A42;
then C in K by A9, A14, A40, A41;
hence x in K by A37, ORDINAL1:12; ::_thesis: verum
end;
then card (sup L) c= card K by CARD_1:11;
then A43: card (sup L) c= K by CARD_1:def_2;
now__::_thesis:_(_(_A_=_{}_&_K_=_omega_)_or_(_A_<>_{}_&_not_K_<>_alef_A_)_)
percases ( A = {} or A <> {} ) ;
case A = {} ; ::_thesis: K = omega
then not omega in X by A14, RELAT_1:42;
then not omega in K by A9;
then A44: K c= omega by CARD_1:4;
omega c= K by A8, CARD_3:85;
hence K = omega by A44, XBOOLE_0:def_10; ::_thesis: verum
end;
caseA45: A <> {} ; ::_thesis: not K <> alef A
assume K <> alef A ; ::_thesis: contradiction
then A46: card (sup L) in K by A34, A43, A45, CARD_1:3;
not alef A is finite by Th3;
then A47: card (sup L) in X by A9, A34, A45, A46;
then consider B being Ordinal such that
A48: card (sup L) = alef B and
A49: f . (card (sup L)) = B by A14;
A = B by A34, A45, A48, CARD_1:22;
then A in A by A14, A47, A49, FUNCT_1:def_3;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence K = alef A by CARD_1:46; ::_thesis: verum
end;
A50: S1[ {} ] ;
for M being Cardinal holds S1[M] from CARD_1:sch_1(A50, A1, A5);
hence ( M is infinite implies ex A being Ordinal st M = alef A ) ; ::_thesis: verum
end;
registration
let phi be Ordinal-Sequence;
cluster Union phi -> ordinal ;
coherence
Union phi is ordinal
proof
ex A being Ordinal st rng phi c= A by ORDINAL2:def_4;
then On (rng phi) = rng phi by ORDINAL3:6;
hence Union phi is ordinal by ORDINAL3:5; ::_thesis: verum
end;
end;
theorem Th5: :: CARD_5:5
for A being Ordinal
for X being set st X c= A holds
ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
proof
let A be Ordinal; ::_thesis: for X being set st X c= A holds
ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
let X be set ; ::_thesis: ( X c= A implies ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) )
set R = RelIncl X;
set B = order_type_of (RelIncl X);
set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X));
assume A1: X c= A ; ::_thesis: ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
then RelIncl X is well-ordering by WELLORD2:8;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2;
then ( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic ) by WELLORD1:40, WELLORD2:8;
then A2: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X by WELLORD1:def_9;
then A3: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one by WELLORD1:def_7;
A4: field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) by WELLORD2:def_1;
then A5: dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X) by A2, WELLORD1:def_7;
A6: field (RelIncl X) = X by WELLORD2:def_1;
then A7: rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X by A2, WELLORD1:def_7;
reconsider phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) as T-Sequence by A5, ORDINAL1:def_7;
reconsider phi = phi as Ordinal-Sequence by A1, A7, ORDINAL2:def_4;
take phi ; ::_thesis: ( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
thus phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) ; ::_thesis: ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
thus phi is increasing ::_thesis: ( dom phi = order_type_of (RelIncl X) & rng phi = X )
proof
let a, b be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: ( not a in b or not b in dom phi or phi . a in phi . b )
assume that
A8: a in b and
A9: b in dom phi ; ::_thesis: phi . a in phi . b
A10: a in dom phi by A8, A9, ORDINAL1:10;
reconsider a9 = phi . a, b9 = phi . b as Ordinal ;
A11: b9 in X by A7, A9, FUNCT_1:def_3;
a c= b by A8, ORDINAL1:def_2;
then [a,b] in RelIncl (order_type_of (RelIncl X)) by A5, A9, A10, WELLORD2:def_1;
then A12: [a9,b9] in RelIncl X by A2, WELLORD1:def_7;
a9 in X by A7, A10, FUNCT_1:def_3;
then A13: a9 c= b9 by A12, A11, WELLORD2:def_1;
a <> b by A8;
then a9 <> b9 by A3, A9, A10, FUNCT_1:def_4;
then a9 c< b9 by A13, XBOOLE_0:def_8;
hence phi . a in phi . b by ORDINAL1:11; ::_thesis: verum
end;
thus ( dom phi = order_type_of (RelIncl X) & rng phi = X ) by A2, A4, A6, WELLORD1:def_7; ::_thesis: verum
end;
theorem Th6: :: CARD_5:6
for A being Ordinal
for X being set st X c= A holds
sup X is_cofinal_with order_type_of (RelIncl X)
proof
let A be Ordinal; ::_thesis: for X being set st X c= A holds
sup X is_cofinal_with order_type_of (RelIncl X)
let X be set ; ::_thesis: ( X c= A implies sup X is_cofinal_with order_type_of (RelIncl X) )
assume A1: X c= A ; ::_thesis: sup X is_cofinal_with order_type_of (RelIncl X)
then consider phi being Ordinal-Sequence such that
phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) and
A2: ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) by Th5;
take phi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom phi = order_type_of (RelIncl X) & rng phi c= sup X & phi is increasing & sup X = sup phi )
On X = X by A1, ORDINAL3:6;
hence ( dom phi = order_type_of (RelIncl X) & rng phi c= sup X & phi is increasing & sup X = sup phi ) by A2, ORDINAL2:def_3; ::_thesis: verum
end;
theorem Th7: :: CARD_5:7
for A being Ordinal
for X being set st X c= A holds
card X = card (order_type_of (RelIncl X))
proof
let A be Ordinal; ::_thesis: for X being set st X c= A holds
card X = card (order_type_of (RelIncl X))
let X be set ; ::_thesis: ( X c= A implies card X = card (order_type_of (RelIncl X)) )
set R = RelIncl X;
set B = order_type_of (RelIncl X);
set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X));
assume X c= A ; ::_thesis: card X = card (order_type_of (RelIncl X))
then RelIncl X is well-ordering by WELLORD2:8;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2;
then ( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic ) by WELLORD1:40, WELLORD2:8;
then A1: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X by WELLORD1:def_9;
field (RelIncl X) = X by WELLORD2:def_1;
then A2: rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X by A1, WELLORD1:def_7;
field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) by WELLORD2:def_1;
then A3: dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X) by A1, WELLORD1:def_7;
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one by A1, WELLORD1:def_7;
then order_type_of (RelIncl X),X are_equipotent by A3, A2, WELLORD2:def_4;
hence card X = card (order_type_of (RelIncl X)) by CARD_1:5; ::_thesis: verum
end;
theorem Th8: :: CARD_5:8
for A being Ordinal ex B being Ordinal st
( B c= card A & A is_cofinal_with B )
proof
let A be Ordinal; ::_thesis: ex B being Ordinal st
( B c= card A & A is_cofinal_with B )
set M = card A;
card A,A are_equipotent by CARD_1:def_2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = card A and
A3: rng f = A by WELLORD2:def_4;
defpred S1[ set ] means not f . $1 in Union (f | $1);
reconsider f = f as T-Sequence by A2, ORDINAL1:def_7;
reconsider f = f as Ordinal-Sequence by A3, ORDINAL2:def_4;
consider X being set such that
A4: for x being set holds
( x in X iff ( x in card A & S1[x] ) ) from XBOOLE_0:sch_1();
set R = RelIncl X;
set B = order_type_of (RelIncl X);
take order_type_of (RelIncl X) ; ::_thesis: ( order_type_of (RelIncl X) c= card A & A is_cofinal_with order_type_of (RelIncl X) )
A5: X c= card A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in card A )
thus ( not x in X or x in card A ) by A4; ::_thesis: verum
end;
hence order_type_of (RelIncl X) c= card A by WELLORD2:14; ::_thesis: A is_cofinal_with order_type_of (RelIncl X)
set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X));
RelIncl X is well-ordering by A5, WELLORD2:8;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2;
then ( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic ) by WELLORD1:40, WELLORD2:8;
then A6: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X by WELLORD1:def_9;
then A7: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one by WELLORD1:def_7;
field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) by WELLORD2:def_1;
then A8: dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X) by A6, WELLORD1:def_7;
field (RelIncl X) = X by WELLORD2:def_1;
then A9: rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X by A6, WELLORD1:def_7;
reconsider phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) as T-Sequence by A8, ORDINAL1:def_7;
reconsider phi = phi as Ordinal-Sequence by A5, A9, ORDINAL2:def_4;
A10: dom (f * phi) = order_type_of (RelIncl X) by A2, A5, A8, A9, RELAT_1:27;
then reconsider xi = f * phi as T-Sequence by ORDINAL1:def_7;
rng (f * phi) c= A by A3, RELAT_1:26;
then reconsider xi = xi as Ordinal-Sequence by ORDINAL2:def_4;
take xi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom xi = order_type_of (RelIncl X) & rng xi c= A & xi is increasing & A = sup xi )
thus ( dom xi = order_type_of (RelIncl X) & rng xi c= A ) by A2, A3, A5, A8, A9, RELAT_1:26, RELAT_1:27; ::_thesis: ( xi is increasing & A = sup xi )
thus xi is increasing ::_thesis: A = sup xi
proof
let a, b be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: ( not a in b or not b in dom xi or xi . a in xi . b )
assume that
A11: a in b and
A12: b in dom xi ; ::_thesis: xi . a in xi . b
A13: a in dom xi by A11, A12, ORDINAL1:10;
then A14: phi . a in X by A8, A9, A10, FUNCT_1:def_3;
a <> b by A11;
then A15: phi . a <> phi . b by A8, A7, A10, A12, A13, FUNCT_1:def_4;
reconsider a9 = phi . a, b9 = phi . b as Ordinal ;
reconsider a99 = f . a9, b99 = f . b9 as Ordinal ;
A16: phi . b in X by A8, A9, A10, A12, FUNCT_1:def_3;
then not b99 in Union (f | b9) by A4;
then A17: Union (f | b9) c= b99 by ORDINAL1:16;
a c= b by A11, ORDINAL1:def_2;
then [a,b] in RelIncl (order_type_of (RelIncl X)) by A10, A12, A13, WELLORD2:def_1;
then [(phi . a),(phi . b)] in RelIncl X by A6, WELLORD1:def_7;
then a9 c= b9 by A14, A16, WELLORD2:def_1;
then a9 c< b9 by A15, XBOOLE_0:def_8;
then a9 in b9 by ORDINAL1:11;
then a99 c= Union (f | b9) by A2, A5, A14, FUNCT_1:50, ZFMISC_1:74;
then A18: a99 c= b99 by A17, XBOOLE_1:1;
a99 <> b99 by A1, A2, A5, A15, A14, A16, FUNCT_1:def_4;
then A19: a99 c< b99 by A18, XBOOLE_0:def_8;
( a99 = xi . a & b99 = xi . b ) by A11, A12, FUNCT_1:12, ORDINAL1:10;
hence xi . a in xi . b by A19, ORDINAL1:11; ::_thesis: verum
end;
thus A c= sup xi :: according to XBOOLE_0:def_10 ::_thesis: sup xi c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in sup xi )
assume x in A ; ::_thesis: x in sup xi
then consider y being set such that
A20: y in dom f and
A21: x = f . y by A3, FUNCT_1:def_3;
reconsider x9 = x, y = y as Ordinal by A20, A21;
now__::_thesis:_x_in_sup_xi
percases ( not f . y in Union (f | y) or f . y in Union (f | y) ) ;
suppose not f . y in Union (f | y) ; ::_thesis: x in sup xi
then y in X by A2, A4, A20;
then consider z being set such that
A22: ( z in order_type_of (RelIncl X) & y = phi . z ) by A8, A9, FUNCT_1:def_3;
( x9 = xi . z & xi . z in rng xi ) by A10, A21, A22, FUNCT_1:12, FUNCT_1:def_3;
hence x in sup xi by ORDINAL2:19; ::_thesis: verum
end;
supposeA23: f . y in Union (f | y) ; ::_thesis: x in sup xi
defpred S2[ Ordinal] means ( $1 in y & f . y in f . $1 );
consider z being set such that
A24: z in dom (f | y) and
A25: f . y in (f | y) . z by A23, Th2;
reconsider z = z as Ordinal by A24;
A26: (f | y) . z = f . z by A24, FUNCT_1:47;
dom (f | y) = (dom f) /\ y by RELAT_1:61;
then z in y by A24, XBOOLE_0:def_4;
then A27: ex C being Ordinal st S2[C] by A25, A26;
consider C being Ordinal such that
A28: ( S2[C] & ( for B being Ordinal st S2[B] holds
C c= B ) ) from ORDINAL1:sch_1(A27);
now__::_thesis:_(_C_in_card_A_&_not_f_._C_in_Union_(f_|_C)_)
thus C in card A by A2, A20, A28, ORDINAL1:10; ::_thesis: not f . C in Union (f | C)
assume f . C in Union (f | C) ; ::_thesis: contradiction
then consider a being set such that
A29: a in dom (f | C) and
A30: f . C in (f | C) . a by Th2;
reconsider a = a as Ordinal by A29;
reconsider fa = (f | C) . a, fy = f . y as Ordinal ;
f . a = fa by A29, FUNCT_1:47;
then A31: fy in f . a by A28, A30, ORDINAL1:10;
dom (f | C) = (dom f) /\ C by RELAT_1:61;
then A32: a in C by A29, XBOOLE_0:def_4;
then a in y by A28, ORDINAL1:10;
hence contradiction by A28, A32, A31, ORDINAL1:5; ::_thesis: verum
end;
then C in X by A4;
then consider z being set such that
A33: z in order_type_of (RelIncl X) and
A34: C = phi . z by A8, A9, FUNCT_1:def_3;
reconsider z = z as Ordinal by A33;
reconsider xz = xi . z as Ordinal ;
xz in rng xi by A10, A33, FUNCT_1:def_3;
then A35: xz in sup xi by ORDINAL2:19;
x9 in xz by A10, A21, A28, A33, A34, FUNCT_1:12;
hence x in sup xi by A35, ORDINAL1:10; ::_thesis: verum
end;
end;
end;
hence x in sup xi ; ::_thesis: verum
end;
sup A = A by ORDINAL2:18;
hence sup xi c= A by A3, ORDINAL2:22, RELAT_1:26; ::_thesis: verum
end;
theorem Th9: :: CARD_5:9
for A being Ordinal ex M being Cardinal st
( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds
M c= B ) )
proof
let A be Ordinal; ::_thesis: ex M being Cardinal st
( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds
M c= B ) )
defpred S1[ Ordinal] means ( $1 c= card A & A is_cofinal_with $1 );
A1: ex B being Ordinal st S1[B] by Th8;
consider C being Ordinal such that
A2: S1[C] and
A3: for B being Ordinal st S1[B] holds
C c= B from ORDINAL1:sch_1(A1);
take M = card C; ::_thesis: ( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds
M c= B ) )
consider B being Ordinal such that
A4: B c= M and
A5: C is_cofinal_with B by Th8;
A6: M c= C by CARD_1:8;
then A7: B c= C by A4, XBOOLE_1:1;
then B c= card A by A2, XBOOLE_1:1;
then C c= B by A2, A3, A5, ORDINAL4:37;
then A8: C = B by A7, XBOOLE_0:def_10;
hence ( M c= card A & A is_cofinal_with M ) by A2, A4, A6, XBOOLE_0:def_10; ::_thesis: for B being Ordinal st A is_cofinal_with B holds
M c= B
let B be Ordinal; ::_thesis: ( A is_cofinal_with B implies M c= B )
assume that
A9: A is_cofinal_with B and
A10: not M c= B ; ::_thesis: contradiction
A11: C = M by A4, A6, A8, XBOOLE_0:def_10;
then not B c= card A by A3, A9, A10;
hence contradiction by A2, A11, A10, XBOOLE_1:1; ::_thesis: verum
end;
Lm3: for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
proof
let phi, psi be Ordinal-Sequence; ::_thesis: ( rng phi = rng psi & phi is increasing & psi is increasing implies for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A ) )
assume that
A1: rng phi = rng psi and
A2: phi is increasing ; ::_thesis: ( not psi is increasing or for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A ) )
defpred S1[ Ordinal] means ( $1 in dom phi implies ( $1 in dom psi & phi . $1 = psi . $1 ) );
assume A3: for A, B being Ordinal st A in B & B in dom psi holds
psi . A in psi . B ; :: according to ORDINAL2:def_12 ::_thesis: for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
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 & B in dom phi holds
( B in dom psi & phi . B = psi . B ) and
A6: A in dom phi ; ::_thesis: ( A in dom psi & phi . A = psi . A )
phi . A in rng phi by A6, FUNCT_1:def_3;
then consider x being set such that
A7: x in dom psi and
A8: phi . A = psi . x by A1, FUNCT_1:def_3;
reconsider x = x as Ordinal by A7;
A9: now__::_thesis:_not_A_in_x
assume A10: A in x ; ::_thesis: contradiction
then A11: A in dom psi by A7, ORDINAL1:10;
then psi . A in rng psi by FUNCT_1:def_3;
then consider y being set such that
A12: y in dom phi and
A13: psi . A = phi . y by A1, FUNCT_1:def_3;
reconsider y = y as Ordinal by A12;
psi . A in psi . x by A3, A7, A10;
then not A c= y by A2, A8, A12, A13, ORDINAL1:5, ORDINAL4:9;
then A14: y in A by ORDINAL1:16;
then A15: psi . y = phi . y by A5, A12;
psi . y in psi . A by A3, A11, A14;
hence contradiction by A13, A15; ::_thesis: verum
end;
now__::_thesis:_not_x_in_A
assume A16: x in A ; ::_thesis: contradiction
then ( phi . x in phi . A & x in dom phi ) by A2, A6, ORDINAL1:10, ORDINAL2:def_12;
then phi . A in phi . A by A5, A8, A16;
hence contradiction ; ::_thesis: verum
end;
hence ( A in dom psi & phi . A = psi . A ) by A7, A8, A9, ORDINAL1:14; ::_thesis: verum
end;
thus for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A4); ::_thesis: verum
end;
theorem :: CARD_5:10
for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
phi = psi
proof
let phi, psi be Ordinal-Sequence; ::_thesis: ( rng phi = rng psi & phi is increasing & psi is increasing implies phi = psi )
assume A1: ( rng phi = rng psi & phi is increasing & psi is increasing ) ; ::_thesis: phi = psi
A2: dom phi = dom psi
proof
thus dom phi c= dom psi :: according to XBOOLE_0:def_10 ::_thesis: dom psi c= dom phi
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom phi or x in dom psi )
assume x in dom phi ; ::_thesis: x in dom psi
hence x in dom psi by A1, Lm3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom psi or x in dom phi )
assume x in dom psi ; ::_thesis: x in dom phi
hence x in dom phi by A1, Lm3; ::_thesis: verum
end;
for x being set st x in dom phi holds
phi . x = psi . x by A1, Lm3;
hence phi = psi by A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th11: :: CARD_5:11
for phi being Ordinal-Sequence st phi is increasing holds
phi is one-to-one
proof
let phi be Ordinal-Sequence; ::_thesis: ( phi is increasing implies phi is one-to-one )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def_12 ::_thesis: phi is one-to-one
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom phi or not b1 in dom phi or not phi . x = phi . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom phi or not y in dom phi or not phi . x = phi . y or x = y )
assume that
A2: ( x in dom phi & y in dom phi ) and
A3: phi . x = phi . y ; ::_thesis: x = y
reconsider A = x, B = y as Ordinal by A2;
A4: ( A in B or A = B or B in A ) by ORDINAL1:14;
not phi . A in phi . B by A3;
hence x = y by A1, A2, A3, A4; ::_thesis: verum
end;
theorem Th12: :: CARD_5:12
for phi, psi being Ordinal-Sequence holds (phi ^ psi) | (dom phi) = phi
proof
let phi, psi be Ordinal-Sequence; ::_thesis: (phi ^ psi) | (dom phi) = phi
dom (phi ^ psi) = (dom phi) +^ (dom psi) by ORDINAL4:def_1;
then dom phi c= dom (phi ^ psi) by ORDINAL3:24;
then A1: dom phi = (dom (phi ^ psi)) /\ (dom phi) by XBOOLE_1:28;
for x being set st x in dom phi holds
phi . x = (phi ^ psi) . x by ORDINAL4:def_1;
hence (phi ^ psi) | (dom phi) = phi by A1, FUNCT_1:46; ::_thesis: verum
end;
theorem :: CARD_5:13
for X being set
for M being Cardinal st X <> {} holds
card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M))
proof
let X be set ; ::_thesis: for M being Cardinal st X <> {} holds
card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M))
let M be Cardinal; ::_thesis: ( X <> {} implies card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) )
set Z = { Y where Y is Subset of X : card Y in M } ;
X, card X are_equipotent by CARD_1:def_2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by WELLORD2:def_4;
defpred S1[ set , set ] means ex A being Ordinal ex phi being Ordinal-Sequence st
( $2 = [A,phi] & dom phi = M & phi | A is increasing & rng (phi | A) = f .: $1 & ( for B being Ordinal st A c= B & B in M holds
phi . B = {} ) );
A4: for x being set st x in { Y where Y is Subset of X : card Y in M } holds
ex y being set st S1[x,y]
proof
deffunc H1( set ) -> set = {} ;
let x be set ; ::_thesis: ( x in { Y where Y is Subset of X : card Y in M } implies ex y being set st S1[x,y] )
set A = order_type_of (RelIncl (f .: x));
consider xi2 being Ordinal-Sequence such that
A5: ( dom xi2 = M -^ (order_type_of (RelIncl (f .: x))) & ( for B being Ordinal st B in M -^ (order_type_of (RelIncl (f .: x))) holds
xi2 . B = H1(B) ) ) from ORDINAL2:sch_3();
assume x in { Y where Y is Subset of X : card Y in M } ; ::_thesis: ex y being set st S1[x,y]
then A6: ex Y being Subset of X st
( x = Y & card Y in M ) ;
consider xi1 being Ordinal-Sequence such that
xi1 = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (f .: x)))),(RelIncl (f .: x))) and
A7: xi1 is increasing and
A8: dom xi1 = order_type_of (RelIncl (f .: x)) and
A9: rng xi1 = f .: x by A3, Th5, RELAT_1:111;
set phi = xi1 ^ xi2;
take y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)]; ::_thesis: S1[x,y]
take order_type_of (RelIncl (f .: x)) ; ::_thesis: ex phi being Ordinal-Sequence st
( y = [(order_type_of (RelIncl (f .: x))),phi] & dom phi = M & phi | (order_type_of (RelIncl (f .: x))) is increasing & rng (phi | (order_type_of (RelIncl (f .: x)))) = f .: x & ( for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds
phi . B = {} ) )
take xi1 ^ xi2 ; ::_thesis: ( y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: x))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: x)))) = f .: x & ( for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds
(xi1 ^ xi2) . B = {} ) )
card (f .: x) = card (order_type_of (RelIncl (f .: x))) by A3, Th7, RELAT_1:111;
then card (order_type_of (RelIncl (f .: x))) in M by A6, CARD_1:67, ORDINAL1:12;
then order_type_of (RelIncl (f .: x)) in M by CARD_3:44;
then order_type_of (RelIncl (f .: x)) c= M by ORDINAL1:def_2;
then (order_type_of (RelIncl (f .: x))) +^ (M -^ (order_type_of (RelIncl (f .: x)))) = M by ORDINAL3:def_5;
hence ( y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: x))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: x)))) = f .: x ) by A7, A8, A9, A5, Th12, ORDINAL4:def_1; ::_thesis: for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds
(xi1 ^ xi2) . B = {}
let B be Ordinal; ::_thesis: ( order_type_of (RelIncl (f .: x)) c= B & B in M implies (xi1 ^ xi2) . B = {} )
assume that
A10: order_type_of (RelIncl (f .: x)) c= B and
A11: B in M ; ::_thesis: (xi1 ^ xi2) . B = {}
A12: B -^ (order_type_of (RelIncl (f .: x))) in M -^ (order_type_of (RelIncl (f .: x))) by A10, A11, ORDINAL3:53;
B = (order_type_of (RelIncl (f .: x))) +^ (B -^ (order_type_of (RelIncl (f .: x)))) by A10, ORDINAL3:def_5;
then (xi1 ^ xi2) . B = xi2 . (B -^ (order_type_of (RelIncl (f .: x)))) by A8, A5, A12, ORDINAL4:def_1;
hence (xi1 ^ xi2) . B = {} by A5, A12; ::_thesis: verum
end;
consider g being Function such that
A13: ( dom g = { Y where Y is Subset of X : card Y in M } & ( for x being set st x in { Y where Y is Subset of X : card Y in M } holds
S1[x,g . x] ) ) from CLASSES1:sch_1(A4);
assume A14: X <> {} ; ::_thesis: card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M))
rng g c= [:M,(Funcs (M,(card X))):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in [:M,(Funcs (M,(card X))):] )
assume x in rng g ; ::_thesis: x in [:M,(Funcs (M,(card X))):]
then consider y being set such that
A15: y in dom g and
A16: x = g . y by FUNCT_1:def_3;
consider A being Ordinal, phi being Ordinal-Sequence such that
A17: x = [A,phi] and
A18: dom phi = M and
A19: phi | A is increasing and
A20: rng (phi | A) = f .: y and
A21: for B being Ordinal st A c= B & B in M holds
phi . B = {} by A13, A15, A16;
A22: ex Y being Subset of X st
( y = Y & card Y in M ) by A13, A15;
rng phi c= card X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in card X )
assume x in rng phi ; ::_thesis: x in card X
then consider z being set such that
A23: z in dom phi and
A24: x = phi . z by FUNCT_1:def_3;
reconsider z = z as Ordinal by A23;
( z in A or A c= z ) by ORDINAL1:16;
then ( ( x in f .: y & f .: y c= card X ) or x = {} ) by A3, A18, A20, A21, A23, A24, FUNCT_1:50, RELAT_1:111;
hence x in card X by A14, ORDINAL3:8; ::_thesis: verum
end;
then A25: phi in Funcs (M,(card X)) by A18, FUNCT_2:def_2;
A26: ( A c= M or M c= A ) ;
phi | A is one-to-one by A19, Th11;
then dom (phi | A),f .: y are_equipotent by A20, WELLORD2:def_4;
then card (dom (phi | A)) = card (f .: y) by CARD_1:5;
then card (dom (phi | A)) in M by A22, CARD_1:67, ORDINAL1:12;
then A27: dom (phi | A) in M by CARD_3:44;
then dom (phi | A) <> M ;
then A in M by A18, A27, A26, RELAT_1:62, RELAT_1:68;
hence x in [:M,(Funcs (M,(card X))):] by A17, A25, ZFMISC_1:87; ::_thesis: verum
end;
then A28: card (rng g) c= card [:M,(Funcs (M,(card X))):] by CARD_1:11;
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 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
A29: x in dom g and
A30: y in dom g and
A31: g . x = g . y ; ::_thesis: x = y
consider A2 being Ordinal, phi2 being Ordinal-Sequence such that
A32: g . y = [A2,phi2] and
dom phi2 = M and
phi2 | A2 is increasing and
A33: rng (phi2 | A2) = f .: y and
for B being Ordinal st A2 c= B & B in M holds
phi2 . B = {} by A13, A30;
consider A1 being Ordinal, phi1 being Ordinal-Sequence such that
A34: g . x = [A1,phi1] and
dom phi1 = M and
phi1 | A1 is increasing and
A35: rng (phi1 | A1) = f .: x and
for B being Ordinal st A1 c= B & B in M holds
phi1 . B = {} by A13, A29;
A36: ( A1 = A2 & phi1 = phi2 ) by A31, A34, A32, XTUPLE_0:1;
A37: ex Y being Subset of X st
( x = Y & card Y in M ) by A13, A29;
thus x c= y :: according to XBOOLE_0:def_10 ::_thesis: y c= x
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x or z in y )
assume A38: z in x ; ::_thesis: z in y
then f . z in f .: x by A2, A37, FUNCT_1:def_6;
then ex x1 being set st
( x1 in dom f & x1 in y & f . z = f . x1 ) by A35, A33, A36, FUNCT_1:def_6;
hence z in y by A1, A2, A37, A38, FUNCT_1:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in y or z in x )
A39: ex Y being Subset of X st
( y = Y & card Y in M ) by A13, A30;
assume A40: z in y ; ::_thesis: z in x
then f . z in f .: y by A2, A39, FUNCT_1:def_6;
then ex x1 being set st
( x1 in dom f & x1 in x & f . z = f . x1 ) by A35, A33, A36, FUNCT_1:def_6;
hence z in x by A1, A2, A39, A40, FUNCT_1:def_4; ::_thesis: verum
end;
then A41: { Y where Y is Subset of X : card Y in M } , rng g are_equipotent by A13, WELLORD2:def_4;
card [:M,(Funcs (M,(card X))):] = card [:M,(card (Funcs (M,(card X)))):] by CARD_2:7
.= M *` (card (Funcs (M,(card X)))) by CARD_2:def_2
.= M *` (exp ((card X),M)) by CARD_2:def_3 ;
hence card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) by A41, A28, CARD_1:5; ::_thesis: verum
end;
theorem Th14: :: CARD_5:14
for M being Cardinal holds M in exp (2,M)
proof
let M be Cardinal; ::_thesis: M in exp (2,M)
( card (bool M) = exp (2,(card M)) & card M = M ) by CARD_1:def_2, CARD_2:31;
hence M in exp (2,M) by CARD_1:14; ::_thesis: verum
end;
registration
cluster epsilon-transitive epsilon-connected ordinal infinite cardinal for set ;
existence
ex b1 being Cardinal st b1 is infinite
proof
take omega ; ::_thesis: omega is infinite
thus omega is infinite ; ::_thesis: verum
end;
end;
registration
cluster infinite -> non empty for set ;
coherence
for b1 being set st b1 is infinite holds
not b1 is empty ;
end;
definition
mode Aleph is infinite Cardinal;
let M be Cardinal;
func cf M -> Cardinal means :Def1: :: CARD_5:def 1
( M is_cofinal_with it & ( for N being Cardinal st M is_cofinal_with N holds
it c= N ) );
existence
ex b1 being Cardinal st
( M is_cofinal_with b1 & ( for N being Cardinal st M is_cofinal_with N holds
b1 c= N ) )
proof
defpred S1[ Ordinal] means ( M is_cofinal_with $1 & $1 is Cardinal );
A1: ex A being Ordinal st S1[A] ;
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);
reconsider K = A as Cardinal by A2;
take K ; ::_thesis: ( M is_cofinal_with K & ( for N being Cardinal st M is_cofinal_with N holds
K c= N ) )
thus M is_cofinal_with K by A2; ::_thesis: for N being Cardinal st M is_cofinal_with N holds
K c= N
let N be Cardinal; ::_thesis: ( M is_cofinal_with N implies K c= N )
assume M is_cofinal_with N ; ::_thesis: K c= N
hence K c= N by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Cardinal st M is_cofinal_with b1 & ( for N being Cardinal st M is_cofinal_with N holds
b1 c= N ) & M is_cofinal_with b2 & ( for N being Cardinal st M is_cofinal_with N holds
b2 c= N ) holds
b1 = b2
proof
let K1, K2 be Cardinal; ::_thesis: ( M is_cofinal_with K1 & ( for N being Cardinal st M is_cofinal_with N holds
K1 c= N ) & M is_cofinal_with K2 & ( for N being Cardinal st M is_cofinal_with N holds
K2 c= N ) implies K1 = K2 )
assume ( M is_cofinal_with K1 & ( for N being Cardinal st M is_cofinal_with N holds
K1 c= N ) & M is_cofinal_with K2 & ( for N being Cardinal st M is_cofinal_with N holds
K2 c= N ) ) ; ::_thesis: K1 = K2
then ( K1 c= K2 & K2 c= K1 ) ;
hence K1 = K2 by XBOOLE_0:def_10; ::_thesis: verum
end;
let N be Cardinal;
funcN -powerfunc_of M -> Cardinal-Function means :Def2: :: CARD_5:def 2
( ( for x being set holds
( x in dom it iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
it . K = exp (K,N) ) );
existence
ex b1 being Cardinal-Function st
( ( for x being set holds
( x in dom b1 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b1 . K = exp (K,N) ) )
proof
deffunc H1( set ) -> set = exp ((card $1),N);
defpred S1[ set ] means $1 is Cardinal;
consider X being set such that
A3: for x being set holds
( x in X iff ( x in M & S1[x] ) ) from XBOOLE_0:sch_1();
consider f being Cardinal-Function such that
A4: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from CARD_3:sch_1();
take f ; ::_thesis: ( ( for x being set holds
( x in dom f iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
f . K = exp (K,N) ) )
thus for x being set holds
( x in dom f iff ( x in M & x is Cardinal ) ) by A3, A4; ::_thesis: for K being Cardinal st K in M holds
f . K = exp (K,N)
let K be Cardinal; ::_thesis: ( K in M implies f . K = exp (K,N) )
assume K in M ; ::_thesis: f . K = exp (K,N)
then ( K = card K & K in X ) by A3, CARD_1:def_2;
hence f . K = exp (K,N) by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Cardinal-Function st ( for x being set holds
( x in dom b1 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b1 . K = exp (K,N) ) & ( for x being set holds
( x in dom b2 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b2 . K = exp (K,N) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 in M & $1 is Cardinal );
let f1, f2 be Cardinal-Function; ::_thesis: ( ( for x being set holds
( x in dom f1 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
f1 . K = exp (K,N) ) & ( for x being set holds
( x in dom f2 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
f2 . K = exp (K,N) ) implies f1 = f2 )
assume that
A5: for x being set holds
( x in dom f1 iff S1[x] ) and
A6: for K being Cardinal st K in M holds
f1 . K = exp (K,N) and
A7: for x being set holds
( x in dom f2 iff S1[x] ) and
A8: for K being Cardinal st K in M holds
f2 . K = exp (K,N) ; ::_thesis: f1 = f2
A9: now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A10: x in dom f1 ; ::_thesis: f1 . x = f2 . x
then reconsider K = x as Cardinal by A5;
A11: K in M by A5, A10;
hence f1 . x = exp (K,N) by A6
.= f2 . x by A8, A11 ;
::_thesis: verum
end;
dom f1 = dom f2 from XBOOLE_0:sch_2(A5, A7);
hence f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines cf CARD_5:def_1_:_
for M, b2 being Cardinal holds
( b2 = cf M iff ( M is_cofinal_with b2 & ( for N being Cardinal st M is_cofinal_with N holds
b2 c= N ) ) );
:: deftheorem Def2 defines -powerfunc_of CARD_5:def_2_:_
for M, N being Cardinal
for b3 being Cardinal-Function holds
( b3 = N -powerfunc_of M iff ( ( for x being set holds
( x in dom b3 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b3 . K = exp (K,N) ) ) );
registration
let A be Ordinal;
cluster alef A -> infinite ;
coherence
not alef A is finite by Th3;
end;
begin
theorem :: CARD_5:15
for a being Aleph ex A being Ordinal st a = alef A by Th4;
theorem Th16: :: CARD_5:16
for n being Element of NAT
for a being Aleph holds
( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )
proof
let n be Element of NAT ; ::_thesis: for a being Aleph holds
( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )
let a be Aleph; ::_thesis: ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )
( omega c= a & card n in omega ) by CARD_3:85;
hence ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a ) ; ::_thesis: verum
end;
theorem Th17: :: CARD_5:17
for M being Cardinal
for a being Aleph st ( a c= M or a in M ) holds
M is Aleph
proof
let M be Cardinal; ::_thesis: for a being Aleph st ( a c= M or a in M ) holds
M is Aleph
let a be Aleph; ::_thesis: ( ( a c= M or a in M ) implies M is Aleph )
assume A1: ( a c= M or a in M ) ; ::_thesis: M is Aleph
omega c= a by Th16;
then omega c= M by A1, XBOOLE_1:1;
hence M is Aleph ; ::_thesis: verum
end;
theorem Th18: :: CARD_5:18
for M being Cardinal
for a being Aleph st ( a c= M or a in M ) holds
( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
proof
let M be Cardinal; ::_thesis: for a being Aleph st ( a c= M or a in M ) holds
( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
let a be Aleph; ::_thesis: ( ( a c= M or a in M ) implies ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) )
A1: card 0 in a by Th16;
assume A2: ( a c= M or a in M ) ; ::_thesis: ( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
then M is infinite by Th17;
hence ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) by A2, A1, CARD_2:76, CARD_4:16; ::_thesis: verum
end;
theorem :: CARD_5:19
for a being Aleph holds
( a +` a = a & a *` a = a ) by CARD_2:75, CARD_4:15;
theorem Th20: :: CARD_5:20
for M being Cardinal
for a being Aleph holds M c= exp (M,a)
proof
let M be Cardinal; ::_thesis: for a being Aleph holds M c= exp (M,a)
let a be Aleph; ::_thesis: M c= exp (M,a)
1 in a by Lm1, Th16;
then ( ( M = 0 & {} c= exp (M,a) ) or ( exp (M,1) c= exp (M,a) & exp (M,1) = M ) ) by CARD_2:27, CARD_2:93, XBOOLE_1:2;
hence M c= exp (M,a) ; ::_thesis: verum
end;
theorem :: CARD_5:21
for a being Aleph holds union a = a by ORDINAL1:def_6;
registration
let a be Aleph;
let M be Cardinal;
clustera +` M -> infinite ;
coherence
not a +` M is finite
proof
( a c= M or M c= a ) ;
then ( ( a +` M = M & M is Aleph ) or a +` M = a ) by Th18, CARD_2:76;
hence not a +` M is finite ; ::_thesis: verum
end;
end;
registration
let M be Cardinal;
let a be Aleph;
clusterM +` a -> infinite ;
coherence
not M +` a is finite ;
end;
registration
let a, b be Aleph;
clustera *` b -> infinite ;
coherence
not a *` b is finite
proof
( a c= b or b c= a ) ;
hence not a *` b is finite by Th18; ::_thesis: verum
end;
cluster exp (a,b) -> infinite ;
coherence
not exp (a,b) is finite
proof
1 in b by Lm1, Th16;
then A1: exp (a,1) c= exp (a,b) by CARD_2:92;
( exp (a,1) = a & omega c= a ) by Th16, CARD_2:27;
then omega c= exp (a,b) by A1, XBOOLE_1:1;
hence not exp (a,b) is finite ; ::_thesis: verum
end;
end;
begin
definition
let IT be Aleph;
attrIT is regular means :: CARD_5:def 3
cf IT = IT;
end;
:: deftheorem defines regular CARD_5:def_3_:_
for IT being Aleph holds
( IT is regular iff cf IT = IT );
notation
let IT be Aleph;
antonym irregular IT for regular ;
end;
registration
let a be Aleph;
cluster nextcard a -> infinite ;
coherence
not nextcard a is finite
proof
a in nextcard a by CARD_1:18;
then omega c= nextcard a ;
hence not nextcard a is finite ; ::_thesis: verum
end;
end;
theorem Th22: :: CARD_5:22
cf omega = omega
proof
defpred S1[ set , set ] means $2 c= $1;
assume A1: cf omega <> omega ; ::_thesis: contradiction
cf omega c= omega by Def1;
then cf omega in omega by A1, CARD_1:3;
then reconsider B = cf omega as finite set ;
set n = card B;
A2: for x, y being set st S1[x,y] & S1[y,x] holds
x = y by XBOOLE_0:def_10;
A3: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by XBOOLE_1:1;
card (cf omega) = cf omega by CARD_1:def_2;
then omega is_cofinal_with card B by Def1;
then consider xi being Ordinal-Sequence such that
A4: dom xi = card B and
A5: rng xi c= omega and
xi is increasing and
A6: omega = sup xi by ORDINAL2:def_17;
reconsider rxi = rng xi as finite set by A4, FINSET_1:8;
A7: rxi <> {} by A6, ORDINAL2:18;
consider x being set such that
A8: ( x in rxi & ( for y being set st y in rxi & y <> x holds
not S1[y,x] ) ) from CARD_2:sch_1(A7, A2, A3);
reconsider x = x as Ordinal by A5, A8;
now__::_thesis:_for_A_being_Ordinal_st_A_in_rng_xi_holds_
A_in_succ_x
let A be Ordinal; ::_thesis: ( A in rng xi implies A in succ x )
assume A in rng xi ; ::_thesis: A in succ x
then ( A c= x or not x c= A ) by A8;
hence A in succ x by ORDINAL1:22; ::_thesis: verum
end;
then A9: omega c= succ x by A6, ORDINAL2:20;
succ x in omega by A5, A8, ORDINAL1:28;
hence contradiction by A9; ::_thesis: verum
end;
Lm4: 1 = card 1
by CARD_1:def_2;
theorem Th23: :: CARD_5:23
for a being Aleph holds cf (nextcard a) = nextcard a
proof
let a be Aleph; ::_thesis: cf (nextcard a) = nextcard a
nextcard a is_cofinal_with cf (nextcard a) by Def1;
then consider xi being Ordinal-Sequence such that
A1: dom xi = cf (nextcard a) and
A2: rng xi c= nextcard a and
xi is increasing and
A3: nextcard a = sup xi by ORDINAL2:def_17;
A4: ( card (Union xi) c= Sum (Card xi) & Sum ((cf (nextcard a)) --> a) = (cf (nextcard a)) *` a ) by CARD_2:65, CARD_3:39;
A5: ( card (nextcard a) = nextcard a & succ (Union xi) = (Union xi) +^ 1 ) by CARD_1:def_2, ORDINAL2:31;
A6: now__::_thesis:_for_x_being_set_st_x_in_cf_(nextcard_a)_holds_
(Card_xi)_._x_c=_((cf_(nextcard_a))_-->_a)_._x
let x be set ; ::_thesis: ( x in cf (nextcard a) implies (Card xi) . x c= ((cf (nextcard a)) --> a) . x )
assume A7: x in cf (nextcard a) ; ::_thesis: (Card xi) . x c= ((cf (nextcard a)) --> a) . x
xi . x in rng xi by A1, A7, FUNCT_1:def_3;
then A8: card (xi . x) in nextcard a by A2, CARD_1:8, ORDINAL1:12;
( (Card xi) . x = card (xi . x) & ((cf (nextcard a)) --> a) . x = a ) by A1, A7, CARD_3:def_2, FUNCOP_1:7;
hence (Card xi) . x c= ((cf (nextcard a)) --> a) . x by A8, CARD_3:91; ::_thesis: verum
end;
( dom (Card xi) = dom xi & dom ((cf (nextcard a)) --> a) = cf (nextcard a) ) by CARD_3:def_2, FUNCOP_1:13;
then Sum (Card xi) c= Sum ((cf (nextcard a)) --> a) by A1, A6, CARD_3:30;
then card (Union xi) c= (cf (nextcard a)) *` a by A4, XBOOLE_1:1;
then A9: (card (Union xi)) +` 1 c= ((cf (nextcard a)) *` a) +` 1 by CARD_2:84;
A10: card ((Union xi) +^ 1) = (card (Union xi)) +` (card 1) by CARD_2:13;
ex A being Ordinal st rng xi c= A by ORDINAL2:def_4;
then On (rng xi) = rng xi by ORDINAL3:6;
then A11: card (nextcard a) c= card (succ (Union xi)) by A3, CARD_1:11, ORDINAL3:72;
A12: cf (nextcard a) c= nextcard a by Def1;
now__::_thesis:_cf_(nextcard_a)_=_nextcard_a
percases ( cf (nextcard a) = 0 or cf (nextcard a) <> 0 ) ;
suppose cf (nextcard a) = 0 ; ::_thesis: cf (nextcard a) = nextcard a
then A13: (cf (nextcard a)) *` a = 0 by CARD_2:20;
( 0 +` 1 = 1 & 1 in nextcard a ) by Lm1, Th16, CARD_2:18;
hence cf (nextcard a) = nextcard a by A11, A5, A9, A10, A13, Lm4; ::_thesis: verum
end;
supposeA14: cf (nextcard a) <> 0 ; ::_thesis: cf (nextcard a) = nextcard a
0 c= cf (nextcard a) by XBOOLE_1:2;
then A15: 0 in cf (nextcard a) by A14, CARD_1:3;
A16: ( cf (nextcard a) c= a or a c= cf (nextcard a) ) ;
1 in a by Lm1, Th16;
then A17: ( ( (cf (nextcard a)) *` a = a & a +` 1 = a & a in nextcard a ) or ( (cf (nextcard a)) *` a = cf (nextcard a) & cf (nextcard a) is Aleph ) ) by A15, A16, Th18, CARD_1:18, CARD_2:76, CARD_4:16;
then ( nextcard a c= (cf (nextcard a)) +` 1 & 1 in cf (nextcard a) ) by A11, A5, A9, A10, Lm1, Th16, CARD_1:4, XBOOLE_1:1;
then nextcard a c= cf (nextcard a) by A11, A5, A9, A10, A17, Lm1, CARD_1:4, CARD_2:76;
hence cf (nextcard a) = nextcard a by A12, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
hence cf (nextcard a) = nextcard a ; ::_thesis: verum
end;
theorem Th24: :: CARD_5:24
for a being Aleph holds omega c= cf a
proof
let a be Aleph; ::_thesis: omega c= cf a
A1: a is_cofinal_with cf a by Def1;
then cf a <> {} by ORDINAL2:50;
then A2: {} in cf a by ORDINAL3:8;
cf a is limit_ordinal by A1, ORDINAL4:38;
hence omega c= cf a by A2, ORDINAL1:def_11; ::_thesis: verum
end;
theorem :: CARD_5:25
for n being Element of NAT holds
( cf 0 = 0 & cf (card (n + 1)) = 1 )
proof
let n be Element of NAT ; ::_thesis: ( cf 0 = 0 & cf (card (n + 1)) = 1 )
A1: succ n is_cofinal_with 1 by ORDINAL3:73;
( card (n + 1) = n + 1 & n + 1 = succ n ) by CARD_1:def_2, NAT_1:38;
then cf (card (n + 1)) c= 1 by A1, Def1;
then A2: ( cf (card (n + 1)) = 1 or ( cf (card (n + 1)) = 0 & {} c= n & n in succ n ) ) by ORDINAL1:6, ORDINAL3:16, XBOOLE_1:2;
( cf 0 c= 0 & 0 c= cf 0 ) by Def1, XBOOLE_1:2;
hence cf 0 = 0 by XBOOLE_0:def_10; ::_thesis: cf (card (n + 1)) = 1
card (n + 1) is_cofinal_with cf (card (n + 1)) by Def1;
hence cf (card (n + 1)) = 1 by A2, ORDINAL2:50; ::_thesis: verum
end;
theorem Th26: :: CARD_5:26
for X being set
for M being Cardinal st X c= M & card X in cf M holds
( sup X in M & union X in M )
proof
let X be set ; ::_thesis: for M being Cardinal st X c= M & card X in cf M holds
( sup X in M & union X in M )
let M be Cardinal; ::_thesis: ( X c= M & card X in cf M implies ( sup X in M & union X in M ) )
assume that
A1: X c= M and
A2: card X in cf M ; ::_thesis: ( sup X in M & union X in M )
set A = order_type_of (RelIncl X);
A3: card (order_type_of (RelIncl X)) = card X by A1, Th7;
consider N being Cardinal such that
A4: N c= card (order_type_of (RelIncl X)) and
A5: order_type_of (RelIncl X) is_cofinal_with N and
for C being Ordinal st order_type_of (RelIncl X) is_cofinal_with C holds
N c= C by Th9;
sup X is_cofinal_with order_type_of (RelIncl X) by A1, Th6;
then A6: sup X is_cofinal_with N by A5, ORDINAL4:37;
A7: now__::_thesis:_not_sup_X_=_M
assume sup X = M ; ::_thesis: contradiction
then cf M c= N by A6, Def1;
hence contradiction by A2, A3, A4, CARD_1:4; ::_thesis: verum
end;
for x being set st x in X holds
x is Ordinal by A1;
then reconsider A = union X as Ordinal by ORDINAL1:23;
A8: sup M = M by ORDINAL2:18;
sup X c= sup M by A1, ORDINAL2:22;
then A9: sup X c< M by A8, A7, XBOOLE_0:def_8;
hence sup X in M by ORDINAL1:11; ::_thesis: union X in M
A c= sup X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in sup X )
assume x in A ; ::_thesis: x in sup X
then consider Y being set such that
A10: x in Y and
A11: Y in X by TARSKI:def_4;
reconsider Y = Y as Ordinal by A1, A11;
Y in sup X by A11, ORDINAL2:19;
then Y c= sup X by ORDINAL1:def_2;
hence x in sup X by A10; ::_thesis: verum
end;
hence union X in M by A9, ORDINAL1:11, ORDINAL1:12; ::_thesis: verum
end;
theorem Th27: :: CARD_5:27
for M, N being Cardinal
for phi being Ordinal-Sequence st dom phi = M & rng phi c= N & M in cf N holds
( sup phi in N & Union phi in N )
proof
let M, N be Cardinal; ::_thesis: for phi being Ordinal-Sequence st dom phi = M & rng phi c= N & M in cf N holds
( sup phi in N & Union phi in N )
let phi be Ordinal-Sequence; ::_thesis: ( dom phi = M & rng phi c= N & M in cf N implies ( sup phi in N & Union phi in N ) )
assume that
A1: dom phi = M and
A2: rng phi c= N and
A3: M in cf N ; ::_thesis: ( sup phi in N & Union phi in N )
A4: card M = M by CARD_1:def_2;
card (rng phi) c= card M by A1, CARD_1:12;
then card (rng phi) in cf N by A3, A4, ORDINAL1:12;
hence ( sup phi in N & Union phi in N ) by A2, Th26; ::_thesis: verum
end;
registration
let a be Aleph;
cluster cf a -> infinite ;
coherence
not cf a is finite by Th17, Th24;
end;
theorem Th28: :: CARD_5:28
for a being Aleph st cf a in a holds
a is limit_cardinal
proof
let a be Aleph; ::_thesis: ( cf a in a implies a is limit_cardinal )
assume A1: cf a in a ; ::_thesis: a is limit_cardinal
given M being Cardinal such that A2: a = nextcard M ; :: according to CARD_1:def_4 ::_thesis: contradiction
cf a c= M by A1, A2, CARD_3:91;
then reconsider M = M as Aleph ;
nextcard M in nextcard M by A1, A2, Th23;
hence contradiction ; ::_thesis: verum
end;
theorem Th29: :: CARD_5:29
for a being Aleph st cf a in a holds
ex xi being Ordinal-Sequence st
( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi )
proof
let a be Aleph; ::_thesis: ( cf a in a implies ex xi being Ordinal-Sequence st
( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi ) )
a is_cofinal_with cf a by Def1;
then consider xi being Ordinal-Sequence such that
A1: dom xi = cf a and
A2: rng xi c= a and
xi is increasing and
A3: a = sup xi by ORDINAL2:def_17;
deffunc H1( T-Sequence) -> set = (nextcard (xi . (dom $1))) \/ (nextcard (sup $1));
consider phi being T-Sequence such that
A4: ( dom phi = cf a & ( for A being Ordinal
for psi being T-Sequence st A in cf a & psi = phi | A holds
phi . A = H1(psi) ) ) from ORDINAL1:sch_4();
phi is Ordinal-yielding
proof
take sup (rng phi) ; :: according to ORDINAL2:def_4 ::_thesis: rng phi c= sup (rng phi)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in sup (rng phi) )
assume A5: x in rng phi ; ::_thesis: x in sup (rng phi)
then consider y being set such that
A6: y in dom phi and
A7: x = phi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A6;
y c= dom phi by A6, ORDINAL1:def_2;
then dom (phi | y) = y by RELAT_1:62;
then x = (nextcard (xi . y)) \/ (nextcard (sup (phi | y))) by A4, A6, A7;
hence x in sup (rng phi) by A5, ORDINAL2:19; ::_thesis: verum
end;
then reconsider phi = phi as Ordinal-Sequence ;
defpred S1[ Ordinal] means ( $1 in cf a implies phi . $1 in a );
assume cf a in a ; ::_thesis: ex xi being Ordinal-Sequence st
( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi )
then A8: a is limit_cardinal by Th28;
A9: now__::_thesis:_for_A_being_Ordinal_st_(_for_B_being_Ordinal_st_B_in_A_holds_
S1[B]_)_holds_
S1[A]
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A10: for B being Ordinal st B in A holds
S1[B] ; ::_thesis: S1[A]
thus S1[A] ::_thesis: verum
proof
assume A11: A in cf a ; ::_thesis: phi . A in a
then A12: card A in cf a by CARD_1:9;
A c= dom phi by A4, A11, ORDINAL1:def_2;
then A13: dom (phi | A) = A by RELAT_1:62;
then phi . A = (nextcard (xi . A)) \/ (nextcard (sup (phi | A))) by A4, A11;
then A14: ( phi . A = nextcard (xi . A) or phi . A = nextcard (sup (phi | A)) ) by ORDINAL3:12;
A15: rng (phi | A) c= a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (phi | A) or x in a )
assume x in rng (phi | A) ; ::_thesis: x in a
then consider y being set such that
A16: y in dom (phi | A) and
A17: x = (phi | A) . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A16;
( x = phi . y & y in cf a ) by A11, A13, A16, A17, FUNCT_1:47, ORDINAL1:10;
hence x in a by A10, A13, A16; ::_thesis: verum
end;
(phi | A) .: A = rng (phi | A) by A13, RELAT_1:113;
then card (rng (phi | A)) in cf a by A12, CARD_1:67, ORDINAL1:12;
then sup (rng (phi | A)) in a by A15, Th26;
then card (sup (phi | A)) in a by CARD_1:9;
then A18: nextcard (card (sup (phi | A))) c= a by CARD_3:90;
xi . A in rng xi by A1, A11, FUNCT_1:def_3;
then card (xi . A) in a by A2, CARD_1:9;
then A19: nextcard (card (xi . A)) c= a by CARD_3:90;
A20: ( nextcard (card (sup (phi | A))) <> a & nextcard (card (sup (phi | A))) = nextcard (sup (phi | A)) ) by A8, Th1, CARD_1:def_4;
( a <> nextcard (card (xi . A)) & nextcard (card (xi . A)) = nextcard (xi . A) ) by A8, Th1, CARD_1:def_4;
hence phi . A in a by A19, A18, A20, A14, CARD_1:3; ::_thesis: verum
end;
end;
A21: for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A9);
A22: rng phi c= a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in a )
assume x in rng phi ; ::_thesis: x in a
then ex y being set st
( y in dom phi & x = phi . y ) by FUNCT_1:def_3;
hence x in a by A4, A21; ::_thesis: verum
end;
take phi ; ::_thesis: ( dom phi = cf a & rng phi c= a & phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi )
thus dom phi = cf a by A4; ::_thesis: ( rng phi c= a & phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi )
thus rng phi c= a ::_thesis: ( phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in a )
assume x in rng phi ; ::_thesis: x in a
then ex y being set st
( y in dom phi & x = phi . y ) by FUNCT_1:def_3;
hence x in a by A4, A21; ::_thesis: verum
end;
thus phi is increasing ::_thesis: ( a = sup phi & phi is Cardinal-Function & not 0 in rng phi )
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom phi or phi . A in phi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume that
A23: A in B and
A24: B in dom phi ; ::_thesis: phi . A in phi . B
reconsider C = phi . A as Ordinal ;
A in dom phi by A23, A24, ORDINAL1:10;
then C in rng (phi | B) by A23, FUNCT_1:50;
then A25: C in sup (phi | B) by ORDINAL2:19;
sup (phi | B) in nextcard (sup (phi | B)) by CARD_1:18;
then A26: C in nextcard (sup (phi | B)) by A25, ORDINAL1:10;
phi . B = (nextcard (xi . (dom (phi | B)))) \/ (nextcard (sup (phi | B))) by A4, A24;
hence phi . A in phi . B by A26, XBOOLE_0:def_3; ::_thesis: verum
end;
thus a c= sup phi :: according to XBOOLE_0:def_10 ::_thesis: ( sup phi c= a & phi is Cardinal-Function & not 0 in rng phi )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in sup phi )
assume x in a ; ::_thesis: x in sup phi
then reconsider x = x as Element of a ;
consider A being Ordinal such that
A27: A in rng xi and
A28: x c= A by A3, ORDINAL2:21;
consider y being set such that
A29: y in dom xi and
A30: A = xi . y by A27, FUNCT_1:def_3;
reconsider y = y as Ordinal by A29;
y c= cf a by A1, A29, ORDINAL1:def_2;
then dom (phi | y) = y by A4, RELAT_1:62;
then ( A in nextcard A & phi . y = (nextcard A) \/ (nextcard (sup (phi | y))) ) by A1, A4, A29, A30, CARD_1:18;
then A in phi . y by XBOOLE_0:def_3;
then A31: A c= phi . y by ORDINAL1:def_2;
phi . y in rng phi by A1, A4, A29, FUNCT_1:def_3;
then phi . y in sup phi by ORDINAL2:19;
hence x in sup phi by A28, A31, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum
end;
sup a = a by ORDINAL2:18;
hence sup phi c= a by A22, ORDINAL2:22; ::_thesis: ( phi is Cardinal-Function & not 0 in rng phi )
phi is Cardinal-yielding
proof
let y be set ; :: according to CARD_3:def_1 ::_thesis: ( not y in dom phi or phi . y is set )
assume A32: y in dom phi ; ::_thesis: phi . y is set
then reconsider y = y as Ordinal ;
y c= dom phi by A32, ORDINAL1:def_2;
then dom (phi | y) = y by RELAT_1:62;
then phi . y = (nextcard (xi . y)) \/ (nextcard (sup (phi | y))) by A4, A32;
hence phi . y is set by ORDINAL3:12; ::_thesis: verum
end;
hence phi is Cardinal-Function ; ::_thesis: not 0 in rng phi
assume 0 in rng phi ; ::_thesis: contradiction
then consider x being set such that
A33: x in dom phi and
A34: 0 = phi . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A33;
x c= dom phi by A33, ORDINAL1:def_2;
then dom (phi | x) = x by RELAT_1:62;
then 0 = (nextcard (xi . x)) \/ (nextcard (sup (phi | x))) by A4, A33, A34;
then ( 0 = nextcard (xi . x) or 0 = nextcard (sup (phi | x)) ) ;
hence contradiction by CARD_1:15; ::_thesis: verum
end;
theorem :: CARD_5:30
for a being Aleph holds
( omega is regular & nextcard a is regular )
proof
let a be Aleph; ::_thesis: ( omega is regular & nextcard a is regular )
thus cf omega = omega by Th22; :: according to CARD_5:def_3 ::_thesis: nextcard a is regular
thus cf (nextcard a) = nextcard a by Th23; :: according to CARD_5:def_3 ::_thesis: verum
end;
begin
theorem Th31: :: CARD_5:31
for a, b being Aleph st a c= b holds
exp (a,b) = exp (2,b)
proof
let a, b be Aleph; ::_thesis: ( a c= b implies exp (a,b) = exp (2,b) )
A1: card (bool a) = exp (2,(card a)) by CARD_2:31;
( card a = a & card a in card (bool a) ) by CARD_1:14, CARD_1:def_2;
then A2: exp (a,b) c= exp ((exp (2,a)),b) by A1, CARD_2:92;
assume a c= b ; ::_thesis: exp (a,b) = exp (2,b)
then A3: ( exp ((exp (2,a)),b) = exp (2,(a *` b)) & a *` b = b ) by Th18, CARD_2:30;
2 in a by Lm2, Th16;
then exp (2,b) c= exp (a,b) by CARD_2:92;
hence exp (a,b) = exp (2,b) by A2, A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: CARD_5:32
for a, b being Aleph holds exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)
proof
let a, b be Aleph; ::_thesis: exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)
now__::_thesis:_exp_((nextcard_a),b)_=_(exp_(a,b))_*`_(nextcard_a)
percases ( a in b or b c= a ) by CARD_1:4;
supposeA1: a in b ; ::_thesis: exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)
then a c= b by CARD_1:3;
then A2: exp (a,b) = exp (2,b) by Th31;
nextcard a c= b by A1, CARD_3:90;
then ( exp ((nextcard a),b) = exp (2,b) & nextcard a in exp (2,b) ) by Th14, Th31, ORDINAL1:12;
hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) by A2, Th18; ::_thesis: verum
end;
supposeA3: b c= a ; ::_thesis: exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)
deffunc H1( Ordinal) -> set = Funcs (b,$1);
consider phi being T-Sequence such that
A4: ( dom phi = nextcard a & ( for A being Ordinal st A in nextcard a holds
phi . A = H1(A) ) ) from ORDINAL2:sch_2();
A5: cf (nextcard a) = nextcard a by Th23;
A6: b in nextcard a by A3, CARD_3:91;
Funcs (b,(nextcard a)) c= Union phi
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (b,(nextcard a)) or x in Union phi )
assume x in Funcs (b,(nextcard a)) ; ::_thesis: x in Union phi
then consider f being Function such that
A7: x = f and
A8: dom f = b and
A9: rng f c= nextcard a by FUNCT_2:def_2;
reconsider f = f as T-Sequence by A8, ORDINAL1:def_7;
reconsider f = f as Ordinal-Sequence by A9, ORDINAL2:def_4;
sup f in nextcard a by A6, A5, A8, A9, Th27;
then A10: phi . (sup f) in rng phi by A4, FUNCT_1:def_3;
rng f c= sup f by ORDINAL2:49;
then A11: f in Funcs (b,(sup f)) by A8, FUNCT_2:def_2;
phi . (sup f) = Funcs (b,(sup f)) by A6, A5, A4, A8, A9, Th27;
hence x in Union phi by A7, A11, A10, TARSKI:def_4; ::_thesis: verum
end;
then A12: card (Funcs (b,(nextcard a))) c= card (Union phi) by CARD_1:11;
( card (Funcs (b,(nextcard a))) = exp ((nextcard a),b) & card (Union phi) c= Sum (Card phi) ) by CARD_2:def_3, CARD_3:39;
then A13: exp ((nextcard a),b) c= Sum (Card phi) by A12, XBOOLE_1:1;
a in nextcard a by CARD_1:18;
then A14: ( (exp ((nextcard a),b)) *` (exp ((nextcard a),b)) = exp ((nextcard a),b) & exp (a,b) c= exp ((nextcard a),b) ) by CARD_2:92, CARD_4:15;
( exp ((nextcard a),1) = nextcard a & 1 in b ) by Lm1, Th16, CARD_2:27;
then nextcard a c= exp ((nextcard a),b) by CARD_2:92;
then A15: (exp (a,b)) *` (nextcard a) c= exp ((nextcard a),b) by A14, CARD_2:90;
A16: now__::_thesis:_for_x_being_set_st_x_in_nextcard_a_holds_
(Card_phi)_._x_c=_((nextcard_a)_-->_(exp_(a,b)))_._x
let x be set ; ::_thesis: ( x in nextcard a implies (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x )
A17: ( card (card x) = card x & card b = card b ) ;
assume A18: x in nextcard a ; ::_thesis: (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x
then reconsider x9 = x as Ordinal ;
A19: phi . x9 = Funcs (b,x9) by A4, A18;
card x in nextcard a by A18, CARD_1:8, ORDINAL1:12;
then card x c= a by CARD_3:91;
then Funcs (b,(card x)) c= Funcs (b,a) by FUNCT_5:56;
then A20: card (Funcs (b,(card x))) c= card (Funcs (b,a)) by CARD_1:11;
A21: card (Funcs (b,a)) = exp (a,b) by CARD_2:def_3;
( ((nextcard a) --> (exp (a,b))) . x = exp (a,b) & (Card phi) . x = card (phi . x) ) by A4, A18, CARD_3:def_2, FUNCOP_1:7;
hence (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x by A19, A17, A20, A21, FUNCT_5:61; ::_thesis: verum
end;
( dom (Card phi) = dom phi & dom ((nextcard a) --> (exp (a,b))) = nextcard a ) by CARD_3:def_2, FUNCOP_1:13;
then A22: Sum (Card phi) c= Sum ((nextcard a) --> (exp (a,b))) by A4, A16, CARD_3:30;
Sum ((nextcard a) --> (exp (a,b))) = (nextcard a) *` (exp (a,b)) by CARD_2:65;
then exp ((nextcard a),b) c= (exp (a,b)) *` (nextcard a) by A13, A22, XBOOLE_1:1;
hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) by A15, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) ; ::_thesis: verum
end;
theorem Th33: :: CARD_5:33
for b, a being Aleph holds Sum (b -powerfunc_of a) c= exp (a,b)
proof
let b, a be Aleph; ::_thesis: Sum (b -powerfunc_of a) c= exp (a,b)
set X = { c where c is Element of a : c is Cardinal } ;
set f = { c where c is Element of a : c is Cardinal } --> (exp (a,b));
{ c where c is Element of a : c is Cardinal } c= a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { c where c is Element of a : c is Cardinal } or x in a )
assume x in { c where c is Element of a : c is Cardinal } ; ::_thesis: x in a
then ex c being Element of a st
( x = c & c is Cardinal ) ;
hence x in a ; ::_thesis: verum
end;
then A1: { c where c is Element of a : c is Cardinal } --> (exp (a,b)) c= a --> (exp (a,b)) by FUNCT_4:4;
Sum (a --> (exp (a,b))) = a *` (exp (a,b)) by CARD_2:65;
then A2: Sum ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) c= a *` (exp (a,b)) by A1, CARD_3:33;
A3: ( dom ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) = { c where c is Element of a : c is Cardinal } & dom (b -powerfunc_of a) = { c where c is Element of a : c is Cardinal } )
proof
thus dom ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) = { c where c is Element of a : c is Cardinal } by FUNCOP_1:13; ::_thesis: dom (b -powerfunc_of a) = { c where c is Element of a : c is Cardinal }
thus dom (b -powerfunc_of a) c= { c where c is Element of a : c is Cardinal } :: according to XBOOLE_0:def_10 ::_thesis: { c where c is Element of a : c is Cardinal } c= dom (b -powerfunc_of a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (b -powerfunc_of a) or x in { c where c is Element of a : c is Cardinal } )
assume x in dom (b -powerfunc_of a) ; ::_thesis: x in { c where c is Element of a : c is Cardinal }
then ( x in a & x is Cardinal ) by Def2;
hence x in { c where c is Element of a : c is Cardinal } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { c where c is Element of a : c is Cardinal } or x in dom (b -powerfunc_of a) )
assume x in { c where c is Element of a : c is Cardinal } ; ::_thesis: x in dom (b -powerfunc_of a)
then ex c being Element of a st
( x = c & c is Cardinal ) ;
hence x in dom (b -powerfunc_of a) by Def2; ::_thesis: verum
end;
( 1 in b & exp (a,1) = a ) by Lm1, Th16, CARD_2:27;
then a c= exp (a,b) by CARD_2:93;
then A4: a *` (exp (a,b)) = exp (a,b) by Th18;
now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_a_:_c_is_Cardinal__}__holds_
(b_-powerfunc_of_a)_._x_c=_(_{__c_where_c_is_Element_of_a_:_c_is_Cardinal__}__-->_(exp_(a,b)))_._x
let x be set ; ::_thesis: ( x in { c where c is Element of a : c is Cardinal } implies (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x )
assume A5: x in { c where c is Element of a : c is Cardinal } ; ::_thesis: (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x
then consider c being Element of a such that
A6: x = c and
A7: c is Cardinal ;
reconsider c = c as Cardinal by A7;
A8: ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x = exp (a,b) by A5, FUNCOP_1:7;
(b -powerfunc_of a) . x = exp (c,b) by A6, Def2;
hence (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x by A8, CARD_2:93; ::_thesis: verum
end;
then Sum (b -powerfunc_of a) c= Sum ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) by A3, CARD_3:30;
hence Sum (b -powerfunc_of a) c= exp (a,b) by A2, A4, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: CARD_5:34
for a, b being Aleph st a is limit_cardinal & b in cf a holds
exp (a,b) = Sum (b -powerfunc_of a)
proof
let a, b be Aleph; ::_thesis: ( a is limit_cardinal & b in cf a implies exp (a,b) = Sum (b -powerfunc_of a) )
assume that
A1: a is limit_cardinal and
A2: b in cf a ; ::_thesis: exp (a,b) = Sum (b -powerfunc_of a)
deffunc H1( Ordinal) -> set = Funcs (b,$1);
consider L being T-Sequence such that
A3: ( dom L = a & ( for A being Ordinal st A in a holds
L . A = H1(A) ) ) from ORDINAL2:sch_2();
A4: now__::_thesis:_for_x_being_set_st_x_in_a_holds_
(Card_L)_._x_c=_(a_-->_(Sum_(b_-powerfunc_of_a)))_._x
let x be set ; ::_thesis: ( x in a implies (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x )
A5: card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) by CARD_3:40;
assume A6: x in a ; ::_thesis: (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x
then reconsider x9 = x as Ordinal ;
set m = card x9;
A7: card x9 in a by A6, CARD_1:8, ORDINAL1:12;
then card x9 in dom (b -powerfunc_of a) by Def2;
then A8: (b -powerfunc_of a) . (card x) in rng (b -powerfunc_of a) by FUNCT_1:def_3;
x9, card x9 are_equipotent by CARD_1:def_2;
then A9: card (Funcs (b,x9)) = card (Funcs (b,(card x9))) by FUNCT_5:60;
( L . x = Funcs (b,x9) & (Card L) . x = card (L . x) ) by A3, A6, CARD_3:def_2;
then A10: (Card L) . x = exp ((card x9),b) by A9, CARD_2:def_3;
(b -powerfunc_of a) . (card x) = exp ((card x),b) by A7, Def2;
then card (exp ((card x),b)) c= card (Union (b -powerfunc_of a)) by A8, CARD_1:11, ZFMISC_1:74;
then A11: card (exp ((card x),b)) c= Sum (b -powerfunc_of a) by A5, XBOOLE_1:1;
card (exp ((card x),b)) = exp ((card x),b) by CARD_1:def_2;
hence (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x by A6, A10, A11, FUNCOP_1:7; ::_thesis: verum
end;
( dom (a --> (Sum (b -powerfunc_of a))) = a & dom (Card L) = dom L ) by CARD_3:def_2, FUNCOP_1:13;
then A12: Sum (Card L) c= Sum (a --> (Sum (b -powerfunc_of a))) by A3, A4, CARD_3:30;
a c= Sum (b -powerfunc_of a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in Sum (b -powerfunc_of a) )
assume A13: x in a ; ::_thesis: x in Sum (b -powerfunc_of a)
then reconsider x9 = x as Ordinal ;
set m = card x9;
card x9 in a by A13, CARD_1:8, ORDINAL1:12;
then A14: nextcard (card x9) c= a by CARD_3:90;
nextcard (card x9) <> a by A1, CARD_1:def_4;
then A15: nextcard (card x9) in a by A14, CARD_1:3;
then nextcard (card x9) in dom (b -powerfunc_of a) by Def2;
then A16: (b -powerfunc_of a) . (nextcard (card x9)) in rng (b -powerfunc_of a) by FUNCT_1:def_3;
(b -powerfunc_of a) . (nextcard (card x9)) = exp ((nextcard (card x9)),b) by A15, Def2;
then A17: card (exp ((nextcard (card x9)),b)) c= card (Union (b -powerfunc_of a)) by A16, CARD_1:11, ZFMISC_1:74;
A18: nextcard (card x9) c= exp ((nextcard (card x9)),b) by Th20;
card x = card (card x) ;
then A19: ( x9 in nextcard x9 & nextcard (card x) = nextcard x ) by CARD_1:18, CARD_3:88;
( card (exp ((nextcard (card x9)),b)) = exp ((nextcard (card x9)),b) & card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) ) by CARD_1:def_2, CARD_3:40;
then exp ((nextcard (card x9)),b) c= Sum (b -powerfunc_of a) by A17, XBOOLE_1:1;
then nextcard (card x) c= Sum (b -powerfunc_of a) by A18, XBOOLE_1:1;
hence x in Sum (b -powerfunc_of a) by A19; ::_thesis: verum
end;
then A20: a *` (Sum (b -powerfunc_of a)) = Sum (b -powerfunc_of a) by Th18;
Funcs (b,a) c= Union L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (b,a) or x in Union L )
assume x in Funcs (b,a) ; ::_thesis: x in Union L
then consider f being Function such that
A21: x = f and
A22: dom f = b and
A23: rng f c= a by FUNCT_2:def_2;
reconsider f = f as T-Sequence by A22, ORDINAL1:def_7;
reconsider f = f as Ordinal-Sequence by A23, ORDINAL2:def_4;
rng f c= sup f by ORDINAL2:49;
then A24: x in Funcs (b,(sup f)) by A21, A22, FUNCT_2:def_2;
sup f in a by A2, A22, A23, Th27;
then A25: L . (sup f) in rng L by A3, FUNCT_1:def_3;
L . (sup f) = Funcs (b,(sup f)) by A2, A3, A22, A23, Th27;
hence x in Union L by A24, A25, TARSKI:def_4; ::_thesis: verum
end;
then A26: card (Funcs (b,a)) c= card (Union L) by CARD_1:11;
card (Union L) c= Sum (Card L) by CARD_3:39;
then card (Funcs (b,a)) c= Sum (Card L) by A26, XBOOLE_1:1;
then A27: exp (a,b) c= Sum (Card L) by CARD_2:def_3;
A28: Sum (b -powerfunc_of a) c= exp (a,b) by Th33;
Sum (a --> (Sum (b -powerfunc_of a))) = a *` (Sum (b -powerfunc_of a)) by CARD_2:65;
then exp (a,b) c= a *` (Sum (b -powerfunc_of a)) by A27, A12, XBOOLE_1:1;
hence exp (a,b) = Sum (b -powerfunc_of a) by A28, A20, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: CARD_5:35
for a, b being Aleph st cf a c= b & b in a holds
exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a))
proof
let a, b be Aleph; ::_thesis: ( cf a c= b & b in a implies exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a)) )
assume that
A1: cf a c= b and
A2: b in a ; ::_thesis: exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a))
consider phi being Ordinal-Sequence such that
A3: dom phi = cf a and
A4: rng phi c= a and
phi is increasing and
A5: a = sup phi and
A6: phi is Cardinal-Function and
A7: not 0 in rng phi by A1, A2, Th29, ORDINAL1:12;
defpred S1[ set , set ] means ex g, h being Function st
( g = $1 & h = $2 & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) );
A8: for x being set st x in Funcs (b,a) holds
ex x1 being set st S1[x,x1]
proof
let x be set ; ::_thesis: ( x in Funcs (b,a) implies ex x1 being set st S1[x,x1] )
assume x in Funcs (b,a) ; ::_thesis: ex x1 being set st S1[x,x1]
then consider g being Function such that
A9: ( x = g & dom g = b & rng g c= a ) by FUNCT_2:def_2;
defpred S2[ set , set ] means ex fx being Function st
( $2 = [fx,(phi . $1)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . $1 implies fx . z = g . z ) & ( not g . z in phi . $1 implies fx . z = 0 ) ) ) );
A10: for y being set st y in cf a holds
ex x2 being set st S2[y,x2]
proof
deffunc H1( set ) -> Element of NAT = 0 ;
deffunc H2( set ) -> set = g . $1;
let y be set ; ::_thesis: ( y in cf a implies ex x2 being set st S2[y,x2] )
assume y in cf a ; ::_thesis: ex x2 being set st S2[y,x2]
defpred S3[ set ] means g . $1 in phi . y;
consider fx being Function such that
A11: ( dom fx = b & ( for z being set st z in b holds
( ( S3[z] implies fx . z = H2(z) ) & ( not S3[z] implies fx . z = H1(z) ) ) ) ) from PARTFUN1:sch_1();
take [fx,(phi . y)] ; ::_thesis: S2[y,[fx,(phi . y)]]
take fx ; ::_thesis: ( [fx,(phi . y)] = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) )
thus ( [fx,(phi . y)] = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) by A11; ::_thesis: verum
end;
consider h being Function such that
A12: ( dom h = cf a & ( for y being set st y in cf a holds
S2[y,h . y] ) ) from CLASSES1:sch_1(A10);
take h ; ::_thesis: S1[x,h]
take g ; ::_thesis: ex h being Function st
( g = x & h = h & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) )
take h ; ::_thesis: ( g = x & h = h & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) )
thus ( g = x & h = h & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) ) by A9, A12; ::_thesis: verum
end;
consider f being Function such that
A13: ( dom f = Funcs (b,a) & ( for x being set st x in Funcs (b,a) holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A8);
deffunc H1( set ) -> set = Funcs (b,$1);
consider F being Function such that
A14: ( dom F = dom (b -powerfunc_of a) & ( for x being set st x in dom (b -powerfunc_of a) holds
F . x = H1(x) ) ) from FUNCT_1:sch_3();
A15: rng f c= Funcs ((cf a),(Union (disjoin F)))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Funcs ((cf a),(Union (disjoin F))) )
assume y in rng f ; ::_thesis: y in Funcs ((cf a),(Union (disjoin F)))
then consider x being set such that
A16: x in dom f and
A17: y = f . x by FUNCT_1:def_3;
consider g, h being Function such that
g = x and
A18: h = f . x and
dom g = b and
rng g c= a and
A19: dom h = cf a and
A20: for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) by A13, A16;
rng h c= Union (disjoin F)
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in rng h or x1 in Union (disjoin F) )
assume x1 in rng h ; ::_thesis: x1 in Union (disjoin F)
then consider x2 being set such that
A21: x2 in dom h and
A22: x1 = h . x2 by FUNCT_1:def_3;
consider fx being Function such that
A23: x1 = [fx,(phi . x2)] and
A24: dom fx = b and
A25: for z being set st z in b holds
( ( g . z in phi . x2 implies fx . z = g . z ) & ( not g . z in phi . x2 implies fx . z = 0 ) ) by A19, A20, A21, A22;
rng fx c= phi . x2
proof
reconsider x2 = x2 as Ordinal by A19, A21;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng fx or z in phi . x2 )
reconsider A = phi . x2 as Ordinal ;
assume z in rng fx ; ::_thesis: z in phi . x2
then consider z9 being set such that
A26: ( z9 in dom fx & z = fx . z9 ) by FUNCT_1:def_3;
A27: ( ( z = g . z9 & g . z9 in phi . x2 ) or z = 0 ) by A24, A25, A26;
A <> 0 by A3, A7, A19, A21, FUNCT_1:def_3;
hence z in phi . x2 by A27, ORDINAL3:8; ::_thesis: verum
end;
then A28: fx in Funcs (b,(phi . x2)) by A24, FUNCT_2:def_2;
A29: ( [fx,(phi . x2)] `1 = fx & [fx,(phi . x2)] `2 = phi . x2 ) ;
( phi . x2 in rng phi & phi . x2 is Cardinal ) by A3, A6, A19, A21, CARD_3:def_1, FUNCT_1:def_3;
then A30: phi . x2 in dom (b -powerfunc_of a) by A4, Def2;
then F . (phi . x2) = Funcs (b,(phi . x2)) by A14;
hence x1 in Union (disjoin F) by A14, A23, A28, A30, A29, CARD_3:22; ::_thesis: verum
end;
hence y in Funcs ((cf a),(Union (disjoin F))) by A17, A18, A19, FUNCT_2:def_2; ::_thesis: verum
end;
( card (card (Union (disjoin F))) = card (Union (disjoin F)) & card (cf a) = cf a ) by CARD_1:def_2;
then A31: card (Funcs ((cf a),(Union (disjoin F)))) = card (Funcs ((cf a),(card (Union (disjoin F))))) by FUNCT_5:61
.= exp ((card (Union (disjoin F))),(cf a)) by CARD_2:def_3 ;
A32: dom (Card F) = dom F by CARD_3:def_2;
A33: 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
A34: x in dom f and
A35: y in dom f and
A36: f . x = f . y ; ::_thesis: x = y
consider g1, h1 being Function such that
A37: g1 = x and
A38: h1 = f . x and
A39: dom g1 = b and
A40: rng g1 c= a and
dom h1 = cf a and
A41: for x1 being set st x1 in cf a holds
ex fx being Function st
( h1 . x1 = [fx,(phi . x1)] & dom fx = b & ( for z being set st z in b holds
( ( g1 . z in phi . x1 implies fx . z = g1 . z ) & ( not g1 . z in phi . x1 implies fx . z = 0 ) ) ) ) by A13, A34;
consider g2, h2 being Function such that
A42: g2 = y and
A43: h2 = f . y and
A44: dom g2 = b and
A45: rng g2 c= a and
dom h2 = cf a and
A46: for x2 being set st x2 in cf a holds
ex fx being Function st
( h2 . x2 = [fx,(phi . x2)] & dom fx = b & ( for z being set st z in b holds
( ( g2 . z in phi . x2 implies fx . z = g2 . z ) & ( not g2 . z in phi . x2 implies fx . z = 0 ) ) ) ) by A13, A35;
now__::_thesis:_for_x1_being_set_st_x1_in_b_holds_
g1_._x1_=_g2_._x1
let x1 be set ; ::_thesis: ( x1 in b implies g1 . x1 = g2 . x1 )
assume x1 in b ; ::_thesis: g1 . x1 = g2 . x1
then reconsider X = x1 as Element of b ;
( g1 . X in rng g1 & g2 . X in rng g2 ) by A39, A44, FUNCT_1:def_3;
then reconsider A1 = g1 . x1, A2 = g2 . x1 as Element of a by A40, A45;
set A = A1 \/ A2;
( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12;
then succ (A1 \/ A2) in a by ORDINAL1:28;
then consider B being Ordinal such that
A47: B in rng phi and
A48: succ (A1 \/ A2) c= B by A5, ORDINAL2:21;
consider x2 being set such that
A49: x2 in dom phi and
A50: B = phi . x2 by A47, FUNCT_1:def_3;
A51: A1 \/ A2 in succ (A1 \/ A2) by ORDINAL1:6;
then A52: A2 in B by A48, ORDINAL1:12, XBOOLE_1:7;
consider f1 being Function such that
A53: h1 . x2 = [f1,(phi . x2)] and
dom f1 = b and
A54: for z being set st z in b holds
( ( g1 . z in phi . x2 implies f1 . z = g1 . z ) & ( not g1 . z in phi . x2 implies f1 . z = 0 ) ) by A3, A41, A49;
A1 in B by A48, A51, ORDINAL1:12, XBOOLE_1:7;
then A55: f1 . X = g1 . x1 by A50, A54;
consider f2 being Function such that
A56: h2 . x2 = [f2,(phi . x2)] and
dom f2 = b and
A57: for z being set st z in b holds
( ( g2 . z in phi . x2 implies f2 . z = g2 . z ) & ( not g2 . z in phi . x2 implies f2 . z = 0 ) ) by A3, A46, A49;
f1 = f2 by A36, A38, A43, A53, A56, XTUPLE_0:1;
hence g1 . x1 = g2 . x1 by A50, A57, A52, A55; ::_thesis: verum
end;
hence x = y by A37, A39, A42, A44, FUNCT_1:2; ::_thesis: verum
end;
A58: dom (disjoin F) = dom F by CARD_3:def_3;
A59: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
(Card_(disjoin_F))_._x_=_(Card_F)_._x
let x be set ; ::_thesis: ( x in dom F implies (Card (disjoin F)) . x = (Card F) . x )
assume A60: x in dom F ; ::_thesis: (Card (disjoin F)) . x = (Card F) . x
then A61: (disjoin F) . x = [:(F . x),{x}:] by CARD_3:def_3;
( (Card F) . x = card (F . x) & (Card (disjoin F)) . x = card ((disjoin F) . x) ) by A58, A60, CARD_3:def_2;
hence (Card (disjoin F)) . x = (Card F) . x by A61, CARD_1:69; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
(Card_F)_._x_=_(b_-powerfunc_of_a)_._x
let x be set ; ::_thesis: ( x in dom F implies (Card F) . x = (b -powerfunc_of a) . x )
assume A62: x in dom F ; ::_thesis: (Card F) . x = (b -powerfunc_of a) . x
then reconsider M = x as Cardinal by A14, Def2;
M in a by A14, A62, Def2;
then A63: (b -powerfunc_of a) . M = exp (M,b) by Def2;
( (Card F) . x = card (F . x) & F . x = Funcs (b,x) ) by A14, A62, CARD_3:def_2;
hence (Card F) . x = (b -powerfunc_of a) . x by A63, CARD_2:def_3; ::_thesis: verum
end;
then A64: Card F = b -powerfunc_of a by A14, A32, FUNCT_1:2;
dom (Card (disjoin F)) = dom (disjoin F) by CARD_3:def_2;
then Card F = Card (disjoin F) by A58, A32, A59, FUNCT_1:2;
then card (Union (disjoin F)) c= Sum (b -powerfunc_of a) by A64, CARD_3:39;
then A65: exp ((card (Union (disjoin F))),(cf a)) c= exp ((Sum (b -powerfunc_of a)),(cf a)) by CARD_2:93;
exp (a,b) = card (Funcs (b,a)) by CARD_2:def_3;
then exp (a,b) c= card (Funcs ((cf a),(Union (disjoin F)))) by A13, A33, A15, CARD_1:10;
then A66: ( exp ((exp (a,b)),(cf a)) = exp (a,(b *` (cf a))) & exp (a,b) c= exp ((Sum (b -powerfunc_of a)),(cf a)) ) by A31, A65, CARD_2:30, XBOOLE_1:1;
Sum (b -powerfunc_of a) c= exp (a,b) by Th33;
then A67: exp ((Sum (b -powerfunc_of a)),(cf a)) c= exp ((exp (a,b)),(cf a)) by CARD_2:93;
b *` (cf a) = b by A1, Th18;
hence exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a)) by A67, A66, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm5: for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
proof
let O be Ordinal; ::_thesis: for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
let X be finite set ; ::_thesis: ( X c= O implies order_type_of (RelIncl X) is finite )
assume X c= O ; ::_thesis: order_type_of (RelIncl X) is finite
then RelIncl X is well-ordering by WELLORD2:8;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2;
hence order_type_of (RelIncl X) is finite by CARD_3:105; ::_thesis: verum
end;
theorem Th36: :: CARD_5:36
for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) = card X
proof
let O be Ordinal; ::_thesis: for X being finite set st X c= O holds
order_type_of (RelIncl X) = card X
let X be finite set ; ::_thesis: ( X c= O implies order_type_of (RelIncl X) = card X )
assume A1: X c= O ; ::_thesis: order_type_of (RelIncl X) = card X
then order_type_of (RelIncl X) is finite by Lm5;
then reconsider o = order_type_of (RelIncl X) as Nat ;
card X = card (order_type_of (RelIncl X)) by A1, Th7;
then o = card X by CARD_1:def_2;
hence order_type_of (RelIncl X) = card X ; ::_thesis: verum
end;
theorem Th37: :: CARD_5:37
for x being set
for O being Ordinal st {x} c= O holds
order_type_of (RelIncl {x}) = 1
proof
let x be set ; ::_thesis: for O being Ordinal st {x} c= O holds
order_type_of (RelIncl {x}) = 1
let O be Ordinal; ::_thesis: ( {x} c= O implies order_type_of (RelIncl {x}) = 1 )
card {x} = 1 by CARD_2:42;
hence ( {x} c= O implies order_type_of (RelIncl {x}) = 1 ) by Th36; ::_thesis: verum
end;
theorem :: CARD_5:38
for x being set
for O being Ordinal st {x} c= O holds
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x
proof
let x be set ; ::_thesis: for O being Ordinal st {x} c= O holds
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x
let O be Ordinal; ::_thesis: ( {x} c= O implies canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x )
set X = {x};
set R = RelIncl {x};
set C = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x}));
A1: RelIncl {0} = {[0,0]} by WELLORD2:22;
assume A2: {x} c= O ; ::_thesis: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x
then A3: order_type_of (RelIncl {x}) = {0} by Th37, CARD_1:49;
RelIncl {x} is well-ordering by A2, WELLORD2:8;
then RelIncl {x}, RelIncl (order_type_of (RelIncl {x})) are_isomorphic by WELLORD2:def_2;
then A4: RelIncl (order_type_of (RelIncl {x})), RelIncl {x} are_isomorphic by WELLORD1:40;
RelIncl (order_type_of (RelIncl {x})) is well-ordering by WELLORD2:8;
then A5: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) is_isomorphism_of RelIncl (order_type_of (RelIncl {x})), RelIncl {x} by A4, WELLORD1:def_9;
then A6: rng (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {x}))) = field (RelIncl {x}) by A3, WELLORD1:def_7
.= {x} by WELLORD2:def_1 ;
dom (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {x}))) = field (RelIncl {0}) by A5, A3, WELLORD1:def_7
.= {0} by A1, RELAT_1:173 ;
hence canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x by A3, A6, FUNCT_4:112; ::_thesis: verum
end;
registration
let O be Ordinal;
let X be Subset of O;
let n be set ;
cluster(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n -> ordinal ;
coherence
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal
proof
consider phi being Ordinal-Sequence such that
A1: phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) and
phi is increasing and
dom phi = order_type_of (RelIncl X) and
A2: rng phi = X by Th5;
percases ( n in dom phi or not n in dom phi ) ;
suppose n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal
then phi . n in rng phi by FUNCT_1:def_3;
hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal by A1, A2; ::_thesis: verum
end;
suppose not n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal
hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
end;
registration
let X be natural-membered set ;
let n be set ;
cluster(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n -> natural ;
coherence
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural
proof
X c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in NAT )
assume x in X ; ::_thesis: x in NAT
hence x in NAT by ORDINAL1:def_12; ::_thesis: verum
end;
then reconsider X = X as Subset of NAT ;
consider phi being Ordinal-Sequence such that
A1: phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) and
phi is increasing and
dom phi = order_type_of (RelIncl X) and
A2: rng phi = X by Th5;
percases ( n in dom phi or not n in dom phi ) ;
supposeA3: n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural
phi . n in rng phi by A3, FUNCT_1:def_3;
hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural by A1, A2; ::_thesis: verum
end;
suppose not n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural
hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
end;
theorem :: CARD_5:39
for F being Subset of omega holds card F c= order_type_of (RelIncl F)
proof
let F be Subset of omega; ::_thesis: card F c= order_type_of (RelIncl F)
card F = card (order_type_of (RelIncl F)) by Th7;
hence card F c= order_type_of (RelIncl F) by CARD_1:8; ::_thesis: verum
end;