:: 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 b1 being Nat holds Seg b1 = (b1 + 1) \ {0}
proof end;

theorem Th9: :: CARD_5:9
for b1 being set holds nextcard (Card b1) = nextcard b1
proof end;

theorem Th10: :: CARD_5:10
for b1 being set
for b2 being Function holds
( b1 in Union b2 iff ex b3 being set st
( b3 in dom b2 & b1 in b2 . b3 ) )
proof end;

theorem Th11: :: CARD_5:11
for b1 being Ordinal holds not alef b1 is finite
proof end;

theorem Th12: :: CARD_5:12
for b1 being Cardinal st not b1 is finite holds
ex b2 being Ordinal st b1 = alef b2
proof end;

theorem Th13: :: CARD_5:13
for b1 being Cardinal holds
( ex b2 being Nat st b1 = Card b2 or ex b2 being Ordinal st b1 = alef b2 )
proof end;

registration
let c1 be Ordinal-Sequence;
cluster Union a1 -> ordinal ;
coherence
Union c1 is ordinal
proof end;
end;

theorem Th14: :: CARD_5:14
for b1 being Ordinal
for b2 being set st b2 c= b1 holds
ex b3 being Ordinal-Sequence st
( b3 = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl b2))),(RelIncl b2) & b3 is increasing & dom b3 = order_type_of (RelIncl b2) & rng b3 = b2 )
proof end;

theorem Th15: :: CARD_5:15
for b1 being Ordinal
for b2 being set st b2 c= b1 holds
sup b2 is_cofinal_with order_type_of (RelIncl b2)
proof end;

theorem Th16: :: CARD_5:16
for b1 being Ordinal
for b2 being set st b2 c= b1 holds
Card b2 = Card (order_type_of (RelIncl b2))
proof end;

theorem Th17: :: CARD_5:17
for b1 being Ordinal ex b2 being Ordinal st
( b2 c= Card b1 & b1 is_cofinal_with b2 )
proof end;

theorem Th18: :: CARD_5:18
for b1 being Ordinal ex b2 being Cardinal st
( b2 <=` Card b1 & b1 is_cofinal_with b2 & ( for b3 being Ordinal st b1 is_cofinal_with b3 holds
b2 c= b3 ) )
proof end;

Lemma11: for b1, b2 being Ordinal-Sequence st rng b1 = rng b2 & b1 is increasing & b2 is increasing holds
for b3 being Ordinal st b3 in dom b1 holds
( b3 in dom b2 & b1 . b3 = b2 . b3 )
proof end;

theorem Th19: :: CARD_5:19
for b1, b2 being Ordinal-Sequence st rng b1 = rng b2 & b1 is increasing & b2 is increasing holds
b1 = b2
proof end;

theorem Th20: :: CARD_5:20
for b1 being Ordinal-Sequence st b1 is increasing holds
b1 is one-to-one
proof end;

theorem Th21: :: CARD_5:21
for b1, b2 being Ordinal-Sequence holds (b1 ^ b2) | (dom b1) = b1
proof end;

theorem Th22: :: CARD_5:22
for b1 being set
for b2 being Cardinal st b1 <> {} holds
Card { b3 where B is Subset of b1 : Card b3 <` b2 } <=` b2 *` (exp (Card b1),b2)
proof end;

