:: CARD_1 semantic presentation

Lm1: for A, B being Ordinal st A c= B holds
succ A c= succ B

proof end;

definition

let IT be set ;
attr IT is cardinal means :Def1: :: CARD_1:def 1
ex B being Ordinal st
( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) );

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 :: CARD_1:1

canceled;

theorem :: CARD_1:2

canceled;

theorem :: CARD_1:3

canceled;

theorem Th4: :: CARD_1:4

for X being set ex A being Ordinal st X,A are_equipotent

proof end;

notation

let M, N be Cardinal;
synonym M <=` N for M c= N;
synonym M <` N for M in N;

end;

theorem :: CARD_1:5

canceled;

theorem :: CARD_1:6

canceled;

theorem :: CARD_1:7

canceled;

theorem Th8: :: CARD_1:8

for M, N being Cardinal holds
( M = N iff M,N are_equipotent )

proof end;

theorem :: CARD_1:9

canceled;

theorem :: CARD_1:10

canceled;

theorem :: CARD_1:11

canceled;

theorem :: CARD_1:12

canceled;

theorem :: CARD_1:13

for M, N being Cardinal holds
( M <` N iff ( M <=` N & M <> N ) )

proof end;

theorem :: CARD_1:14

for M, N being Cardinal holds
( M <` N iff not N <=` M ) by ORDINAL1:7, ORDINAL1:26;

definition

let X be set ;
canceled;
canceled;
canceled;
func Card X -> Cardinal means :Def5: :: CARD_1:def 5
X,it are_equipotent ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem CARD_1:def 2 :

:: deftheorem CARD_1:def 3 :

:: deftheorem CARD_1:def 4 :

:: deftheorem Def5 defines Card CARD_1:def 5 :

theorem :: CARD_1:15

canceled;

theorem :: CARD_1:16

canceled;

theorem :: CARD_1:17

canceled;

theorem :: CARD_1:18

canceled;

theorem :: CARD_1:19

canceled;

theorem :: CARD_1:20

canceled;

theorem Th21: :: CARD_1:21

for X, Y being set holds
( X,Y are_equipotent iff Card X = Card Y )

proof end;

theorem Th22: :: CARD_1:22

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

proof end;

theorem Th23: :: CARD_1:23

for X being set
for M being Cardinal st X c= M holds
Card X <=` M

proof end;

theorem Th24: :: CARD_1:24

for A being Ordinal holds Card A c= A

proof end;

theorem :: CARD_1:25

for X being set
for M being Cardinal st X in M holds
Card X <` M

proof end;

theorem Th26: :: CARD_1:26

