:: On Powers of Cardinals
:: by Grzegorz Bancerek
::
:: Received August 24, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


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

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 ) )
proofend;

theorem Th3: :: CARD_5:3
for A being Ordinal holds alef A is infinite
proofend;

theorem Th4: :: CARD_5:4
for M being Cardinal st M is infinite holds
ex A being Ordinal st M = alef A
proofend;

registration
let phi be Ordinal-Sequence;
cluster Union phi ->  ordinal ;
coherence
 Union phi is ordinal
proofend;
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 )
proofend;

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)
proofend;

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))
proofend;

theorem Th8: :: CARD_5:8
for A being Ordinal ex B being Ordinal st
( B c= card A & A is_cofinal_with B )
proofend;

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 ) )
proofend;

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 )
proofend;

theorem :: CARD_5:10
for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
phi = psi
proofend;

theorem Th11: :: CARD_5:11
for phi being Ordinal-Sequence st phi is increasing holds
phi is one-to-one
proofend;

theorem Th12: :: CARD_5:12
for phi, psi being Ordinal-Sequence holds (phi ^ psi) | (dom phi) = phi
proofend;

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))
proofend;

theorem Th14: :: CARD_5:14
for M being Cardinal holds M in exp (2,M)
proofend;

registration
cluster epsilon-transitive epsilon-connected ordinal infinite cardinal for set ;
existence
 ex b1 being Cardinal st b1 is infinite
proofend;
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 &amp; ( 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 &amp; ( for N being Cardinal st M is_cofinal_with N holds
b1 c= N ) )
proofend;
uniqueness
 for b1, b2 being Cardinal st M is_cofinal_with b1 &amp; ( for N being Cardinal st M is_cofinal_with N holds
b1 c= N ) &amp; M is_cofinal_with b2 &amp; ( for N being Cardinal st M is_cofinal_with N holds
b2 c= N ) holds
b1 = b2
proofend;
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 &amp; x is Cardinal ) ) ) &amp; ( 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 &amp; x is Cardinal ) ) ) &amp; ( for K being Cardinal st K in M holds
b1 . K = exp (K,N) ) )
proofend;
uniqueness
 for b1, b2 being Cardinal-Function st ( for x being set holds
( x in dom b1 iff ( x in M &amp; x is Cardinal ) ) ) &amp; ( for K being Cardinal st K in M holds
b1 . K = exp (K,N) ) &amp; ( for x being set holds
( x in dom b2 iff ( x in M &amp; x is Cardinal ) ) ) &amp; ( for K being Cardinal st K in M holds
b2 . K = exp (K,N) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines cf CARD_5:def_1_:_
 for M, b2 being Cardinal holds
( b2 = cf M iff ( M is_cofinal_with b2 &amp; ( 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 &amp; x is Cardinal ) ) ) &amp; ( 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 &amp; a <> 1 &amp; a <> 2 &amp; a <> card n &amp; card n in a &amp; omega c= a )
proofend;

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

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 &amp; M +` a = M &amp; a *` M = M &amp; M *` a = M )
proofend;

theorem :: CARD_5:19
for a being Aleph holds
( a +` a = a &amp; 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)
proofend;

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
proofend;
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
proofend;
cluster exp (a,b) ->  infinite ;
coherence
 not exp (a,b) is finite
proofend;
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
proofend;
end;

theorem Th22: :: CARD_5:22
cf omega = omega
proofend;

Lm4:  1 = card 1
by CARD_1:def_2;

theorem Th23: :: CARD_5:23
for a being Aleph holds cf (nextcard a) = nextcard a
proofend;

theorem Th24: :: CARD_5:24
for a being Aleph holds omega c= cf a
proofend;

theorem :: CARD_5:25
for n being Element of NAT holds
( cf 0 = 0 &amp; cf (card (n + 1)) = 1 )
proofend;

theorem Th26: :: CARD_5:26
for X being set
for M being Cardinal st X c= M &amp; card X in cf M holds
( sup X in M &amp; union X in M )
proofend;

theorem Th27: :: CARD_5:27
for M, N being Cardinal
for phi being Ordinal-Sequence st dom phi = M &amp; rng phi c= N &amp; M in cf N holds
( sup phi in N &amp; Union phi in N )
proofend;

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

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 &amp; rng xi c= a &amp; xi is increasing &amp; a = sup xi &amp; xi is Cardinal-Function &amp; not 0 in rng xi )
proofend;

theorem :: CARD_5:30
for a being Aleph holds
( omega is regular &amp; nextcard a is regular )
proofend;

begin

theorem Th31: :: CARD_5:31
for a, b being Aleph st a c= b holds
exp (a,b) = exp (2,b)
proofend;

theorem :: CARD_5:32
for a, b being Aleph holds exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)
proofend;

theorem Th33: :: CARD_5:33
for b, a being Aleph holds Sum (b -powerfunc_of a) c= exp (a,b)
proofend;

theorem :: CARD_5:34
for a, b being Aleph st a is limit_cardinal &amp; b in cf a holds
exp (a,b) = Sum (b -powerfunc_of a)
proofend;

theorem :: CARD_5:35
for a, b being Aleph st cf a c= b &amp; b in a holds
exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a))
proofend;

Lm5:  for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
proofend;

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

theorem Th37: :: CARD_5:37
for x being set
for O being Ordinal st {x} c= O holds
order_type_of (RelIncl {x}) = 1
proofend;

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

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
proofend;
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
proofend;
end;

theorem :: CARD_5:39
for F being Subset of omega holds card F c= order_type_of (RelIncl F)
proofend;