:: CARD_4 semantic presentation

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

theorem Th1: :: CARD_4:1
for b1 being set holds
( b1 is finite iff Card b1 is finite )
proof end;

theorem Th2: :: CARD_4:2
for b1 being set holds
( b1 is finite iff Card b1 <` alef 0 )
proof end;

theorem Th3: :: CARD_4:3
for b1 being set st b1 is finite holds
( Card b1 in alef 0 & Card b1 in omega ) by Th2, CARD_1:83;

theorem Th4: :: CARD_4:4
for b1 being set holds
( b1 is finite iff ex b2 being Nat st Card b1 = Card b2 )
proof end;

theorem Th5: :: CARD_4:5
for b1 being Ordinal holds (succ b1) \ {b1} = b1
proof end;

theorem Th6: :: CARD_4:6
for b1 being Nat
for b2 being Ordinal st b2,b1 are_equipotent holds
b2 = b1
proof end;

theorem Th7: :: CARD_4:7
for b1 being Ordinal holds
( b1 is finite iff b1 in omega )
proof end;

theorem Th8: :: CARD_4:8
for b1 being Ordinal holds
( not b1 is finite iff omega c= b1 )
proof end;

theorem Th9: :: CARD_4:9
for b1 being Cardinal holds
( b1 is finite iff b1 in alef 0 ) by Th7, CARD_1:83;

theorem Th10: :: CARD_4:10
canceled;

theorem Th11: :: CARD_4:11
for b1 being Cardinal holds
( not b1 is finite iff alef 0 c= b1 )
proof end;

theorem Th12: :: CARD_4:12
canceled;

theorem Th13: :: CARD_4:13
for b1, b2 being Cardinal st b1 is finite & not b2 is finite holds
( b1 <` b2 & b1 <=` b2 )
proof end;

theorem Th14: :: CARD_4:14
for b1 being set holds
( not b1 is finite iff ex b2 being set st
( b2 c= b1 & Card b2 = alef 0 ) )
proof end;

theorem Th15: :: CARD_4:15
not NAT is finite by Th8;

registration
cluster NAT -> infinite ;
coherence
not omega is finite
by Th15;
end;

theorem Th16: :: CARD_4:16
canceled;

theorem Th17: :: CARD_4:17
for b1 being set holds
( b1 = {} iff Card b1 = 0 ) by CARD_1:47, CARD_2:59;

theorem Th18: :: CARD_4:18
canceled;

theorem Th19: :: CARD_4:19
for b1 being Cardinal holds 0 <=` b1
proof end;

theorem Th20: :: CARD_4:20
for b1, b2 being set holds
( Card b1 = Card b2 iff nextcard b1 = nextcard b2 )
proof end;

theorem Th21: :: CARD_4:21
for b1, b2 being Cardinal holds
( b1 = b2 iff nextcard b2 = nextcard b1 )
proof end;

theorem Th22: :: CARD_4:22
for b1, b2 being Cardinal holds
( b1 <` b2 iff nextcard b1 <=` b2 )
proof end;

theorem Th23: :: CARD_4:23
for b1, b2 being Cardinal holds
( b1 <` nextcard b2 iff b1 <=` b2 )
proof end;

theorem Th24: :: CARD_4:24
for b1 being Cardinal holds
( 0 <` b1 iff 1 <=` b1 )
proof end;

theorem Th25: :: CARD_4:25
for b1 being Cardinal holds
( 1 <` b1 iff 2 <=` b1 )
proof end;

theorem Th26: :: CARD_4:26
for b1, b2 being Cardinal st b1 is finite & ( b2 <=` b1 or b2 <` b1 ) holds
b2 is finite
proof end;

set c1 = succ one ;

theorem Th27: :: CARD_4:27
for b1 being Ordinal holds
( b1 is_limit_ordinal iff for b2 being Ordinal
for b3 being Nat st b2 in b1 holds
b2 +^ b3 in b1 )
proof end;

theorem Th28: :: CARD_4:28
for b1 being Nat
for b2 being Ordinal holds
( b2 +^ (succ b1) = (succ b2) +^ b1 & b2 +^ (b1 + 1) = (succ b2) +^ b1 )
proof end;

theorem Th29: :: CARD_4:29
for b1 being Ordinal ex b2 being Nat st b1 *^ (succ one ) = b1 +^ b2
proof end;

theorem Th30: :: CARD_4:30
for b1 being Ordinal st b1 is_limit_ordinal holds
b1 *^ (succ one ) = b1
proof end;

theorem Th31: :: CARD_4:31
for b1 being Ordinal st omega c= b1 holds
one +^ b1 = b1
proof end;

theorem Th32: :: CARD_4:32
for b1 being Cardinal st not b1 is finite holds
b1 is_limit_ordinal
proof end;

theorem Th33: :: CARD_4:33
for b1 being Cardinal st not b1 is finite holds
b1 +` b1 = b1
proof end;

theorem Th34: :: CARD_4:34
for b1, b2 being Cardinal st not b1 is finite & ( b2 <=` b1 or b2 <` b1 ) holds
( b1 +` b2 = b1 & b2 +` b1 = b1 )
proof end;

theorem Th35: :: CARD_4:35
for b1, b2 being set st not b1 is finite & ( b1,b2 are_equipotent or b2,b1 are_equipotent ) holds
( b1 \/ b2,b1 are_equipotent & Card (b1 \/ b2) = Card b1 )
proof end;

theorem Th36: :: CARD_4:36
for b1, b2 being set st not b1 is finite & b2 is finite holds
( b1 \/ b2,b1 are_equipotent & Card (b1 \/ b2) = Card b1 )
proof end;

theorem Th37: :: CARD_4:37
for b1, b2 being set st not b1 is finite & ( Card b2 <` Card b1 or Card b2 <=` Card b1 ) holds
( b1 \/ b2,b1 are_equipotent & Card (b1 \/ b2) = Card b1 )
proof end;

theorem Th38: :: CARD_4:38
for b1, b2 being finite Cardinal holds b1 +` b2 is finite
proof end;

theorem Th39: :: CARD_4:39
for b1, b2 being Cardinal st not b1 is finite holds
( not b1 +` b2 is finite & not b2 +` b1 is finite )
proof end;

theorem Th40: :: CARD_4:40
for b1, b2 being finite Cardinal holds b1 *` b2 is finite
proof end;

theorem Th41: :: CARD_4:41
for b1, b2, b3, b4 being Cardinal st ( ( b1 <` b2 & b3 <` b4 ) or ( b1 <=` b2 & b3 <` b4 ) or ( b1 <` b2 & b3 <=` b4 ) or ( b1 <=` b2 & b3 <=` b4 ) ) holds
( b1 +` b3 <=` b2 +` b4 & b3 +` b1 <=` b2 +` b4 )
proof end;

theorem Th42: :: CARD_4:42
for b1, b2, b3 being Cardinal st ( b1 <` b2 or b1 <=` b2 ) holds
( b3 +` b1 <=` b3 +` b2 & b3 +` b1 <=` b2 +` b3 & b1 +` b3 <=` b3 +` b2 & b1 +` b3 <=` b2 +` b3 ) by Th41;

definition
let c2 be set ;
attr a1 is countable means :Def1: :: CARD_4:def 1
Card a1 <=` alef 0;
end;

:: deftheorem Def1 defines countable CARD_4:def 1 :
for b1 being set holds
( b1 is countable iff Card b1 <=` alef 0 );

theorem Th43: :: CARD_4:43
for b1 being set st b1 is finite holds
b1 is countable
proof end;

theorem Th44: :: CARD_4:44
( omega is countable & NAT is countable )
proof end;

theorem Th45: :: CARD_4:45
for b1 being set holds
( b1 is countable iff ex b2 being Function st
( dom b2 = NAT & b1 c= rng b2 ) )
proof end;

theorem Th46: :: CARD_4:46
for b1, b2 being set st b1 c= b2 & b2 is countable holds
b1 is countable
proof end;

theorem Th47: :: CARD_4:47
for b1, b2 being set st b1 is countable & b2 is countable holds
b1 \/ b2 is countable
proof end;

theorem Th48: :: CARD_4:48
for b1, b2 being set st b1 is countable holds
( b1 /\ b2 is countable & b2 /\ b1 is countable )
proof end;

theorem Th49: :: CARD_4:49
for b1, b2 being set st b1 is countable holds
b1 \ b2 is countable
proof end;

theorem Th50: :: CARD_4:50
for b1, b2 being set st b1 is countable & b2 is countable holds
b1 \+\ b2 is countable
proof end;

theorem Th51: :: CARD_4:51
for b1 being Nat
for b2 being Real holds
( ( b2 <> 0 or b1 = 0 ) iff b2 |^ b1 <> 0 )
proof end;

definition
let c2, c3 be Nat;
redefine func |^ as c1 |^ c2 -> Nat;
coherence
c2 |^ c3 is Nat
proof end;
end;

Lemma33: for b1, b2, b3, b4 being Nat st (2 |^ b1) * ((2 * b2) + 1) = (2 |^ b3) * ((2 * b4) + 1) holds
b1 <= b3
proof end;

theorem Th52: :: CARD_4:52
for b1, b2, b3, b4 being Nat st (2 |^ b1) * ((2 * b2) + 1) = (2 |^ b3) * ((2 * b4) + 1) holds
( b1 = b3 & b2 = b4 )
proof end;

Lemma35: for b1 being set st b1 in [:NAT ,NAT :] holds
ex b2, b3 being Nat st b1 = [b2,b3]
proof end;

theorem Th53: :: CARD_4:53
( [:NAT ,NAT :], NAT are_equipotent & Card NAT = Card [:NAT ,NAT :] )
proof end;

theorem Th54: :: CARD_4:54
(alef 0) *` (alef 0) = alef 0 by Th53, CARD_1:83, CARD_1:84, CARD_2:def 2;

theorem Th55: :: CARD_4:55
for b1, b2 being set st b1 is countable & b2 is countable holds
[:b1,b2:] is countable
proof end;

theorem Th56: :: CARD_4:56
for b1 being non empty set holds
( 1 -tuples_on b1,b1 are_equipotent & Card (1 -tuples_on b1) = Card b1 )
proof end;

theorem Th57: :: CARD_4:57
for b1 being non empty set
for b2, b3 being Nat holds
( [:(b2 -tuples_on b1),(b3 -tuples_on b1):],(b2 + b3) -tuples_on b1 are_equipotent & Card [:(b2 -tuples_on b1),(b3 -tuples_on b1):] = Card ((b2 + b3) -tuples_on b1) )
proof end;

theorem Th58: :: CARD_4:58
for b1 being non empty set
for b2 being Nat st b1 is countable holds
b2 -tuples_on b1 is countable
proof end;

theorem Th59: :: CARD_4:59
for b1, b2 being Cardinal
for b3 being Function st Card (dom b3) <=` b1 & ( for b4 being set st b4 in dom b3 holds
Card (b3 . b4) <=` b2 ) holds
Card (Union b3) <=` b1 *` b2
proof end;

theorem Th60: :: CARD_4:60
for b1 being set
for b2, b3 being Cardinal st Card b1 <=` b2 & ( for b4 being set st b4 in b1 holds
Card b4 <=` b3 ) holds
Card (union b1) <=` b2 *` b3
proof end;

