:: CARD_2 semantic presentation

theorem Th1: :: CARD_2:1
canceled;

theorem Th2: :: CARD_2:2
for b1, b2 being set holds
( Card b1 <=` Card b2 iff ex b3 being Function st b1 c= b3 .: b2 )
proof end;

theorem Th3: :: CARD_2:3
for b1 being set
for b2 being Function holds Card (b2 .: b1) <=` Card b1 by Th2;

theorem Th4: :: CARD_2:4
for b1, b2 being set st Card b1 <` Card b2 holds
b2 \ b1 <> {}
proof end;

theorem Th5: :: CARD_2:5
for b1, b2, b3 being set st b1 in b2 & b2,b3 are_equipotent holds
( b3 <> {} & ex b4 being set st b4 in b3 )
proof end;

theorem Th6: :: CARD_2:6
for b1 being set holds
( bool b1, bool (Card b1) are_equipotent & Card (bool b1) = Card (bool (Card b1)) )
proof end;

deffunc H1( set ) -> set = a1 `1 ;

theorem Th7: :: CARD_2:7
for b1, b2, b3 being set st b1 in Funcs b2,b3 holds
( b1,b2 are_equipotent & Card b1 = Card b2 )
proof end;

Lemma3: for b1, b2 being Ordinal
for b3, b4 being set st b3 <> b4 holds
( b1 +^ b2,[:b1,{b3}:] \/ [:b2,{b4}:] are_equipotent & Card (b1 +^ b2) = Card ([:b1,{b3}:] \/ [:b2,{b4}:]) )
proof end;

deffunc H2( set , set ) -> set = [:a1,{0}:] \/ [:a2,{1}:];

Lemma4: for b1, b2 being set holds
( [:b1,b2:],[:b2,b1:] are_equipotent & Card [:b1,b2:] = Card [:b2,b1:] )
proof end;

definition
let c1, c2 be Cardinal;
func c1 +` c2 -> Cardinal equals :: CARD_2:def 1
 Card (a1 +^ a2);
coherence
Card (c1 +^ c2) is Cardinal ;
commutativity
for b1, b2, b3 being Cardinal st b1 = Card (b2 +^ b3) holds
b1 = Card (b3 +^ b2)
proof end;
func c1 *` c2 -> Cardinal equals :: CARD_2:def 2
 Card [:a1,a2:];
coherence
Card [:c1,c2:] is Cardinal ;
commutativity
for b1, b2, b3 being Cardinal st b1 = Card [:b2,b3:] holds
b1 = Card [:b3,b2:] by Lemma4;
func exp c1,c2 -> Cardinal equals :: CARD_2:def 3
 Card (Funcs a2,a1);
coherence
Card (Funcs c2,c1) is Cardinal ;
end;

:: deftheorem Def1 defines +` CARD_2:def 1 :
for b1, b2 being Cardinal holds b1 +` b2 = Card (b1 +^ b2);

:: deftheorem Def2 defines *` CARD_2:def 2 :
for b1, b2 being Cardinal holds b1 *` b2 = Card [:b1,b2:];

:: deftheorem Def3 defines exp CARD_2:def 3 :
for b1, b2 being Cardinal holds exp b1,b2 = Card (Funcs b2,b1);

theorem Th8: :: CARD_2:8
canceled;

theorem Th9: :: CARD_2:9
canceled;

theorem Th10: :: CARD_2:10
canceled;

theorem Th11: :: CARD_2:11
for b1, b2 being set holds
( [:b1,b2:],[:b2,b1:] are_equipotent & Card [:b1,b2:] = Card [:b2,b1:] ) by Lemma4;

theorem Th12: :: CARD_2:12
for b1, b2, b3 being set holds
( [:[:b1,b2:],b3:],[:b1,[:b2,b3:]:] are_equipotent & Card [:[:b1,b2:],b3:] = Card [:b1,[:b2,b3:]:] )
proof end;

theorem Th13: :: CARD_2:13
for b1, b2 being set holds
( b1,[:b1,{b2}:] are_equipotent & Card b1 = Card [:b1,{b2}:] )
proof end;

Lemma7: for b1, b2 being set holds [:b1,b2:],[:(Card b1),b2:] are_equipotent
proof end;

theorem Th14: :: CARD_2:14
for b1, b2 being set holds
( [:b1,b2:],[:(Card b1),b2:] are_equipotent & [:b1,b2:],[:b1,(Card b2):] are_equipotent & [:b1,b2:],[:(Card b1),(Card b2):] are_equipotent & Card [:b1,b2:] = Card [:(Card b1),b2:] & Card [:b1,b2:] = Card [:b1,(Card b2):] & Card [:b1,b2:] = Card [:(Card b1),(Card b2):] )
proof end;

theorem Th15: :: CARD_2:15
for b1, b2, b3, b4 being set st b1,b2 are_equipotent & b3,b4 are_equipotent holds
( [:b1,b3:],[:b2,b4:] are_equipotent & Card [:b1,b3:] = Card [:b2,b4:] )
proof end;

theorem Th16: :: CARD_2:16
for b1, b2 being Ordinal
for b3, b4 being set st b3 <> b4 holds
( b1 +^ b2,[:b1,{b3}:] \/ [:b2,{b4}:] are_equipotent & Card (b1 +^ b2) = Card ([:b1,{b3}:] \/ [:b2,{b4}:]) ) by Lemma3;

theorem Th17: :: CARD_2:17
for b1, b2 being Cardinal
for b3, b4 being set st b3 <> b4 holds
( b1 +` b2,[:b1,{b3}:] \/ [:b2,{b4}:] are_equipotent & b1 +` b2 = Card ([:b1,{b3}:] \/ [:b2,{b4}:]) )
proof end;

theorem Th18: :: CARD_2:18
for b1, b2 being Ordinal holds
( b1 *^ b2,[:b1,b2:] are_equipotent & Card (b1 *^ b2) = Card [:b1,b2:] )
proof end;

deffunc H3( set , set ) -> set = [:a1,{0}:] \/ [:a2,{1}:];

deffunc H4( set , set , set , set ) -> set = [:a1,{a3}:] \/ [:a2,{a4}:];

Lemma12: 2 = {{} ,one }
proof end;

theorem Th19: :: CARD_2:19
( 0 = Card {} & 1 = Card one & 2 = Card (succ one ) )
proof end;

theorem Th20: :: CARD_2:20
1 = one
proof end;

theorem Th21: :: CARD_2:21
canceled;

theorem Th22: :: CARD_2:22
( 2 = {{} ,one } & 2 = succ one )
proof end;

theorem Th23: :: CARD_2:23
for b1, b2, b3, b4, b5, b6, b7, b8 being set st b1,b2 are_equipotent & b3,b4 are_equipotent & b5 <> b6 & b7 <> b8 holds
( [:b1,{b5}:] \/ [:b3,{b6}:],[:b2,{b7}:] \/ [:b4,{b8}:] are_equipotent & Card ([:b1,{b5}:] \/ [:b3,{b6}:]) = Card ([:b2,{b7}:] \/ [:b4,{b8}:]) )
proof end;

theorem Th24: :: CARD_2:24
for b1, b2 being Ordinal holds Card (b1 +^ b2) = (Card b1) +` (Card b2)
proof end;

theorem Th25: :: CARD_2:25
for b1, b2 being Ordinal holds Card (b1 *^ b2) = (Card b1) *` (Card b2)
proof end;

theorem Th26: :: CARD_2:26
for b1, b2 being set holds
( [:b1,{0}:] \/ [:b2,{1}:],[:b2,{0}:] \/ [:b1,{1}:] are_equipotent & Card ([:b1,{0}:] \/ [:b2,{1}:]) = Card ([:b2,{0}:] \/ [:b1,{1}:]) ) by Th23;

theorem Th27: :: CARD_2:27
for b1, b2, b3, b4 being set holds
( [:b1,b2:] \/ [:b3,b4:],[:b2,b1:] \/ [:b4,b3:] are_equipotent & Card ([:b1,b2:] \/ [:b3,b4:]) = Card ([:b2,b1:] \/ [:b4,b3:]) )
proof end;

theorem Th28: :: CARD_2:28
for b1, b2, b3, b4 being set st b1 <> b2 holds
(Card b3) +` (Card b4) = Card ([:b3,{b1}:] \/ [:b4,{b2}:])
proof end;

theorem Th29: :: CARD_2:29
for b1 being Cardinal holds b1 +` 0 = b1
proof end;

Lemma20: for b1, b2, b3, b4 being set st b1 <> b2 holds
[:b3,{b1}:] misses [:b4,{b2}:]
proof end;

theorem Th30: :: CARD_2:30
canceled;

theorem Th31: :: CARD_2:31
for b1, b2, b3 being Cardinal holds (b1 +` b2) +` b3 = b1 +` (b2 +` b3)
proof end;

theorem Th32: :: CARD_2:32
for b1 being Cardinal holds b1 *` 0 = 0 by CARD_1:47, ZFMISC_1:113;

theorem Th33: :: CARD_2:33
for b1 being Cardinal holds b1 *` 1 = b1
proof end;

theorem Th34: :: CARD_2:34
canceled;

theorem Th35: :: CARD_2:35
for b1, b2, b3 being Cardinal holds (b1 *` b2) *` b3 = b1 *` (b2 *` b3)
proof end;

theorem Th36: :: CARD_2:36
for b1 being Cardinal holds 2 *` b1 = b1 +` b1
proof end;

theorem Th37: :: CARD_2:37
for b1, b2, b3 being Cardinal holds b1 *` (b2 +` b3) = (b1 *` b2) +` (b1 *` b3)
proof end;

theorem Th38: :: CARD_2:38
for b1 being Cardinal holds exp b1,0 = 1
proof end;

theorem Th39: :: CARD_2:39
for b1 being Cardinal st b1 <> 0 holds
exp 0,b1 = 0 by CARD_1:47, FUNCT_2:14;

theorem Th40: :: CARD_2:40
for b1 being Cardinal holds
( exp b1,1 = b1 & exp 1,b1 = 1 )
proof end;

theorem Th41: :: CARD_2:41
for b1, b2, b3 being Cardinal holds exp b1,(b2 +` b3) = (exp b1,b2) *` (exp b1,b3)
proof end;

theorem Th42: :: CARD_2:42
for b1, b2, b3 being Cardinal holds exp (b1 *` b2),b3 = (exp b1,b3) *` (exp b2,b3)
proof end;

theorem Th43: :: CARD_2:43
for b1, b2, b3 being Cardinal holds exp b1,(b2 *` b3) = exp (exp b1,b2),b3
proof end;

