:: On Powers of Cardinals
:: by Grzegorz Bancerek
::
:: Received August 24, 1992
:: 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 (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & 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 (RelIncl X)

proof 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 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

cluster epsilon-transitive epsilon-connected ordinal infinite cardinal for set ;

existence
ex b₁ being Cardinal st b₁ is infinite

proof end;

end;

registration

cluster infinite -> non empty for set ;

coherence
for b₁ being set st b₁ is infinite holds
not b₁ 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 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₂ ;
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 b₁ being Cardinal-Function st
( ( for x being object 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 object 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 object 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 Def1 defines cf CARD_5:def 1 :
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 Def2 defines -powerfunc_of CARD_5:def 2 :
for M, N being Cardinal
for b₃ being Cardinal-Function holds
( b₃ = N -powerfunc_of M iff ( ( for x being object 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 aleph A -> infinite ;

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 CARD_2:75, CARD_4:15;

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;

cluster nextcard a -> infinite ;

coherence
not nextcard a is finite

proof end;

end;

theorem Th21: :: CARD_5:22

cf omega = omega

proof end;

theorem Th22: :: CARD_5:23

for a being Aleph holds cf (nextcard a) = 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;

cluster cf a -> infinite ;

coherence
not cf a is finite by Th16, Th23;

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 Th21, Th22;

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 ((nextcard a),b) = (exp (a,b)) *` (nextcard a)

proof end;

theorem Th32: :: CARD_5:33

for a, b being Aleph holds Sum (b -powerfunc_of a) 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 (b -powerfunc_of a)

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 (b -powerfunc_of a)),(cf a))

proof end;

Lm4: for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) 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 (RelIncl X) = 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 (RelIncl {x}) = 1

proof end;

theorem :: CARD_5:38

for x being object
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:39

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

proof end;