:: CARD_5 semantic presentation

Lemma1: ( 0 = Card 0 & 1 = Card 1 & 2 = Card 2 )
by CARD_1:def 5;

theorem Th1: :: CARD_5:1

( 1 = {0} & 2 = {0,1} )

proof end;

theorem Th2: :: CARD_5:2

canceled;

theorem Th3: :: CARD_5:3

canceled;

theorem Th4: :: CARD_5:4

canceled;

theorem Th5: :: CARD_5:5

canceled;

theorem Th6: :: CARD_5:6

canceled;

theorem Th7: :: CARD_5:7

canceled;

theorem Th8: :: CARD_5:8

for b₁ being Nat holds Seg b₁ = (b₁ + 1) \ {0}

proof end;

theorem Th9: :: CARD_5:9

for b₁ being set holds nextcard (Card b₁) = nextcard b₁

proof end;

theorem Th10: :: CARD_5:10

for b₁ being set
for b₂ being Function holds
( b₁ in Union b₂ iff ex b₃ being set st
( b₃ in dom b₂ & b₁ in b₂ . b₃ ) )

proof end;

theorem Th11: :: CARD_5:11

for b₁ being Ordinal holds not alef b₁ is finite

proof end;

theorem Th12: :: CARD_5:12

for b₁ being Cardinal st not b₁ is finite holds
ex b₂ being Ordinal st b₁ = alef b₂

proof end;

theorem Th13: :: CARD_5:13

for b₁ being Cardinal holds
( ex b₂ being Nat st b₁ = Card b₂ or ex b₂ being Ordinal st b₁ = alef b₂ )

proof end;

registration

let c₁ be Ordinal-Sequence;
cluster Union a₁ -> ordinal ;
coherence

proof end;

end;

theorem Th14: :: CARD_5:14

for b₁ being Ordinal
for b₂ being set st b₂ c= b₁ holds
ex b₃ being Ordinal-Sequence st
( b₃ = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl b₂))),(RelIncl b₂) & b₃ is increasing & dom b₃ = order_type_of (RelIncl b₂) & rng b₃ = b₂ )

proof end;

theorem Th15: :: CARD_5:15

for b₁ being Ordinal
for b₂ being set st b₂ c= b₁ holds
sup b₂ is_cofinal_with order_type_of (RelIncl b₂)

proof end;

theorem Th16: :: CARD_5:16

for b₁ being Ordinal
for b₂ being set st b₂ c= b₁ holds
Card b₂ = Card (order_type_of (RelIncl b₂))

proof end;

theorem Th17: :: CARD_5:17

for b₁ being Ordinal ex b₂ being Ordinal st
( b₂ c= Card b₁ & b₁ is_cofinal_with b₂ )

proof end;

theorem Th18: :: CARD_5:18

for b₁ being Ordinal ex b₂ being Cardinal st
( b₂ <=` Card b₁ & b₁ is_cofinal_with b₂ & ( for b₃ being Ordinal st b₁ is_cofinal_with b₃ holds
b₂ c= b₃ ) )

proof end;

Lemma11: for b₁, b₂ being Ordinal-Sequence st rng b₁ = rng b₂ & b₁ is increasing & b₂ is increasing holds
for b₃ being Ordinal st b₃ in dom b₁ holds
( b₃ in dom b₂ & b₁ . b₃ = b₂ . b₃ )

proof end;

theorem Th19: :: CARD_5:19

for b₁, b₂ being Ordinal-Sequence st rng b₁ = rng b₂ & b₁ is increasing & b₂ is increasing holds
b₁ = b₂

proof end;

theorem Th20: :: CARD_5:20

for b₁ being Ordinal-Sequence st b₁ is increasing holds
b₁ is one-to-one

proof end;

theorem Th21: :: CARD_5:21

for b₁, b₂ being Ordinal-Sequence holds (b₁ ^ b₂) | (dom b₁) = b₁

proof end;

theorem Th22: :: CARD_5:22

for b₁ being set
for b₂ being Cardinal st b₁ <> {} holds
Card { b₃ where B is Subset of b₁ : Card b₃ <` b₂ } <=` b₂ *` (exp (Card b₁),b₂)

proof end;

theorem Th23: :: CARD_5:23

for b₁ being Cardinal holds b₁ <` exp 2,b₁

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 c₁ be Cardinal;
canceled;
func cf c₁ -> Cardinal means :Def2: :: CARD_5:def 2
( a₁ is_cofinal_with a₂ & ( for b₁ being Cardinal st a₁ is_cofinal_with b₁ holds
a₂ <=` b₁ ) );
existence

proof end;

uniqueness

proof end;

