Lm2: 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 Th19: :: 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 <` M } <=` M *` (exp (Card X),M)

proof end;

theorem Th23: :: CARD_5:23

for M being Cardinal holds M <` exp 2,M

proof end;

registration

cluster infinite set ;
existence

proof end;

cluster infinite set ;
existence

proof end;

end;

registration

cluster infinite -> non empty set ;
coherence ;

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 <=` N ) );
existence

proof end;

uniqueness

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

proof end;

uniqueness

proof end;

end;

:: deftheorem CARD_5:def 1 :

:: deftheorem Def2 defines cf CARD_5:def 2 :

:: deftheorem Def3 defines -powerfunc_of CARD_5:def 3 :

registration

let A be Ordinal;
cluster alef A -> non empty infinite ;
coherence by Th11;

end;

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 Nat
for a being Aleph holds
( a <> 0 & a <> 1 & a <> 2 & a <> Card n & Card n <` a & alef 0 <=` a )

proof end;

theorem Th26: :: CARD_5:26

for M being Cardinal
for a being Aleph st ( a <=` M or a <` M ) holds
M is Aleph

proof end;

theorem Th27: :: CARD_5:27

for M being Cardinal
for a being Aleph st ( a <=` M or a <` 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_4:33, 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 <=` exp M,a

proof end;

theorem Th32: :: CARD_5:32

for a being Aleph holds union a = a

proof end;

registration

let a be Aleph;
let M be Cardinal;
cluster a +` M -> non empty infinite ;
coherence

proof end;

end;

registration

let M be Cardinal;
let a be Aleph;
cluster M +` a -> non empty infinite ;
coherence ;

end;

registration

let a, b be Aleph;
cluster a *` b -> non empty infinite ;
coherence

proof end;

cluster exp a,b -> non empty infinite ;
coherence

proof end;

end;

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 :

notation

let IT be Aleph;
antonym irregular IT for regular IT;

end;

registration

let a be Aleph;
cluster nextcard a -> non empty infinite ;
coherence

proof end;

cluster -> ordinal Element of a;
coherence ;

end;

theorem :: CARD_5:33

canceled;

theorem Th34: :: CARD_5:34

cf (alef 0) = alef 0

proof end;

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 alef 0 <=` cf a

proof end;

theorem :: CARD_5:37

for n being 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 <` 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 <` cf N holds
( sup phi in N & Union phi in N )

proof end;

registration

let a be Aleph;
cluster cf a -> non empty infinite ;
coherence

proof end;

end;

theorem Th40: :: CARD_5:40

for a being Aleph st cf a <` a holds
a is_limit_cardinal

proof end;

theorem Th41: :: CARD_5:41

for a being Aleph st cf a <` 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
( alef 0 is regular & nextcard a is regular )

proof end;

theorem Th43: :: CARD_5:43

for a, b being Aleph st a <=` 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) <=` exp a,b

proof end;

theorem :: CARD_5:46

for a, b being Aleph st a is_limit_cardinal & b <` 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 <=` b & b <` a holds
exp a,b = exp (Sum (b -powerfunc_of a)),(cf a)

proof end;