:: Cardinal Numbers
:: by Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let IT be object ;

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 :
for IT being object holds
( IT is cardinal iff ex B being Ordinal st
( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) );

registration

cluster cardinal for set ;

existence
ex b₁ being set st b₁ is cardinal

proof end;

end;

definition

mode Cardinal is cardinal set ;

end;

registration

cluster cardinal -> ordinal for set ;

coherence
for b₁ being set st b₁ is cardinal holds
b₁ is ordinal ;

end;

theorem :: CARD_1:1

canceled;

::$CT

theorem Th1: :: CARD_1:2

for M, N being Cardinal st M,N are_equipotent holds
M = N

proof end;

theorem :: CARD_1:3

for M, N being Cardinal holds
( M in N iff ( M c= N & M <> N ) ) by ORDINAL1:11, XBOOLE_0:def 8;

theorem :: CARD_1:4

for M, N being Cardinal holds
( M in N iff not N c= M ) by ORDINAL1:5, ORDINAL1:16;

definition

let X be set ;

func card X -> Cardinal means :Def2: :: CARD_1:def 2
X,it are_equipotent ;

existence
ex b₁ being Cardinal st X,b₁ are_equipotent

proof end;

uniqueness
for b₁, b₂ being Cardinal st X,b₁ are_equipotent & X,b₂ are_equipotent holds
b₁ = b₂ by Th1, WELLORD2:15;
projectivity
for b₁ being Cardinal
for b₂ being set st b₂,b₁ are_equipotent holds
b₁,b₁ are_equipotent ;

end;

:: deftheorem Def2 defines card CARD_1:def 2 :
for X being set
for b₂ being Cardinal holds
( b₂ = card X iff X,b₂ are_equipotent );

registration

let C be Cardinal;

reduce card C to C;

reducibility
card C = C by Def2;

end;

registration

cluster empty -> cardinal for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is cardinal

proof end;

end;

registration

let X be empty set ;

cluster card X -> empty ;

coherence
card X is empty ;

end;

registration

let X be empty set ;

cluster card X -> zero ;

coherence
card X is zero ;

end;

registration

let X be non empty set ;

cluster card X -> non empty ;

coherence
not card X is empty

proof end;

end;

registration

let X be non empty set ;

cluster card X -> non zero ;

coherence
not card X is zero ;

end;

theorem Th4: :: CARD_1:5

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

proof end;

theorem Th5: :: CARD_1:6

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

proof end;

theorem Th6: :: CARD_1:7

for X being set
for M being Cardinal st X c= M holds
card X c= M

proof end;

theorem Th7: :: CARD_1:8

for A being Ordinal holds card A c= A

proof end;

theorem :: CARD_1:9

for X being set
for M being Cardinal st X in M holds
card X in M by Th7, ORDINAL1:12;

:: Cantor-Bernstein Theorem

theorem Th9: :: CARD_1:10

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

proof end;

theorem Th10: :: CARD_1:11

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

proof end;

theorem Th11: :: CARD_1:12

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

proof end;

theorem Th12: :: CARD_1:13

for X being set holds not X, bool X are_equipotent

proof end;

:: Cantor Theorem

theorem Th13: :: CARD_1:14

for X being set holds card X in card (bool X)

proof end;

definition

let X be set ;

func nextcard X -> Cardinal means :Def3: :: CARD_1:def 3
( card X in it & ( for M being Cardinal st card X in M holds
it c= M ) );

existence
ex b₁ being Cardinal st
( card X in b₁ & ( for M being Cardinal st card X in M holds
b₁ c= M ) )

proof end;

uniqueness
for b₁, b₂ being Cardinal st card X in b₁ & ( for M being Cardinal st card X in M holds
b₁ c= M ) & card X in b₂ & ( for M being Cardinal st card X in M holds
b₂ c= M ) holds
b₁ = b₂ ;

end;

:: deftheorem Def3 defines nextcard CARD_1:def 3 :
for X being set
for b₂ being Cardinal holds
( b₂ = nextcard X iff ( card X in b₂ & ( for M being Cardinal st card X in M holds
b₂ c= M ) ) );

theorem :: CARD_1:15

for X being set holds {} in nextcard X

proof end;

theorem Th15: :: CARD_1:16

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

proof end;

theorem Th16: :: CARD_1:17

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

proof end;

theorem Th17: :: CARD_1:18

for A being Ordinal holds A in nextcard A

proof end;

definition

let M be Cardinal;

