:: CARD_1 semantic presentation

Lemma1: for b₁, b₂ being Ordinal st b₁ c= b₂ holds
succ b₁ c= succ b₂

proof end;

definition

let c₁ be set ;
attr a₁ is cardinal means :Def1: :: CARD_1:def 1
ex b₁ being Ordinal st
( a₁ = b₁ & ( for b₂ being Ordinal st b₂,b₁ are_equipotent holds
b₁ c= b₂ ) );

end;

:: deftheorem Def1 defines cardinal CARD_1:def 1 :

registration

cluster cardinal set ;
existence

proof end;

end;

definition

mode Cardinal is cardinal set ;

end;

registration

cluster cardinal -> ordinal set ;
coherence

proof end;

end;

theorem Th1: :: CARD_1:1

canceled;

theorem Th2: :: CARD_1:2

canceled;

theorem Th3: :: CARD_1:3

canceled;

theorem Th4: :: CARD_1:4

for b₁ being set ex b₂ being Ordinal st b₁,b₂ are_equipotent

proof end;

notation

let c₁, c₂ be Cardinal;
synonym c₁ <=` c₂ for c₁ c= c₂;
synonym c₁ <` c₂ for c₁ in c₂;

end;

theorem Th5: :: CARD_1:5

canceled;

theorem Th6: :: CARD_1:6

canceled;

theorem Th7: :: CARD_1:7

canceled;

theorem Th8: :: CARD_1:8

for b₁, b₂ being Cardinal holds
( b₁ = b₂ iff b₁,b₂ are_equipotent )

proof end;

theorem Th9: :: CARD_1:9

canceled;

theorem Th10: :: CARD_1:10

canceled;

theorem Th11: :: CARD_1:11

canceled;

theorem Th12: :: CARD_1:12

canceled;

theorem Th13: :: CARD_1:13

for b₁, b₂ being Cardinal holds
( b₁ <` b₂ iff ( b₁ <=` b₂ & b₁ <> b₂ ) )

proof end;

theorem Th14: :: CARD_1:14

for b₁, b₂ being Cardinal holds
( b₁ <` b₂ iff not b₂ <=` b₁ ) by ORDINAL1:7, ORDINAL1:26;

definition

let c₁ be set ;
canceled;
canceled;
canceled;
func Card c₁ -> Cardinal means :Def5: :: CARD_1:def 5
a₁,a₂ are_equipotent ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 CARD_1:def 2 :

:: deftheorem Def3 CARD_1:def 3 :

:: deftheorem Def4 CARD_1:def 4 :

:: deftheorem Def5 defines Card CARD_1:def 5 :

theorem Th15: :: CARD_1:15

canceled;

theorem Th16: :: CARD_1:16

canceled;

theorem Th17: :: CARD_1:17

canceled;

theorem Th18: :: CARD_1:18

canceled;

theorem Th19: :: CARD_1:19

canceled;

theorem Th20: :: CARD_1:20

canceled;

theorem Th21: :: CARD_1:21

for b₁, b₂ being set holds
( b₁,b₂ are_equipotent iff Card b₁ = Card b₂ )

proof end;

theorem Th22: :: CARD_1:22

for b₁ being Relation st b₁ is well-ordering holds
field b₁, order_type_of b₁ are_equipotent

proof end;

theorem Th23: :: CARD_1:23

for b₁ being set
for b₂ being Cardinal st b₁ c= b₂ holds
Card b₁ <=` b₂

proof end;

theorem Th24: :: CARD_1:24

for b₁ being Ordinal holds Card b₁ c= b₁

proof end;

theorem Th25: :: CARD_1:25

for b₁ being set
for b₂ being Cardinal st b₁ in b₂ holds
Card b₁ <` b₂

proof end;

theorem Th26: :: CARD_1:26