theorem Th44: :: CARD_2:44
for b1 being set holds exp 2,(Card b1) = Card (bool b1)
proof end;

theorem Th45: :: CARD_2:45
for b1 being Cardinal holds exp b1,2 = b1 *` b1 by Th22, FUNCT_5:73;

theorem Th46: :: CARD_2:46
for b1, b2 being Cardinal holds exp (b1 +` b2),2 = ((b1 *` b1) +` ((2 *` b1) *` b2)) +` (b2 *` b2)
proof end;

theorem Th47: :: CARD_2:47
for b1, b2 being set holds Card (b1 \/ b2) <=` (Card b1) +` (Card b2)
proof end;

theorem Th48: :: CARD_2:48
for b1, b2 being set st b1 misses b2 holds
Card (b1 \/ b2) = (Card b1) +` (Card b2)
proof end;

theorem Th49: :: CARD_2:49
for b1, b2 being Nat holds b1 + b2 = b1 +^ b2
proof end;

theorem Th50: :: CARD_2:50
for b1, b2 being Nat holds b1 * b2 = b1 *^ b2
proof end;

theorem Th51: :: CARD_2:51
for b1, b2 being Nat holds Card (b1 + b2) = (Card b1) +` (Card b2)
proof end;

theorem Th52: :: CARD_2:52
for b1, b2 being Nat holds Card (b1 * b2) = (Card b1) *` (Card b2)
proof end;

theorem Th53: :: CARD_2:53
for b1, b2 being finite set st b1 misses b2 holds
card (b1 \/ b2) = (card b1) + (card b2)
proof end;

theorem Th54: :: CARD_2:54
for b1 being set
for b2 being finite set st not b1 in b2 holds
card (b2 \/ {b1}) = (card b2) + 1
proof end;

theorem Th55: :: CARD_2:55
canceled;

theorem Th56: :: CARD_2:56
canceled;

theorem Th57: :: CARD_2:57
for b1, b2 being finite set holds
( Card b1 <=` Card b2 iff card b1 <= card b2 )
proof end;