attr M is limit_cardinal means :: CARD_1:def 4
for N being Cardinal holds not M = nextcard N;

end;

:: deftheorem defines limit_cardinal CARD_1:def 4 :
for M being Cardinal holds
( M is limit_cardinal iff for N being Cardinal holds not M = nextcard N );

definition

let A be Ordinal;

func aleph A -> set means :Def5: :: CARD_1:def 5
ex S being Sequence st
( it = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) );

correctness
existence
ex b₁ being set ex S being Sequence st
( b₁ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) );
uniqueness
for b₁, b₂ being set st ex S being Sequence st
( b₁ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) & ex S being Sequence st
( b₂ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def5 defines aleph CARD_1:def 5 :
for A being Ordinal
for b₂ being set holds
( b₂ = aleph A iff ex S being Sequence st
( b₂ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) );

Lm1: now :: thesis: ( aleph 0 = card omega & ( for A being Ordinal holds H₃( succ A) = H₂(A,H₃(A)) ) & ( for A being Ordinal st A <> 0 & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) ) )

deffunc H₁( Ordinal, Sequence) -> Cardinal = card (sup $2);
deffunc H₂( Ordinal, set ) -> Cardinal = nextcard $2;
deffunc H₃( Ordinal) -> set = aleph $1;
A1: for A being Ordinal
for x being object holds
( x = H₃(A) iff ex S being Sequence st
( x = last S & dom S = succ A & S . 0 = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H₂(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
S . C = H₁(C,S | C) ) ) ) by Def5;
H₃( 0 ) = card omega from ORDINAL2:sch 8(A1);
hence aleph 0 = card omega ; :: thesis: ( ( for A being Ordinal holds H₃( succ A) = H₂(A,H₃(A)) ) & ( for A being Ordinal st A <> 0 & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) ) )
thus for A being Ordinal holds H₃( succ A) = H₂(A,H₃(A)) from ORDINAL2:sch 9(A1); :: thesis: for A being Ordinal st A <> 0 & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S)
thus for A being Ordinal st A <> 0 & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) :: thesis: verum

proof

let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal implies for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) )
assume A2: ( A <> 0 & A is limit_ordinal ) ; :: thesis: for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S)
let S be Sequence; :: thesis: ( dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) implies aleph A = card (sup S) )
assume that
A3: dom S = A and
A4: for B being Ordinal st B in A holds
S . B = H₃(B) ; :: thesis: aleph A = card (sup S)
thus H₃(A) = H₁(A,S) from ORDINAL2:sch 10(A1, A2, A3, A4); :: thesis: verum

end;

end;

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

registration

let A be Ordinal;

cluster aleph A -> cardinal ;

coherence
aleph A is cardinal

proof end;

end;

theorem :: CARD_1:19

for A being Ordinal holds aleph (succ A) = nextcard (aleph A) by Lm1;

theorem :: CARD_1:20

for A being Ordinal st A <> {} & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) by Lm1;

theorem Th20: :: CARD_1:21

for A, B being Ordinal holds
( A in B iff aleph A in aleph B )

proof end;

theorem Th21: :: CARD_1:22

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

proof end;

theorem :: CARD_1:23

for A, B being Ordinal holds
( A c= B iff aleph A c= aleph B )

proof end;

theorem :: CARD_1:24

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:25

for X, Y being set st bool Y c= X holds
( card Y in card X & not Y,X are_equipotent )

proof end;

theorem Th25: :: CARD_1:26

for X being set st X, {} are_equipotent holds
X = {} by RELAT_1:42;

theorem :: CARD_1:27

card {} = 0 ;

theorem Th27: :: CARD_1:28

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

proof end;

theorem :: CARD_1:29

for X being set
for x being object holds
( card X = card {x} iff ex x being object st X = {x} ) by Th4, Th27;

theorem Th29: :: CARD_1:30

for x being object holds card {x} = 1

proof end;

theorem Th30: :: CARD_1:31

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 Th31: :: CARD_1:32

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

proof end;

theorem Th32: :: CARD_1:33

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 Th33: :: CARD_1:34

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

proof end;

theorem Th34: :: CARD_1:35

for X, Y being set st succ X, succ Y are_equipotent holds
X,Y are_equipotent

proof end;

theorem Th35: :: CARD_1:36

for n being Nat holds
( n = {} or ex m being Nat st n = succ m )

proof end;

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

proof end;

theorem Th36: :: CARD_1:37

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

proof end;

registration

cluster natural -> cardinal for set ;

correctness
coherence
for b₁ being number st b₁ is natural holds
b₁ is cardinal ;
by Th36;