for b₁, b₂ being set holds
( Card b₁ <=` Card b₂ iff ex b₃ being Function st
( b₃ is one-to-one & dom b₃ = b₁ & rng b₃ c= b₂ ) )

proof end;

theorem Th27: :: CARD_1:27

for b₁, b₂ being set st b₁ c= b₂ holds
Card b₁ <=` Card b₂

proof end;

theorem Th28: :: CARD_1:28

for b₁, b₂ being set holds
( Card b₁ <=` Card b₂ iff ex b₃ being Function st
( dom b₃ = b₂ & b₁ c= rng b₃ ) )

proof end;

theorem Th29: :: CARD_1:29

for b₁ being set holds not b₁, bool b₁ are_equipotent

proof end;

theorem Th30: :: CARD_1:30

for b₁ being set holds Card b₁ <` Card (bool b₁)

proof end;

definition

let c₁ be set ;
func nextcard c₁ -> Cardinal means :Def6: :: CARD_1:def 6
( Card a₁ <` a₂ & ( for b₁ being Cardinal st Card a₁ <` b₁ holds
a₂ <=` b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines nextcard CARD_1:def 6 :

theorem Th31: :: CARD_1:31

canceled;

theorem Th32: :: CARD_1:32

for b₁ being Cardinal holds b₁ <` nextcard b₁

proof end;

theorem Th33: :: CARD_1:33

for b₁ being set holds Card {} <` nextcard b₁

proof end;

theorem Th34: :: CARD_1:34

for b₁, b₂ being set st Card b₁ = Card b₂ holds
nextcard b₁ = nextcard b₂

proof end;

theorem Th35: :: CARD_1:35

for b₁, b₂ being set st b₁,b₂ are_equipotent holds
nextcard b₁ = nextcard b₂

proof end;

theorem Th36: :: CARD_1:36

for b₁ being Ordinal holds b₁ in nextcard b₁

proof end;

definition

let c₁ be Cardinal;
attr a₁ is limit means :Def7: :: CARD_1:def 7
for b₁ being Cardinal holds not a₁ = nextcard b₁;

end;

:: deftheorem Def7 defines limit CARD_1:def 7 :

notation

let c₁ be Cardinal;
synonym c₁ is_limit_cardinal for limit c₁;

end;

definition

let c₁ be Ordinal;
func alef c₁ -> set means :Def8: :: CARD_1:def 8
ex b₁ being T-Sequence st
( a₂ = last b₁ & dom b₁ = succ a₁ & b₁ . {} = Card NAT & ( for b₂ being Ordinal st succ b₂ in succ a₁ holds
b₁ . (succ b₂) = nextcard (union {(b₁ . b₂)}) ) & ( for b₂ being Ordinal st b₂ in succ a₁ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = Card (sup (b₁ | b₂)) ) );
correctness

proof end;

end;

:: deftheorem Def8 defines alef CARD_1:def 8 :

E20: now

deffunc H₁( Ordinal) -> set = alef a₁;
deffunc H₂( Ordinal, set ) -> Cardinal = nextcard (union {a₂});
deffunc H₃( Ordinal, T-Sequence) -> Cardinal = Card (sup a₂);
E21: for b₁ being Ordinal
for b₂ being set holds
( b₂ = H₁(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = Card NAT & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = H₂(b₄,b₃ . b₄) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = H₃(b₄,b₃ | b₄) ) ) ) by Def8;
H₁( {} ) = Card NAT from ORDINAL2:sch 8(E21);
hence alef 0 = Card NAT ;
thus for b₁ being Ordinal holds H₁( succ b₁) = H₂(b₁,H₁(b₁)) from ORDINAL2:sch 9(E21);
thus for b₁ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal holds
for b₂ being T-Sequence st dom b₂ = b₁ & ( for b₃ being Ordinal st b₃ in b₁ holds
b₂ . b₃ = alef b₃ ) holds
alef b₁ = Card (sup b₂)

proof

let c₁ be Ordinal;
assume E22: ( c₁ <> {} & c₁ is_limit_ordinal ) ;
let c₂ be T-Sequence;
assume that
E23: dom c₂ = c₁ and
E24: for b₁ being Ordinal st b₁ in c₁ holds
c₂ . b₁ = H₁(b₁) ;
thus H₁(c₁) = H₃(c₁,c₂) from ORDINAL2:sch 10(E21, E22, E23, E24);

end;

deffunc H₁( Ordinal) -> set = alef a₁;

registration

let c₁ be Ordinal;
cluster alef a₁ -> ordinal cardinal ;
coherence

proof end;

end;

theorem Th37: :: CARD_1:37

canceled;

theorem Th38: :: CARD_1:38

alef 0 = Card NAT by Lemma20;

theorem Th39: :: CARD_1:39

for b₁ being Ordinal holds alef (succ b₁) = nextcard (alef b₁)

proof end;

theorem Th40: :: CARD_1:40

for b₁ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal holds
for b₂ being T-Sequence st dom b₂ = b₁ & ( for b₃ being Ordinal st b₃ in b₁ holds
b₂ . b₃ = alef b₃ ) holds
alef b₁ = Card (sup b₂) by Lemma20;

theorem Th41: :: CARD_1:41

for b₁, b₂ being Ordinal holds
( b₁ in b₂ iff alef b₁ <` alef b₂ )

proof end;

theorem Th42: :: CARD_1:42

for b₁, b₂ being Ordinal st alef b₁ = alef b₂ holds
b₁ = b₂

proof end;

theorem Th43: :: CARD_1:43

for b₁, b₂ being Ordinal holds
( b₁ c= b₂ iff alef b₁ <=` alef b₂ )

proof end;

theorem Th44: :: CARD_1:44

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₂ c= b₃ & b₁,b₃ are_equipotent holds
( b₁,b₂ are_equipotent & b₂,b₃ are_equipotent )

proof end;

theorem Th45: :: CARD_1:45

for b₁, b₂ being set st bool b₁ c= b₂ holds
( Card b₁ <` Card b₂ & not b₁,b₂ are_equipotent )

proof end;

theorem Th46: :: CARD_1:46

for b₁ being set holds
( b₁, {} are_equipotent iff b₁ = {} )

proof end;

theorem Th47: :: CARD_1:47

Card {} = {}

proof end;

theorem Th48: :: CARD_1:48

for b₁, b₂ being set holds
( b₁,{b₂} are_equipotent iff ex b₃ being set st b₁ = {b₃} )

proof end;

theorem Th49: :: CARD_1:49

for b₁, b₂ being set holds
( Card b₁ = Card {b₂} iff ex b₃ being set st b₁ = {b₃} )

proof end;

theorem Th50: :: CARD_1:50

for b₁ being set holds Card {b₁} = one

proof end;

theorem Th51: :: CARD_1:51

0 = {} ;

theorem Th52: :: CARD_1:52

for b₁ being Nat holds succ b₁ = b₁ + 1

proof end;

theorem Th53: :: CARD_1:53

canceled;

theorem Th54: :: CARD_1:54

canceled;

theorem Th55: :: CARD_1:55

canceled;

theorem Th56: :: CARD_1:56

for b₁, b₂ being Nat holds
( b₁ <= b₂ iff b₁ c= b₂ )

proof end;

theorem Th57: :: CARD_1:57

canceled;

theorem Th58: :: CARD_1:58

for b₁, b₂, b₃, b₄ being set st b₁ misses b₂ & b₃ misses b₄ & b₁,b₃ are_equipotent & b₂,b₄ are_equipotent holds
b₁ \/ b₂,b₃ \/ b₄ are_equipotent

proof end;

theorem Th59: :: CARD_1:59

for b₁, b₂, b₃ being set st b₁ in b₂ & b₃ in b₂ holds
b₂ \ {b₁},b₂ \ {b₃} are_equipotent

proof end;

theorem Th60: :: CARD_1:60

for b₁ being set
for b₂ being Function st b₁ c= dom b₂ & b₂ is one-to-one holds
b₁,b₂ .: b₁ are_equipotent

proof end;

theorem Th61: :: CARD_1:61

for b₁, b₂, b₃, b₄ being set st b₁,b₂ are_equipotent & b₃ in b₁ & b₄ in b₂ holds
b₁ \ {b₃},b₂ \ {b₄} are_equipotent

proof end;

theorem Th62: :: CARD_1:62

canceled;

theorem Th63: :: CARD_1:63

canceled;

theorem Th64: :: CARD_1:64

for b₁, b₂ being Nat st b₁,b₂ are_equipotent holds
b₁ = b₂

proof end;

theorem Th65: :: CARD_1:65

for b₁ being set st b₁ in omega holds
b₁ is cardinal

proof end;

registration

cluster -> ordinal cardinal Element of NAT ;
correctness by Th65;

end;

theorem Th66: :: CARD_1:66

for b₁ being Nat holds b₁ = Card b₁ by Def5;

theorem Th67: :: CARD_1:67

canceled;

theorem Th68: :: CARD_1:68

for b₁, b₂ being set st b₁,b₂ are_equipotent & b₁ is finite holds
b₂ is finite

proof end;

theorem Th69: :: CARD_1:69

for b₁ being Nat holds
( b₁ is finite & Card b₁ is finite )

proof end;

theorem Th70: :: CARD_1:70

canceled;

theorem Th71: :: CARD_1:71

for b₁, b₂ being Nat st Card b₁ = Card b₂ holds
b₁ = b₂

proof end;

theorem Th72: :: CARD_1:72

for b₁, b₂ being Nat holds
( Card b₁ <=` Card b₂ iff b₁ <= b₂ )

proof end;

theorem Th73: :: CARD_1:73

for b₁, b₂ being Nat holds
( Card b₁ <` Card b₂ iff b₁ < b₂ )

proof end;

theorem Th74: :: CARD_1:74

for b₁ being set st b₁ is finite holds
ex b₂ being Nat st b₁,b₂ are_equipotent

proof end;

theorem Th75: :: CARD_1:75

canceled;

theorem Th76: :: CARD_1:76

for b₁ being Nat holds nextcard (Card b₁) = Card (b₁ + 1)

proof end;

notation

let c₁ be finite set ;
synonym card c₁ for Card c₁;

end;

definition

let c₁ be finite set ;
canceled;
canceled;
redefine func Card as card c₁ -> Nat means :: CARD_1:def 11
Card a₂ = Card a₁;
coherence

proof end;

compatibility by Def5;

end;

:: deftheorem Def9 CARD_1:def 9 :

:: deftheorem Def10 CARD_1:def 10 :

:: deftheorem Def11 defines card CARD_1:def 11 :

theorem Th77: :: CARD_1:77

canceled;

theorem Th78: :: CARD_1:78

card {} = 0 by Def5;

theorem Th79: :: CARD_1:79

for b₁ being set holds card {b₁} = 1

proof end;

theorem Th80: :: CARD_1:80

for b₁, b₂ being finite set st b₁ c= b₂ holds
card b₁ <= card b₂

proof end;

theorem Th81: :: CARD_1:81

for b₁, b₂ being finite set st b₁,b₂ are_equipotent holds
card b₁ = card b₂ by Th21;

theorem Th82: :: CARD_1:82

for b₁ being set st b₁ is finite holds
nextcard b₁ is finite

proof end;

scheme :: CARD_1:sch 1
s1{ P₁[ set ] } :

for b₁ being Cardinal holds P₁[b₁]

provided

E42: P₁[ {} ] and
E43: for b₁ being Cardinal st P₁[b₁] holds
P₁[ nextcard b₁] and
E44: for b₁ being Cardinal st b₁ <> {} & b₁ is_limit_cardinal & ( for b₂ being Cardinal st b₂ <` b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;

scheme :: CARD_1:sch 2
s2{ P₁[ set ] } :

for b₁ being Cardinal holds P₁[b₁]

provided

E42: for b₁ being Cardinal st ( for b₂ being Cardinal st b₂ <` b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;

theorem Th83: :: CARD_1:83

alef 0 = omega

proof end;

theorem Th84: :: CARD_1:84

Card omega = omega by Lemma20, Th83;

theorem Th85: :: CARD_1:85

Card omega is_limit_cardinal

proof end;

registration

cluster -> ordinal finite cardinal Element of NAT ;
coherence by Th69;

end;

registration

cluster ordinal finite set ;
existence

proof end;

end;

theorem Th86: :: CARD_1:86

for b₁ being finite Cardinal ex b₂ being Nat st b₁ = Card b₂

proof end;

registration

let c₁ be finite set ;
cluster Card a₁ -> ordinal finite ;
coherence ;

end;