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

begin

Lm1: 1 = card 1
by CARD_1:def 5;

Lm2: 2 = card 2
by CARD_1:def 5;

theorem :: CARD_5:1

canceled;

theorem :: CARD_5:2

canceled;

theorem :: CARD_5:3

canceled;

theorem :: CARD_5:4

canceled;

theorem :: CARD_5:5

canceled;

theorem :: CARD_5:6

canceled;

theorem :: CARD_5:7

canceled;

theorem :: CARD_5:8

canceled;

begin

theorem Th9: :: CARD_5:9

for X being set holds nextcard (card X) = nextcard X

proof end;

theorem Th10: :: CARD_5:10

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

theorem Th11: :: CARD_5:11

for A being Ordinal holds not alef A is finite

proof end;

theorem Th12: :: CARD_5:12

for M being Cardinal st not M is finite holds
ex A being Ordinal st M = alef A

proof end;

registration

let phi be Ordinal-Sequence;
cluster Union phi -> ordinal ;
coherence
Union phi is ordinal

proof end;

end;

theorem :: CARD_5:13

canceled;

theorem Th14: :: CARD_5:14

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

theorem Th15: :: CARD_5:15

for A being Ordinal
for X being set st X c= A holds
sup X is_cofinal_with order_type_of (RelIncl X)

proof end;

theorem Th16: :: CARD_5:16

for A being Ordinal
for X being set st X c= A holds
card X = card (order_type_of (RelIncl X))

proof end;

theorem Th17: :: CARD_5:17

for A being Ordinal ex B being Ordinal st
( B c= card A & A is_cofinal_with B )

proof end;

theorem Th18: :: CARD_5:18

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

for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
phi = psi

proof end;

theorem Th20: :: CARD_5:20

for phi being Ordinal-Sequence st phi is increasing holds
phi is one-to-one

proof end;

theorem Th21: :: CARD_5:21

for phi, psi being Ordinal-Sequence holds (phi ^ psi) | (dom phi) = phi

proof end;

theorem :: CARD_5:22

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 Th23: :: CARD_5:23

for M being Cardinal holds M in exp (2,M)

proof end;

registration

cluster epsilon-transitive epsilon-connected ordinal infinite cardinal set ;
existence
not for b₁ being Cardinal holds b₁ is finite

proof end;

end;

registration

cluster infinite -> non empty set ;
coherence
for b₁ being set st not b₁ is finite holds
not b₁ is empty ;

end;

definition

mode Aleph is infinite Cardinal;
let M be Cardinal;
canceled;
func cf M -> Cardinal means :Def2: :: CARD_5:def 2
( M is_cofinal_with it & ( for N being Cardinal st M is_cofinal_with N holds
it c= N ) );
existence
ex b₁ being Cardinal st
( M is_cofinal_with b₁ & ( for N being Cardinal st M is_cofinal_with N holds
b₁ c= N ) )

proof end;

uniqueness
for b₁, b₂ being Cardinal st M is_cofinal_with b₁ & ( for N being Cardinal st M is_cofinal_with N holds
b₁ c= N ) & M is_cofinal_with b₂ & ( for N being Cardinal st M is_cofinal_with N holds
b₂ c= N ) holds
b₁ = b₂

proof end;

let N be Cardinal;
func N -powerfunc_of M -> Cardinal-Function means :Def3: :: CARD_5:def 3
( ( 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 b₁ being Cardinal-Function st
( ( for x being set holds
( x in dom b₁ iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b₁ . K = exp (K,N) ) )

proof end;

uniqueness
for b₁, b₂ being Cardinal-Function st ( for x being set holds
( x in dom b₁ iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b₁ . K = exp (K,N) ) & ( for x being set holds
( x in dom b₂ iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b₂ . K = exp (K,N) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem CARD_5:def 1 :
canceled;

:: deftheorem Def2 defines cf CARD_5:def 2 :
for M, b₂ being Cardinal holds
( b₂ = cf M iff ( M is_cofinal_with b₂ & ( for N being Cardinal st M is_cofinal_with N holds
b₂ c= N ) ) );

:: deftheorem Def3 defines -powerfunc_of CARD_5:def 3 :
for M, N being Cardinal
for b₃ being Cardinal-Function holds
( b₃ = N -powerfunc_of M iff ( ( for x being set holds
( x in dom b₃ iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b₃ . K = exp (K,N) ) ) );

registration

let A be Ordinal;
cluster alef A -> infinite ;
coherence
not alef A is finite by Th11;

end;

begin

theorem :: CARD_5:24

for a being Aleph ex A being Ordinal st a = alef A by Th12;

theorem Th25: :: CARD_5:25

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

theorem Th26: :: CARD_5:26

for M being Cardinal
for a being Aleph st ( a c= M or a in M ) holds
M is Aleph

proof end;

theorem Th27: :: CARD_5:27

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

for a being Aleph holds
( a +` a = a & a *` a = a ) by CARD_3:117, CARD_4:77;

theorem :: CARD_5:29

canceled;

theorem :: CARD_5:30

canceled;

theorem Th31: :: CARD_5:31

for M being Cardinal
for a being Aleph holds M c= exp (M,a)

proof end;

theorem :: CARD_5:32

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;

begin

definition

let IT be Aleph;
attr IT is regular means :: CARD_5:def 4
cf IT = IT;

end;

:: deftheorem defines regular CARD_5:def 4 :
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 end;

end;

theorem :: CARD_5:33

canceled;

theorem Th34: :: CARD_5:34

cf omega = omega

proof end;

Lm4: 1 = card 1
by CARD_1:def 5;

theorem Th35: :: CARD_5:35

for a being Aleph holds cf (nextcard a) = nextcard a

proof end;

theorem Th36: :: CARD_5:36

for a being Aleph holds omega c= cf a

proof end;

theorem :: CARD_5:37

for n being Element of NAT holds
( cf 0 = 0 & cf (card (n + 1)) = 1 )

proof end;

theorem Th38: :: CARD_5:38

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 Th39: :: CARD_5:39

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;
cluster cf a -> infinite ;
coherence
not cf a is finite by Th26, Th36;

end;

theorem Th40: :: CARD_5:40

for a being Aleph st cf a in a holds
a is limit_cardinal

proof end;

theorem Th41: :: CARD_5:41

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

for a being Aleph holds
( omega is regular & nextcard a is regular )

proof end;

begin

theorem Th43: :: CARD_5:43

for a, b being Aleph st a c= b holds
exp (a,b) = exp (2,b)

proof end;

theorem :: CARD_5:44

for a, b being Aleph holds exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)

proof end;

theorem Th45: :: CARD_5:45

for b, a being Aleph holds Sum (b -powerfunc_of a) c= exp (a,b)

proof end;

theorem :: CARD_5:46

for a, b being Aleph st a is limit_cardinal & b in cf a holds
exp (a,b) = Sum (b -powerfunc_of a)

proof end;

theorem :: CARD_5:47

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

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

proof end;

theorem Th48: :: CARD_5:48

for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) = card X

proof end;

theorem Th49: :: CARD_5:49

for x being set
for O being Ordinal st {x} c= O holds
order_type_of (RelIncl {x}) = 1

proof end;

theorem :: CARD_5:50

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

end;

theorem :: CARD_5:51

for F being Subset of omega holds card F c= order_type_of (RelIncl F)

proof end;