for X, Y being set holds
( Card X <=` Card Y iff ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) )

proof end;

theorem Th27: :: CARD_1:27

for X, Y being set st X c= Y holds
Card X <=` Card Y

proof end;

theorem :: CARD_1:28

for X, Y being set holds
( Card X <=` Card Y iff ex f being Function st
( dom f = Y & X c= rng f ) )

proof end;

theorem Th29: :: CARD_1:29

for X being set holds not X, bool X are_equipotent

proof end;

theorem Th30: :: CARD_1:30

for X being set holds Card X <` Card (bool X)

proof end;

definition

let X be set ;
func nextcard X -> Cardinal means :Def6: :: CARD_1:def 6
( Card X <` it & ( for M being Cardinal st Card X <` M holds
it <=` M ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines nextcard CARD_1:def 6 :

theorem :: CARD_1:31

canceled;

theorem Th32: :: CARD_1:32

for M being Cardinal holds M <` nextcard M

proof end;

theorem :: CARD_1:33

for X being set holds Card {} <` nextcard X

proof end;

theorem Th34: :: CARD_1:34

for X, Y being set st Card X = Card Y holds
nextcard X = nextcard Y

proof end;

theorem Th35: :: CARD_1:35

for X, Y being set st X,Y are_equipotent holds
nextcard X = nextcard Y

proof end;

theorem :: CARD_1:36

for A being Ordinal holds A in nextcard A

proof end;

definition

let M be Cardinal;
attr M is limit means :Def7: :: CARD_1:def 7
for N being Cardinal holds not M = nextcard N;

end;

:: deftheorem Def7 defines limit CARD_1:def 7 :

notation

let M be Cardinal;
synonym M is_limit_cardinal for limit M;

end;

definition

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

proof end;

end;

:: deftheorem Def8 defines alef CARD_1:def 8 :

Lm2: now

deffunc H₁( Ordinal) -> set = alef $1;
deffunc H₂( Ordinal, set ) -> Cardinal = nextcard (union {$2});
deffunc H₃( Ordinal, T-Sequence) -> Cardinal = Card (sup $2);
A1: for A being Ordinal
for x being set holds
( x = H₁(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = Card NAT & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H₂(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = H₃(C,L | C) ) ) ) by Def8;
H₁( {} ) = Card NAT from ORDINAL2:sch 8( Card NAT , A1);
hence alef 0 = Card NAT ; :: thesis:
thus for A being Ordinal holds H₁( succ A) = H₂(A,H₁(A)) from ORDINAL2:sch 9( Card NAT , A1); :: thesis:
thus for A being Ordinal st A <> {} & A is_limit_ordinal holds
for L being T-Sequence st dom L = A & ( for B being Ordinal st B in A holds
L . B = alef B ) holds
alef A = Card (sup L) :: thesis:

proof

let A be Ordinal; :: thesis:
assume A2: ( A <> {} & A is_limit_ordinal ) ; :: thesis:
let L be T-Sequence; :: thesis:
assume that
A3: dom L = A and
A4: for B being Ordinal st B in A holds
L . B = H₁(B) ; :: thesis:
thus H₁(A) = H₃(A,L) from ORDINAL2:sch 10( L X Card NAT , A1, A2, A3, A4); :: thesis:

end;

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

registration

let A be Ordinal;
cluster alef A -> ordinal cardinal ;
coherence

proof end;

end;

theorem :: CARD_1:37

canceled;

theorem :: CARD_1:38

alef 0 = Card NAT by Lm2;

theorem Th39: :: CARD_1:39

for A being Ordinal holds alef (succ A) = nextcard (alef A)

proof end;

theorem :: CARD_1:40

for A being Ordinal st A <> {} & A is_limit_ordinal holds
for L being T-Sequence st dom L = A & ( for B being Ordinal st B in A holds
L . B = alef B ) holds
alef A = Card (sup L) by Lm2;

theorem Th41: :: CARD_1:41

for A, B being Ordinal holds
( A in B iff alef A <` alef B )

proof end;

theorem Th42: :: CARD_1:42

for A, B being Ordinal st alef A = alef B holds
A = B

proof end;

theorem :: CARD_1:43

for A, B being Ordinal holds
( A c= B iff alef A <=` alef B )

proof end;

theorem :: CARD_1:44

for X, Y, Z being set st X c= Y & Y c= Z & X,Z are_equipotent holds
( X,Y are_equipotent & Y,Z are_equipotent )

proof end;

theorem :: CARD_1:45

for Y, X being set st bool Y c= X holds
( Card Y <` Card X & not Y,X are_equipotent )

proof end;

theorem :: CARD_1:46

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

proof end;

theorem :: CARD_1:47

Card {} = {}

proof end;

theorem Th48: :: CARD_1:48

for X, x being set holds
( X,{x} are_equipotent iff ex x being set st X = {x} )

proof end;

theorem Th49: :: CARD_1:49

for X, x being set holds
( Card X = Card {x} iff ex x being set st X = {x} )

proof end;

theorem :: CARD_1:50

for x being set holds Card {x} = one

proof end;

theorem Th51: :: CARD_1:51

0 = {} ;

theorem Th52: :: CARD_1:52

for n being Nat holds succ n = n + 1

proof end;

theorem :: CARD_1:53

canceled;

theorem :: CARD_1:54

canceled;

theorem :: CARD_1:55

canceled;

theorem Th56: :: CARD_1:56

for n, m being Nat holds
( n <= m iff n c= m )

proof end;

theorem :: CARD_1:57

canceled;

theorem Th58: :: CARD_1:58

for X, X1, Y, Y1 being set st X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1 are_equipotent holds
X \/ X1,Y \/ Y1 are_equipotent

proof end;

theorem Th59: :: CARD_1:59

for x, X, y being set st x in X & y in X holds
X \ {x},X \ {y} are_equipotent

proof end;

theorem Th60: :: CARD_1:60

for X being set
for f being Function st X c= dom f & f is one-to-one holds
X,f .: X are_equipotent

proof end;

theorem Th61: :: CARD_1:61

for X, Y, x, y being set st X,Y are_equipotent & x in X & y in Y holds
X \ {x},Y \ {y} are_equipotent

proof end;

theorem :: CARD_1:62

canceled;

theorem :: CARD_1:63

canceled;

theorem Th64: :: CARD_1:64

for n, m being Nat st n,m are_equipotent holds
n = m

proof end;

theorem Th65: :: CARD_1:65

for x being set st x in omega holds
x is cardinal

proof end;

registration

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

end;

theorem Th66: :: CARD_1:66

for n being Nat holds n = Card n by Def5;

theorem :: CARD_1:67

canceled;

theorem :: CARD_1:68

for X, Y being set st X,Y are_equipotent & X is finite holds
Y is finite

proof end;

theorem Th69: :: CARD_1:69

for n being Nat holds
( n is finite & Card n is finite )

proof end;

theorem :: CARD_1:70

canceled;

theorem Th71: :: CARD_1:71

for n, m being Nat st Card n = Card m holds
n = m

proof end;

theorem Th72: :: CARD_1:72

for n, m being Nat holds
( Card n <=` Card m iff n <= m )

proof end;

theorem Th73: :: CARD_1:73

for n, m being Nat holds
( Card n <` Card m iff n < m )

proof end;

theorem Th74: :: CARD_1:74

for X being set st X is finite holds
ex n being Nat st X,n are_equipotent

proof end;

theorem :: CARD_1:75

canceled;

theorem Th76: :: CARD_1:76

for n being Nat holds nextcard (Card n) = Card (n + 1)

proof end;

notation

let X be finite set ;
synonym card X for Card X;

end;

definition

let X be finite set ;
canceled;
canceled;
:: original: Card
redefine func card X -> Nat means :: CARD_1:def 11
Card it = Card X;
coherence

proof end;

compatibility by Def5;

end;

:: deftheorem CARD_1:def 9 :

:: deftheorem CARD_1:def 10 :

:: deftheorem defines card CARD_1:def 11 :

theorem :: CARD_1:77

canceled;

theorem :: CARD_1:78

card {} = 0 by Def5;

theorem :: CARD_1:79

for x being set holds card {x} = 1

proof end;

theorem :: CARD_1:80

for X, Y being finite set st X c= Y holds
card X <= card Y

proof end;

theorem :: CARD_1:81

for X, Y being finite set st X,Y are_equipotent holds
card X = card Y by Th21;

theorem :: CARD_1:82

for X being set st X is finite holds
nextcard X is finite

proof end;

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

for M being Cardinal holds P₁[M]

provided

A1: P₁[ {} ] and
A2: for M being Cardinal st P₁[M] holds
P₁[ nextcard M] and
A3: for M being Cardinal st M <> {} & M is_limit_cardinal & ( for N being Cardinal st N <` M holds
P₁[N] ) holds
P₁[M]

proof end;

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

for M being Cardinal holds P₁[M]

provided