theorem Th61: :: CARD_4:61
for b1 being Function st dom b1 is countable & ( for b2 being set st b2 in dom b1 holds
b1 . b2 is countable ) holds
Union b1 is countable
proof end;

theorem Th62: :: CARD_4:62
for b1 being set st b1 is countable & ( for b2 being set st b2 in b1 holds
b2 is countable ) holds
union b1 is countable
proof end;

theorem Th63: :: CARD_4:63
for b1 being Function st dom b1 is finite & ( for b2 being set st b2 in dom b1 holds
b1 . b2 is finite ) holds
Union b1 is finite
proof end;

theorem Th64: :: CARD_4:64
canceled;

theorem Th65: :: CARD_4:65
for b1 being non empty set st b1 is countable holds
b1 * is countable
proof end;

theorem Th66: :: CARD_4:66
for b1 being non empty set holds alef 0 <=` Card (b1 * )
proof end;

scheme :: CARD_4:sch 1
s1{ F1( set ) -> set , P1[ Nat] } :
{ F1(b1) where B is Nat : P1[b1] } is countable
proof end;

scheme :: CARD_4:sch 2
s2{ F1( set , set ) -> set , P1[ set , set ] } :
{ F1(b1,b2) where B is Nat, B is Nat : P1[b1,b2] } is countable
proof end;

scheme :: CARD_4:sch 3
s3{ F1( set , set , set ) -> set , P1[ Nat, Nat, Nat] } :
{ F1(b1,b2,b3) where B is Nat, B is Nat, B is Nat : P1[b1,b2,b3] } is countable
proof end;

theorem Th67: :: CARD_4:67
for b1 being Nat holds
( (alef 0) *` (Card b1) <=` alef 0 & (Card b1) *` (alef 0) <=` alef 0 )
proof end;

theorem Th68: :: CARD_4:68
for b1, b2, b3, b4 being Cardinal st ( ( b1 <` b2 & b3 <` b4 ) or ( b1 <=` b2 & b3 <` b4 ) or ( b1 <` b2 & b3 <=` b4 ) or ( b1 <=` b2 & b3 <=` b4 ) ) holds
( b1 *` b3 <=` b2 *` b4 & b3 *` b1 <=` b2 *` b4 )
proof end;

theorem Th69: :: CARD_4:69
for b1, b2, b3 being Cardinal st ( b1 <` b2 or b1 <=` b2 ) holds
( b3 *` b1 <=` b3 *` b2 & b3 *` b1 <=` b2 *` b3 & b1 *` b3 <=` b3 *` b2 & b1 *` b3 <=` b2 *` b3 ) by Th68;

theorem Th70: :: CARD_4:70
for b1, b2, b3, b4 being Cardinal holds
( ( not ( b1 <` b2 & b3 <` b4 ) & not ( b1 <=` b2 & b3 <` b4 ) & not ( b1 <` b2 & b3 <=` b4 ) & not ( b1 <=` b2 & b3 <=` b4 ) ) or b1 = 0 or exp b1,b3 <=` exp b2,b4 )
proof end;

