:: On Powers of Cardinals
:: by Grzegorz Bancerek
::
:: Copyright (c) 1992-2021 Association of Mizar Users

Lm1: 1 = card 1
;

Lm2: 2 = card 2
;

theorem Th1: :: CARD_5:1
for X being set holds nextcard (card X) = nextcard X
proof end;

theorem Th2: :: CARD_5:2
for y being object
for f being Function holds
( y in Union f iff ex x being object st
( x in dom f & y in f . x ) )
proof end;

theorem Th3: :: CARD_5:3
for A being Ordinal holds aleph A is infinite
proof end;

theorem :: CARD_5:4
for M being Cardinal st M is infinite holds
ex A being Ordinal st M = aleph A
proof end;

registration
let phi be Ordinal-Sequence;
cluster Union phi -> ordinal ;
coherence
Union phi is ordinal
proof 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 ()),()) & phi is increasing & dom phi = order_type_of () & rng phi = X )
proof 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 ()
proof end;

theorem Th7: :: CARD_5:7
for A being Ordinal
for X being set st X c= A holds
card X = card ()
proof 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 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 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 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 end;

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

theorem Th12: :: CARD_5:12
for phi, psi being Ordinal-Sequence holds (phi ^ psi) | (dom phi) = phi
proof 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 end;

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

registration
existence
ex b1 being Cardinal st b1 is infinite
proof 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 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
;
let N be Cardinal;
func N -powerfunc_of M -> Cardinal-Function means :Def2: :: CARD_5:def 2
( ( for x being object 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 object 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 end;
uniqueness
for b1, b2 being Cardinal-Function st ( for x being object 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 object 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 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 object 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;
coherence
not aleph A is finite
by Th3;
end;

theorem :: CARD_5:15
canceled;

::\$CT
theorem Th15: :: CARD_5:16
for n being Nat
for a being Aleph holds
( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )
proof end;

theorem Th16: :: CARD_5:17
for M being Cardinal
for a being Aleph st ( a c= M or a in M ) holds
M is Aleph
proof end;

theorem Th17: :: 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 end;

theorem :: CARD_5:19
for a being Aleph holds
( a + a = a & a * a = a ) by ;

theorem Th19: :: CARD_5:20
for M being Cardinal
for a being Aleph holds M c= exp (M,a)
proof 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;
cluster a + M -> infinite ;
coherence
not a + M is finite
proof end;
end;

registration
let M be Cardinal;
let a be Aleph;
cluster M + a -> infinite ;
coherence
not M + a is finite
;
end;

registration
let a, b be Aleph;
cluster a * b -> infinite ;
coherence
not a * b is finite
proof end;
cluster exp (a,b) -> infinite ;
coherence
not exp (a,b) is finite
proof end;
end;

definition
let IT be Aleph;
attr IT 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;
coherence
not nextcard a is finite
proof end;
end;

theorem Th21: :: CARD_5:22
proof end;

theorem Th22: :: CARD_5:23
for a being Aleph holds cf () = nextcard a
proof end;

theorem Th23: :: CARD_5:24
for a being Aleph holds omega c= cf a
proof end;

theorem :: CARD_5:25
for n being Nat holds
( cf 0 = 0 & cf (card (n + 1)) = 1 )
proof end;

theorem Th25: :: 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 end;

theorem Th26: :: 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 end;

registration
let a be Aleph;
coherence
not cf a is finite
by ;
end;

theorem Th27: :: CARD_5:28
for a being Aleph st cf a in a holds
a is limit_cardinal
proof end;

theorem Th28: :: 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 end;

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

theorem Th30: :: CARD_5:31
for a, b being Aleph st a c= b holds
exp (a,b) = exp (2,b)
proof end;

theorem :: CARD_5:32
for a, b being Aleph holds exp ((),b) = (exp (a,b)) * ()
proof end;

theorem Th32: :: CARD_5:33
for a, b being Aleph holds Sum () c= exp (a,b)
proof end;

theorem :: CARD_5:34
for a, b being Aleph st a is limit_cardinal & b in cf a holds
exp (a,b) = Sum ()
proof end;

theorem :: CARD_5:35
for a, b being Aleph st cf a c= b & b in a holds
exp (a,b) = exp ((Sum ()),(cf a))
proof end;

Lm4: for O being Ordinal
for X being finite set st X c= O holds
order_type_of () is finite

proof end;

theorem Th35: :: CARD_5:36
for O being Ordinal
for X being finite set st X c= O holds
order_type_of () = card X
proof end;

theorem Th36: :: CARD_5:37
for x being object
for O being Ordinal st {x} c= O holds
order_type_of () = 1
proof end;

theorem :: CARD_5:38
for x being object
for O being Ordinal st {x} c= O holds
canonical_isomorphism_of ((),()) = 0 .--> x
proof end;

registration
let O be Ordinal;
let X be Subset of O;
let n be set ;
cluster (canonical_isomorphism_of ((RelIncl ()),())) . n -> ordinal ;
coherence
(canonical_isomorphism_of ((RelIncl ()),())) . n is ordinal
proof end;
end;

registration
let X be natural-membered set ;
let n be set ;
cluster (canonical_isomorphism_of ((RelIncl ()),())) . n -> natural ;
coherence
(canonical_isomorphism_of ((RelIncl ()),())) . n is natural
proof end;
end;

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