end;

theorem Th37: :: CARD_1:38

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

proof end;

theorem Th38: :: CARD_1:39

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

proof end;

theorem :: CARD_1:40

for m, n being Nat st card n = card m holds
n = m ;

theorem :: CARD_1:41

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

theorem :: CARD_1:42

for m, n being Nat holds
( card n in card m iff n in m ) ;

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

proof end;

theorem :: CARD_1:43

canceled;

::$CT

theorem Th42: :: CARD_1:44

for n being Nat holds nextcard (card n) = card (succ n)

proof end;

:: definition
:: let n be Nat;
:: redefine func succ n -> Element of omega;
:: coherence by ORDINAL1:def 12;
:: end;

definition

let X be finite set ;
:: original: card
redefine func card X -> Element of omega ;
coherence
card X is Element of omega

proof end;

end;

theorem :: CARD_1:45

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 in 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

A1: for M being Cardinal st ( for N being Cardinal st N in M holds
P₁[N] ) holds
P₁[M]

proof end;

theorem Th44: :: CARD_1:46

aleph 0 = omega

proof end;

registration

cluster omega -> cardinal for number ;

coherence
for b₁ being number st b₁ = omega holds
b₁ is cardinal by Th44;

end;

theorem :: CARD_1:47

card omega = omega ;

registration

cluster omega -> limit_cardinal ;

coherence
omega is limit_cardinal

proof end;

end;

registration

cluster -> finite for Element of omega ;

coherence
for b₁ being Element of omega holds b₁ is finite by Th38;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal finite cardinal for set ;

existence
ex b₁ being Cardinal st b₁ is finite

proof end;

end;

theorem :: CARD_1:48

for M being finite Cardinal ex n being Nat st M = card n

proof end;

registration

let X be finite set ;

cluster card X -> finite ;

coherence
card X is finite ;

end;

Lm4: for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n

proof end;

Lm5: for A being Ordinal holds
( A is finite iff A in omega )

proof end;

registration

cluster omega -> infinite ;

coherence
not omega is finite

proof end;

end;

registration

cluster infinite for set ;

existence
ex b₁ being set st b₁ is infinite

proof end;

end;

registration

let X be infinite set ;

cluster card X -> infinite ;

coherence
not card X is finite

proof end;

end;

theorem Th47: :: CARD_1:49

1 = {0}

proof end;

theorem Th48: :: CARD_1:50

2 = {0,1}

proof end;

theorem Th49: :: CARD_1:51

3 = {0,1,2}

proof end;

theorem Th50: :: CARD_1:52

4 = {0,1,2,3}

proof end;

theorem Th51: :: CARD_1:53

5 = {0,1,2,3,4}

proof end;

theorem Th52: :: CARD_1:54

6 = {0,1,2,3,4,5}

proof end;

theorem Th53: :: CARD_1:55

7 = {0,1,2,3,4,5,6}

proof end;

theorem Th54: :: CARD_1:56

8 = {0,1,2,3,4,5,6,7}

proof end;

theorem Th55: :: CARD_1:57

9 = {0,1,2,3,4,5,6,7,8}

proof end;

theorem :: CARD_1:58

10 = {0,1,2,3,4,5,6,7,8,9}

proof end;

:: Moved from FRECHET2 by AK on 27.12.2006

theorem :: CARD_1:59

for f being Function st dom f is infinite & f is one-to-one holds
rng f is infinite

proof end;

registration

cluster natural non zero for object ;

existence
ex b₁ being object st
( not b₁ is zero & b₁ is natural )

proof end;

cluster epsilon-transitive epsilon-connected ordinal natural non zero cardinal for set ;

existence
not for b₁ being Nat holds b₁ is zero

proof end;

end;

registration

let n be natural non zero Number ;

cluster Segm n -> non empty ;

coherence
not Segm n is empty

proof end;

end;

definition

let n be natural Number ;
:: original: Segm
redefine func Segm n -> Subset of omega;
coherence
Segm n is Subset of omega

proof end;

end;

:: from CARD_4, 2007.08.16, A.T.

theorem :: CARD_1:60

for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n by Lm4;

theorem :: CARD_1:61

for A being Ordinal holds
( A is finite iff A in omega ) by Lm5;

registration

cluster natural -> finite for set ;

coherence
for b₁ being set st b₁ is natural holds
b₁ is finite ;

end;

:: from CARD_4, CARD_5 etc. 2008.02.21, A.T.

registration