theorem Th71: :: CARD_4:71
for b1, b2, b3 being Cardinal holds
( ( not b1 <` b2 & not b1 <=` b2 ) or b3 = 0 or ( exp b3,b1 <=` exp b3,b2 & exp b1,b3 <=` exp b2,b3 ) )
proof end;

theorem Th72: :: CARD_4:72
for b1, b2 being Cardinal holds
( b1 <=` b1 +` b2 & b2 <=` b1 +` b2 )
proof end;

theorem Th73: :: CARD_4:73
for b1, b2 being Cardinal st b1 <> 0 holds
( b2 <=` b2 *` b1 & b2 <=` b1 *` b2 )
proof end;

theorem Th74: :: CARD_4:74
for b1, b2, b3, b4 being Cardinal st b1 <` b2 & b3 <` b4 holds
( b1 +` b3 <` b2 +` b4 & b3 +` b1 <` b2 +` b4 )
proof end;

theorem Th75: :: CARD_4:75
for b1, b2, b3 being Cardinal st b1 +` b2 <` b1 +` b3 holds
b2 <` b3
proof end;

theorem Th76: :: CARD_4:76
for b1, b2 being set st (Card b1) +` (Card b2) = Card b1 & Card b2 <` Card b1 holds
Card (b1 \ b2) = Card b1
proof end;