let c₂ be Cardinal;
func c₂ -powerfunc_of c₁ -> Cardinal-Function means :Def3: :: CARD_5:def 3
( ( for b₁ being set holds
( b₁ in dom a₃ iff ( b₁ in a₁ & b₁ is Cardinal ) ) ) & ( for b₁ being Cardinal st b₁ in a₁ holds
a₃ . b₁ = exp b₁,a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 CARD_5:def 1 :

:: deftheorem Def2 defines cf CARD_5:def 2 :

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

registration

let c₁ be Ordinal;
cluster alef a₁ -> non empty infinite ;
coherence by Th11;

end;

theorem Th24: :: CARD_5:24

for b₁ being Aleph ex b₂ being Ordinal st b₁ = alef b₂ by Th12;

theorem Th25: :: CARD_5:25

for b₁ being Nat
for b₂ being Aleph holds
( b₂ <> 0 & b₂ <> 1 & b₂ <> 2 & b₂ <> Card b₁ & Card b₁ <` b₂ & alef 0 <=` b₂ )

proof end;

theorem Th26: :: CARD_5:26

for b₁ being Cardinal
for b₂ being Aleph st ( b₂ <=` b₁ or b₂ <` b₁ ) holds
b₁ is Aleph

proof end;

theorem Th27: :: CARD_5:27

for b₁ being Cardinal
for b₂ being Aleph st ( b₂ <=` b₁ or b₂ <` b₁ ) holds
( b₂ +` b₁ = b₁ & b₁ +` b₂ = b₁ & b₂ *` b₁ = b₁ & b₁ *` b₂ = b₁ )

proof end;

theorem Th28: :: CARD_5:28

for b₁ being Aleph holds
( b₁ +` b₁ = b₁ & b₁ *` b₁ = b₁ ) by CARD_4:33, CARD_4:77;

theorem Th29: :: CARD_5:29

canceled;

theorem Th30: :: CARD_5:30

canceled;

theorem Th31: :: CARD_5:31

for b₁ being Cardinal
for b₂ being Aleph holds b₁ <=` exp b₁,b₂

proof end;

theorem Th32: :: CARD_5:32

for b₁ being Aleph holds union b₁ = b₁

proof end;

registration

let c₁ be Aleph;
let c₂ be Cardinal;
cluster a₁ +` a₂ -> non empty infinite ;
coherence

proof end;

end;

registration

let c₁ be Cardinal;
let c₂ be Aleph;
cluster a₁ +` a₂ -> non empty infinite ;
coherence ;

end;

registration

let c₁, c₂ be Aleph;
cluster a₁ *` a₂ -> non empty infinite ;
coherence

proof end;

cluster exp a₁,a₂ -> non empty infinite ;
coherence

proof end;

end;

definition

let c₁ be Aleph;
attr a₁ is regular means :: CARD_5:def 4
cf a₁ = a₁;

end;

:: deftheorem Def4 defines regular CARD_5:def 4 :

notation

let c₁ be Aleph;
antonym irregular c₁ for regular c₁;

end;

registration

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

proof end;

cluster -> ordinal Element of a₁;
coherence ;

end;

theorem Th33: :: CARD_5:33

canceled;

theorem Th34: :: CARD_5:34

cf (alef 0) = alef 0

proof end;

theorem Th35: :: CARD_5:35

for b₁ being Aleph holds cf (nextcard b₁) = nextcard b₁

proof end;

theorem Th36: :: CARD_5:36

for b₁ being Aleph holds alef 0 <=` cf b₁

proof end;

theorem Th37: :: CARD_5:37

for b₁ being Nat holds
( cf 0 = 0 & cf (Card (b₁ + 1)) = 1 )

proof end;

theorem Th38: :: CARD_5:38

for b₁ being set
for b₂ being Cardinal st b₁ c= b₂ & Card b₁ <` cf b₂ holds
( sup b₁ in b₂ & union b₁ in b₂ )

proof end;

theorem Th39: :: CARD_5:39

for b₁, b₂ being Cardinal
for b₃ being Ordinal-Sequence st dom b₃ = b₁ & rng b₃ c= b₂ & b₁ <` cf b₂ holds
( sup b₃ in b₂ & Union b₃ in b₂ )

proof end;

registration

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

proof end;

end;

theorem Th40: :: CARD_5:40

for b₁ being Aleph st cf b₁ <` b₁ holds
b₁ is_limit_cardinal

proof end;

theorem Th41: :: CARD_5:41

for b₁ being Aleph st cf b₁ <` b₁ holds
ex b₂ being Ordinal-Sequence st
( dom b₂ = cf b₁ & rng b₂ c= b₁ & b₂ is increasing & b₁ = sup b₂ & b₂ is Cardinal-Function & not 0 in rng b₂ )

proof end;

theorem Th42: :: CARD_5:42

for b₁ being Aleph holds
( alef 0 is regular & nextcard b₁ is regular )

proof end;

theorem Th43: :: CARD_5:43

for b₁, b₂ being Aleph st b₁ <=` b₂ holds
exp b₁,b₂ = exp 2,b₂

proof end;

theorem Th44: :: CARD_5:44

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

proof end;

theorem Th45: :: CARD_5:45

for b₁, b₂ being Aleph holds Sum (b₁ -powerfunc_of b₂) <=` exp b₂,b₁

proof end;

theorem Th46: :: CARD_5:46

for b₁, b₂ being Aleph st b₁ is_limit_cardinal & b₂ <` cf b₁ holds
exp b₁,b₂ = Sum (b₂ -powerfunc_of b₁)

proof end;

theorem Th47: :: CARD_5:47

for b₁, b₂ being Aleph st cf b₁ <=` b₂ & b₂ <` b₁ holds
exp b₁,b₂ = exp (Sum (b₂ -powerfunc_of b₁)),(cf b₁)

proof end;