theorem Th58: :: CARD_2:58
for b1, b2 being finite set holds
( Card b1 <` Card b2 iff card b1 < card b2 )
proof end;

theorem Th59: :: CARD_2:59
for b1 being set st Card b1 = 0 holds
b1 = {}
proof end;

theorem Th60: :: CARD_2:60
for b1 being set holds
( Card b1 = 1 iff ex b2 being set st b1 = {b2} )
proof end;

theorem Th61: :: CARD_2:61
for b1 being finite set holds
( b1, card b1 are_equipotent & b1, Card (card b1) are_equipotent & b1, Seg (card b1) are_equipotent )
proof end;

theorem Th62: :: CARD_2:62
for b1, b2 being finite set holds card (b1 \/ b2) <= (card b1) + (card b2)
proof end;

theorem Th63: :: CARD_2:63
for b1, b2 being finite set st b2 c= b1 holds
card (b1 \ b2) = (card b1) - (card b2)
proof end;

theorem Th64: :: CARD_2:64
for b1, b2 being finite set holds card (b1 \/ b2) = ((card b1) + (card b2)) - (card (b1 /\ b2))
proof end;

theorem Th65: :: CARD_2:65
for b1, b2 being finite set holds card [:b1,b2:] = (card b1) * (card b2)
proof end;

theorem Th66: :: CARD_2:66
canceled;

theorem Th67: :: CARD_2:67
for b1, b2 being finite set st b1 c< b2 holds
( card b1 < card b2 & Card b1 <` Card b2 )
proof end;

