:: CARD_2 semantic presentation
theorem Th1: :: CARD_2:1
canceled;
theorem Th2: :: CARD_2:2
theorem Th3: :: CARD_2:3
theorem Th4: :: CARD_2:4
theorem Th5: :: CARD_2:5
theorem Th6: :: CARD_2:6
deffunc H1( set ) -> set = a1 `1 ;
theorem Th7: :: CARD_2:7
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}:]) )
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:] )
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)
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 :
:: deftheorem Def2 defines *` CARD_2:def 2 :
:: deftheorem Def3 defines exp CARD_2:def 3 :
theorem Th8: :: CARD_2:8
canceled;
theorem Th9: :: CARD_2:9
canceled;
theorem Th10: :: CARD_2:10
canceled;
theorem Th11: :: CARD_2:11
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:]:] )
theorem Th13: :: CARD_2:13
Lemma7:
for b1, b2 being set holds [:b1,b2:],[:(Card b1),b2:] are_equipotent
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):] )
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:] )
theorem Th16: :: CARD_2:16
theorem Th17: :: CARD_2:17
theorem Th18: :: CARD_2:18
deffunc H3( set , set ) -> set = [:a1,{0}:] \/ [:a2,{1}:];
deffunc H4( set , set , set , set ) -> set = [:a1,{a3}:] \/ [:a2,{a4}:];
Lemma12:
2 = {{} ,one }
theorem Th19: :: CARD_2:19
theorem Th20: :: CARD_2:20
theorem Th21: :: CARD_2:21
canceled;
theorem Th22: :: CARD_2:22
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}:]) )
theorem Th24: :: CARD_2:24
theorem Th25: :: CARD_2:25
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:]) )
theorem Th28: :: CARD_2:28
theorem Th29: :: CARD_2:29
Lemma20:
for b1, b2, b3, b4 being set st b1 <> b2 holds
[:b3,{b1}:] misses [:b4,{b2}:]
theorem Th30: :: CARD_2:30
canceled;
theorem Th31: :: CARD_2:31
theorem Th32: :: CARD_2:32
theorem Th33: :: CARD_2:33
theorem Th34: :: CARD_2:34
canceled;
theorem Th35: :: CARD_2:35
theorem Th36: :: CARD_2:36
theorem Th37: :: CARD_2:37
theorem Th38: :: CARD_2:38
theorem Th39: :: CARD_2:39
theorem Th40: :: CARD_2:40
theorem Th41: :: CARD_2:41
theorem Th42: :: CARD_2:42
theorem Th43: :: CARD_2:43
theorem Th44: :: CARD_2:44
theorem Th45: :: CARD_2:45
theorem Th46: :: CARD_2:46
theorem Th47: :: CARD_2:47
theorem Th48: :: CARD_2:48
theorem Th49: :: CARD_2:49
for
b1,
b2 being
Nat holds
b1 + b2 = b1 +^ b2
theorem Th50: :: CARD_2:50
for
b1,
b2 being
Nat holds
b1 * b2 = b1 *^ b2
theorem Th51: :: CARD_2:51
theorem Th52: :: CARD_2:52
theorem Th53: :: CARD_2:53
theorem Th54: :: CARD_2:54
theorem Th55: :: CARD_2:55
canceled;
theorem Th56: :: CARD_2:56
canceled;
theorem Th57: :: CARD_2:57
theorem Th58: :: CARD_2:58
theorem Th59: :: CARD_2:59
theorem Th60: :: CARD_2:60
for
b1 being
set holds
(
Card b1 = 1 iff ex
b2 being
set st
b1 = {b2} )
theorem Th61: :: CARD_2:61
theorem Th62: :: CARD_2:62
theorem Th63: :: CARD_2:63
theorem Th64: :: CARD_2:64
theorem Th65: :: CARD_2:65
theorem Th66: :: CARD_2:66
canceled;
theorem Th67: :: CARD_2:67
theorem Th68: :: CARD_2:68
theorem Th69: :: CARD_2:69
theorem Th70: :: CARD_2:70
theorem Th71: :: CARD_2:71
for
b1,
b2,
b3,
b4 being
set holds
card {b1,b2,b3,b4} <= 4
theorem Th72: :: CARD_2:72
for
b1,
b2,
b3,
b4,
b5 being
set holds
card {b1,b2,b3,b4,b5} <= 5
theorem Th73: :: CARD_2:73
for
b1,
b2,
b3,
b4,
b5,
b6 being
set holds
card {b1,b2,b3,b4,b5,b6} <= 6
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
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
theorem Th76: :: CARD_2:76
theorem Th77: :: CARD_2:77
for
b1,
b2,
b3 being
set st
b1 <> b2 &
b1 <> b3 &
b2 <> b3 holds
card {b1,b2,b3} = 3
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
theorem Th79: :: CARD_2:79
theorem Th80: :: CARD_2:80
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 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}
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
theorem Th81: :: CARD_2:81