theorem Th77: :: CARD_4:77
for b1 being Cardinal st not b1 is finite holds
b1 *` b1 = b1
proof end;

theorem Th78: :: CARD_4:78
for b1, b2 being Cardinal st not b1 is finite & 0 <` b2 & ( b2 <=` b1 or b2 <` b1 ) holds
( b1 *` b2 = b1 & b2 *` b1 = b1 )
proof end;

theorem Th79: :: CARD_4:79
for b1, b2 being Cardinal st not b1 is finite & ( b2 <=` b1 or b2 <` b1 ) holds
( b1 *` b2 <=` b1 & b2 *` b1 <=` b1 )
proof end;

theorem Th80: :: CARD_4:80
for b1 being set st not b1 is finite holds
( [:b1,b1:],b1 are_equipotent & Card [:b1,b1:] = Card b1 )
proof end;

theorem Th81: :: CARD_4:81
for b1, b2 being set st not b1 is finite & b2 is finite & b2 <> {} holds
( [:b1,b2:],b1 are_equipotent & Card [:b1,b2:] = Card b1 )
proof end;

theorem Th82: :: CARD_4:82
for b1, b2, b3, b4 being Cardinal st b1 <` b2 & b3 <` b4 holds
( b1 *` b3 <` b2 *` b4 & b3 *` b1 <` b2 *` b4 )
proof end;

theorem Th83: :: CARD_4:83
for b1, b2, b3 being Cardinal st b1 *` b2 <` b1 *` b3 holds
b2 <` b3
proof end;

theorem Th84: :: CARD_4:84
for b1 being set st not b1 is finite holds
Card b1 = (alef 0) *` (Card b1)
proof end;

theorem Th85: :: CARD_4:85
for b1, b2 being set st b1 <> {} & b1 is finite & not b2 is finite holds
(Card b2) *` (Card b1) = Card b2
proof end;

theorem Th86: :: CARD_4:86
for b1 being non empty set
for b2 being Nat st not b1 is finite & b2 <> 0 holds
( b2 -tuples_on b1,b1 are_equipotent & Card (b2 -tuples_on b1) = Card b1 )
proof end;

theorem Th87: :: CARD_4:87
for b1 being non empty set st not b1 is finite holds
Card b1 = Card (b1 * )
proof end;