let A be infinite set ;

cluster bool A -> infinite ;

coherence
not bool A is finite

proof end;

let B be non empty set ;

cluster [:A,B:] -> infinite ;

coherence
not [:A,B:] is finite

proof end;

cluster [:B,A:] -> infinite ;

coherence
not [:B,A:] is finite

proof end;

end;

registration

let X be infinite set ;

cluster infinite for Element of bool X;

existence
ex b₁ being Subset of X st b₁ is infinite

proof end;

end;

:: from NECKLA_2, 2008.06.28, A.T.

registration

cluster ordinal finite -> natural for set ;

coherence
for b₁ being number st b₁ is finite & b₁ is ordinal holds
b₁ is natural by Lm5;

end;

theorem Th60: :: CARD_1:62

for f being Function holds card f = card (dom f)

proof end;

registration

let X be finite set ;

cluster RelIncl X -> finite ;

coherence
RelIncl X is finite

proof end;

end;

:: from AMISTD_2, 2010.01.10, A.T

theorem :: CARD_1:63

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

proof end;

theorem :: CARD_1:64

for x being object
for k being Nat holds card (k --> x) = k

proof end;

definition

let N be object ;
let X be set ;

attr X is N -element means :Def6: :: CARD_1:def 7
card X = N;

end;

:: deftheorem CARD_1:def 6 :
canceled;

:: deftheorem Def6 defines -element CARD_1:def 7 :
for N being object
for X being set holds
( X is N -element iff card X = N );

registration

let N be Cardinal;

cluster N -element for set ;

existence
ex b₁ being set st b₁ is N -element

proof end;

end;

registration

cluster 0 -element -> empty for set ;

coherence
for b₁ being set st b₁ is 0 -element holds
b₁ is empty ;

cluster empty -> 0 -element for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is 0 -element ;

end;

registration

let x be object ;

cluster {x} -> 1 -element ;

coherence
{x} is 1 -element

proof end;

end;

registration

let N be Cardinal;

cluster Relation-like Function-like N -element for set ;

existence
ex b₁ being Function st b₁ is N -element

proof end;

end;

registration

let N be Cardinal;
let f be N -element Function;

cluster dom f -> N -element ;

coherence
dom f is N -element

proof end;

end;

registration

cluster 1 -element -> non empty trivial for set ;

coherence
for b₁ being set st b₁ is 1 -element holds
( b₁ is trivial & not b₁ is empty )

proof end;

cluster non empty trivial -> 1 -element for set ;

coherence
for b₁ being set st b₁ is trivial & not b₁ is empty holds
b₁ is 1 -element

proof end;

end;

registration

let X be non empty set ;

cluster 1 -element for Element of bool X;

existence
ex b₁ being Subset of X st b₁ is 1 -element

proof end;

end;

definition

let X be non empty set ;
mode Singleton of X is 1 -element Subset of X;

end;

theorem Th63: :: CARD_1:65

for X being non empty set
for A being Singleton of X ex x being Element of X st A = {x}

proof end;

theorem Th64: :: CARD_1:66

for X, Y being set holds
( card X c= card Y iff ex f being Function st X c= f .: Y )

proof end;

theorem :: CARD_1:67

for X being set
for f being Function holds card (f .: X) c= card X by Th64;

theorem :: CARD_1:68

for X, Y being set st card X in card Y holds
Y \ X <> {}

proof end;

theorem :: CARD_1:69

for X being set
for x being object holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )

proof end;

:: from POLYFORM, 2011.07.25, A.T.

theorem :: CARD_1:70

for f being Function st f is one-to-one holds
card (dom f) = card (rng f)

proof end;

registration

let F be non trivial set ;
let A be Singleton of F;

cluster F \ A -> non empty ;

coherence
not F \ A is empty

proof end;

end;

registration

let k be non empty Cardinal;

cluster k -element -> non empty for set ;

coherence
for b₁ being set st b₁ is k -element holds
not b₁ is empty ;

end;

registration

let k be natural Number ;

cluster Segm k -> finite ;

coherence
Segm k is finite ;

end;

theorem :: CARD_1:71

for f being Function
for x, y being object holds card (f +~ (x,y)) = card f

proof end;

registration

let n be natural non zero Number ;

cluster Segm n -> with_zero ;

coherence
Segm n is with_zero by ORDINAL3:8;

end;

registration

let c be Cardinal;

cluster cardinal for Element of bool c;

existence
ex b₁ being Subset of c st b₁ is cardinal

proof end;

end;