theorem Th68: :: CARD_2:68
for b1, b2 being set st ( Card b1 <=` Card b2 or Card b1 <` Card b2 ) & b2 is finite holds
b1 is finite
proof end;

theorem Th69: :: CARD_2:69
for b1, b2 being set holds card {b1,b2} <= 2
proof end;

theorem Th70: :: CARD_2:70
for b1, b2, b3 being set holds card {b1,b2,b3} <= 3
proof end;

theorem Th71: :: CARD_2:71
for b1, b2, b3, b4 being set holds card {b1,b2,b3,b4} <= 4
proof end;

theorem Th72: :: CARD_2:72
for b1, b2, b3, b4, b5 being set holds card {b1,b2,b3,b4,b5} <= 5
proof end;

theorem Th73: :: CARD_2:73
for b1, b2, b3, b4, b5, b6 being set holds card {b1,b2,b3,b4,b5,b6} <= 6
proof end;

theorem Th74: :: CARD_2:74
for b1, b2, b3, b4, b5, b6, b7 being set holds card {b1,b2,b3,b4,b5,b6,b7} <= 7
proof end;

theorem Th75: :: CARD_2:75
for b1, b2, b3, b4, b5, b6, b7, b8 being set holds card {b1,b2,b3,b4,b5,b6,b7,b8} <= 8
proof end;

theorem Th76: :: CARD_2:76
for b1, b2 being set st b1 <> b2 holds
card {b1,b2} = 2
proof end;

theorem Th77: :: CARD_2:77
for b1, b2, b3 being set st b1 <> b2 & b1 <> b3 & b2 <> b3 holds
card {b1,b2,b3} = 3
proof end;