theorem Th23: :: CARD_5:23
for b1 being Cardinal holds b1 <` exp 2,b1
proof end;

registration
cluster infinite set ;
existence
not for b1 being set holds b1 is finite
proof end;
cluster infinite set ;
existence
not for b1 being Cardinal holds b1 is finite
proof end;
end;

registration
cluster infinite -> non empty set ;
coherence
for b1 being set st not b1 is finite holds
not b1 is empty
;
end;

definition
mode Aleph is infinite Cardinal;
let c1 be Cardinal;
canceled;
func cf c1 -> Cardinal means :Def2: :: CARD_5:def 2
( a1 is_cofinal_with a2 & ( for b1 being Cardinal st a1 is_cofinal_with b1 holds
a2 <=` b1 ) );
existence
ex b1 being Cardinal st
( c1 is_cofinal_with b1 & ( for b2 being Cardinal st c1 is_cofinal_with b2 holds
b1 <=` b2 ) )
proof end;
uniqueness
for b1, b2 being Cardinal st c1 is_cofinal_with b1 & ( for b3 being Cardinal st c1 is_cofinal_with b3 holds
b1 <=` b3 ) & c1 is_cofinal_with b2 & ( for b3 being Cardinal st c1 is_cofinal_with b3 holds
b2 <=` b3 ) holds
b1 = b2
proof end;
let c2 be Cardinal;
func c2 -powerfunc_of c1 -> Cardinal-Function means :Def3: :: CARD_5:def 3
( ( for b1 being set holds
( b1 in dom a3 iff ( b1 in a1 & b1 is Cardinal ) ) ) & ( for b1 being Cardinal st b1 in a1 holds
a3 . b1 = exp b1,a2 ) );
existence
ex b1 being Cardinal-Function st
( ( for b2 being set holds
( b2 in dom b1 iff ( b2 in c1 & b2 is Cardinal ) ) ) & ( for b2 being Cardinal st b2 in c1 holds
b1 . b2 = exp b2,c2 ) )
proof end;
uniqueness
for b1, b2 being Cardinal-Function st ( for b3 being set holds
( b3 in dom b1 iff ( b3 in c1 & b3 is Cardinal ) ) ) & ( for b3 being Cardinal st b3 in c1 holds
b1 . b3 = exp b3,c2 ) & ( for b3 being set holds
( b3 in dom b2 iff ( b3 in c1 & b3 is Cardinal ) ) ) & ( for b3 being Cardinal st b3 in c1 holds
b2 . b3 = exp b3,c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 CARD_5:def 1 :
canceled;

:: deftheorem Def2 defines cf CARD_5:def 2 :
for b1, b2 being Cardinal holds
( b2 = cf b1 iff ( b1 is_cofinal_with b2 & ( for b3 being Cardinal st b1 is_cofinal_with b3 holds
b2 <=` b3 ) ) );

:: deftheorem Def3 defines -powerfunc_of CARD_5:def 3 :
for b1, b2 being Cardinal
for b3 being Cardinal-Function holds
( b3 = b2 -powerfunc_of b1 iff ( ( for b4 being set holds
( b4 in dom b3 iff ( b4 in b1 & b4 is Cardinal ) ) ) & ( for b4 being Cardinal st b4 in b1 holds
b3 . b4 = exp b4,b2 ) ) );

registration
let c1 be Ordinal;
cluster alef a1 -> non empty infinite ;
coherence
not alef c1 is finite
by Th11;
end;

theorem Th24: :: CARD_5:24
for b1 being Aleph ex b2 being Ordinal st b1 = alef b2 by Th12;

theorem Th25: :: CARD_5:25
for b1 being Nat
for b2 being Aleph holds
( b2 <> 0 & b2 <> 1 & b2 <> 2 & b2 <> Card b1 & Card b1 <` b2 & alef 0 <=` b2 )
proof end;

theorem Th26: :: CARD_5:26
for b1 being Cardinal
for b2 being Aleph st ( b2 <=` b1 or b2 <` b1 ) holds
b1 is Aleph
proof end;

theorem Th27: :: CARD_5:27
for b1 being Cardinal
for b2 being Aleph st ( b2 <=` b1 or b2 <` b1 ) holds
( b2 +` b1 = b1 & b1 +` b2 = b1 & b2 *` b1 = b1 & b1 *` b2 = b1 )
proof end;

theorem Th28: :: CARD_5:28
for b1 being Aleph holds
( b1 +` b1 = b1 & b1 *` b1 = b1 ) 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 b1 being Cardinal
for b2 being Aleph holds b1 <=` exp b1,b2
proof end;

theorem Th32: :: CARD_5:32
for b1 being Aleph holds union b1 = b1
proof end;

registration
let c1 be Aleph;
let c2 be Cardinal;
cluster a1 +` a2 -> non empty infinite ;
coherence
not c1 +` c2 is finite
proof end;
end;

registration
let c1 be Cardinal;
let c2 be Aleph;
cluster a1 +` a2 -> non empty infinite ;
coherence
not c1 +` c2 is finite
;
end;

registration
let c1, c2 be Aleph;
cluster a1 *` a2 -> non empty infinite ;
coherence
not c1 *` c2 is finite
proof end;
cluster exp a1,a2 -> non empty infinite ;
coherence
not exp c1,c2 is finite
proof end;
end;

definition
let c1 be Aleph;
attr a1 is regular means :: CARD_5:def 4
cf a1 = a1;
end;

:: deftheorem Def4 defines regular CARD_5:def 4 :
for b1 being Aleph holds
( b1 is regular iff cf b1 = b1 );

notation
let c1 be Aleph;
antonym irregular c1 for regular c1;
end;

registration
let c1 be Aleph;
cluster nextcard a1 -> non empty infinite ;
coherence
not nextcard c1 is finite
proof end;
cluster -> ordinal Element of a1;
coherence
for b1 being Element of c1 holds b1 is ordinal
;
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 b1 being Aleph holds cf (nextcard b1) = nextcard b1
proof end;

theorem Th36: :: CARD_5:36
for b1 being Aleph holds alef 0 <=` cf b1
proof end;

theorem Th37: :: CARD_5:37
for b1 being Nat holds
( cf 0 = 0 & cf (Card (b1 + 1)) = 1 )
proof end;

theorem Th38: :: CARD_5:38
for b1 being set
for b2 being Cardinal st b1 c= b2 & Card b1 <` cf b2 holds
( sup b1 in b2 & union b1 in b2 )
proof end;

theorem Th39: :: CARD_5:39
for b1, b2 being Cardinal
for b3 being Ordinal-Sequence st dom b3 = b1 & rng b3 c= b2 & b1 <` cf b2 holds
( sup b3 in b2 & Union b3 in b2 )
proof end;

registration
let c1 be Aleph;
cluster cf a1 -> non empty infinite ;
coherence
not cf c1 is finite
proof end;
end;

theorem Th40: :: CARD_5:40
for b1 being Aleph st cf b1 <` b1 holds
b1 is_limit_cardinal
proof end;

theorem Th41: :: CARD_5:41
for b1 being Aleph st cf b1 <` b1 holds
ex b2 being Ordinal-Sequence st
( dom b2 = cf b1 & rng b2 c= b1 & b2 is increasing & b1 = sup b2 & b2 is Cardinal-Function & not 0 in rng b2 )
proof end;

theorem Th42: :: CARD_5:42
for b1 being Aleph holds
( alef 0 is regular & nextcard b1 is regular )
proof end;

theorem Th43: :: CARD_5:43
for b1, b2 being Aleph st b1 <=` b2 holds
exp b1,b2 = exp 2,b2
proof end;

theorem Th44: :: CARD_5:44
for b1, b2 being Aleph holds exp (nextcard b1),b2 = (exp b1,b2) *` (nextcard b1)
proof end;

theorem Th45: :: CARD_5:45
for b1, b2 being Aleph holds Sum (b1 -powerfunc_of b2) <=` exp b2,b1
proof end;

theorem Th46: :: CARD_5:46
for b1, b2 being Aleph st b1 is_limit_cardinal & b2 <` cf b1 holds
exp b1,b2 = Sum (b2 -powerfunc_of b1)
proof end;

theorem Th47: :: CARD_5:47
for b1, b2 being Aleph st cf b1 <=` b2 & b2 <` b1 holds
exp b1,b2 = exp (Sum (b2 -powerfunc_of b1)),(cf b1)
proof end;