theorem Th78: :: CARD_2:78
for b1, b2, b3, b4 being set st b1 <> b2 & b1 <> b3 & b1 <> b4 & b2 <> b3 & b2 <> b4 & b3 <> b4 holds
card {b1,b2,b3,b4} = 4
proof end;

theorem Th79: :: CARD_2:79
for b1 being finite set st card b1 = 2 holds
ex b2, b3 being set st
( b2 <> b3 & b1 = {b2,b3} )
proof end;

theorem Th80: :: CARD_2:80
for b1 being Function holds Card (rng b1) c= Card (dom b1)
proof end;

E48: now
let c1 be Nat;
assume E49: for b1 being finite set st card b1 = c1 & b1 <> {} & ( for b2, b3 being set st b2 in b1 & b3 in b1 & not b2 c= b3 holds
b3 c= b2 ) holds
union b1 in b1 ;
let c2 be finite set ;
assume that
E50: card c2 = c1 + 1 and
E51: c2 <> {} and
E52: for b1, b2 being set st b1 in c2 & b2 in c2 & not b1 c= b2 holds
b2 c= b1 ;
consider c3 being Element of c2;
per cases ( c1 = 0 or c1 <> 0 ) ;
suppose c1 = 0 ;
then consider c4 being set such that
E53: c2 = {c4} by E50, Th60;
( c3 = c4 & union c2 = c4 ) by E53, TARSKI:def 1, ZFMISC_1:31;
hence union c2 in c2 by E51;
end;
suppose E53: c1 <> 0 ;
set c4 = c2 \ {c3};
E54: c2 \ {c3} c= c2 by XBOOLE_1:36;
reconsider c5 = c2 \ {c3} as finite set ;
{c3} c= c2 by E51, ZFMISC_1:37;
then E55: card c5 = (c1 + 1) - (card {c3}) by E50, Th63
.= (c1 + 1) - 1 by CARD_1:79
.= c1 ;
for b1, b2 being set st b1 in c5 & b2 in c5 & not b1 c= b2 holds
b2 c= b1 by E52, E54;
then E56: union c5 in c5 by E49, E53, E55, CARD_1:47;
then E57: union c5 in c2 by E54;
E58: ( c3 c= union c5 or union c5 c= c3 ) by E52, E54, E56;
E59: c3 in c2 by E51;
c2 = (c2 \ {c3}) \/ {c3}
proof
thus c2 c= (c2 \ {c3}) \/ {c3} :: according to XBOOLE_0:def 10
proof
let c6 be set ; :: according to TARSKI:def 3
assume c6 in c2 ;
then ( c6 in c2 \ {c3} or c6 in {c3} ) by XBOOLE_0:def 4;
hence c6 in (c2 \ {c3}) \/ {c3} by XBOOLE_0:def 2;
end;
let c6 be set ; :: according to TARSKI:def 3
assume c6 in (c2 \ {c3}) \/ {c3} ;
then ( c6 in c2 \ {c3} or c6 in {c3} ) by XBOOLE_0:def 2;
then ( ( c6 in c2 & not c6 in {c3} ) or c6 in {c3} ) by XBOOLE_0:def 4;
then ( c6 in c2 \/ {c3} & {c3} c= c2 ) by E51, XBOOLE_0:def 2, ZFMISC_1:37;
hence c6 in c2 by XBOOLE_1:12;
end;
then union c2 = (union c5) \/ (union {c3}) by ZFMISC_1:96
.= (union c5) \/ c3 by ZFMISC_1:31 ;
hence union c2 in c2 by E57, E58, E59, XBOOLE_1:12;
end;
end;
end;

Lemma49: for b1 being finite set st b1 <> {} & ( for b2, b3 being set st b2 in b1 & b3 in b1 & not b2 c= b3 holds
b3 c= b2 ) holds
union b1 in b1
proof end;

theorem Th81: :: CARD_2:81
for b1 being set st b1 <> {} & b1 is finite & ( for b2, b3 being set st b2 in b1 & b3 in b1 & not b2 c= b3 holds
b3 c= b2 ) holds
union b1 in b1 by Lemma49;