:: Cardinal Numbers
:: by Grzegorz Bancerek
::
:: 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
existence
ex b1 being set st b1 is cardinal
proof end;
end;

definition end;

registration
coherence
for b1 being set st b1 is cardinal holds
b1 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 ; theorem :: CARD_1:4 for M, N being Cardinal holds ( M in N iff not N c= M ) by ; definition let X be set ; func card X -> Cardinal means :Def2: :: CARD_1:def 2 X,it are_equipotent ; existence ex b1 being Cardinal st X,b1 are_equipotent proof end; uniqueness for b1, b2 being Cardinal st X,b1 are_equipotent & X,b2 are_equipotent holds b1 = b2 by ; projectivity for b1 being Cardinal for b2 being set st b2,b1 are_equipotent holds b1,b1 are_equipotent ; end; :: deftheorem Def2 defines card CARD_1:def 2 : for X being set for b2 being Cardinal holds ( b2 = card X iff X,b2 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 b1 being set st b1 is empty holds b1 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 ; :: 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 b1 being Cardinal st ( card X in b1 & ( for M being Cardinal st card X in M holds b1 c= M ) ) proof end; uniqueness for b1, b2 being Cardinal st card X in b1 & ( for M being Cardinal st card X in M holds b1 c= M ) & card X in b2 & ( for M being Cardinal st card X in M holds b2 c= M ) holds b1 = b2 ; end; :: deftheorem Def3 defines nextcard CARD_1:def 3 : for X being set for b2 being Cardinal holds ( b2 = nextcard X iff ( card X in b2 & ( for M being Cardinal st card X in M holds b2 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 b1 being set ex S being Sequence st ( b1 = 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 b1, b2 being set st ex S being Sequence st ( b1 = 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 ( b2 = 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 b1 = b2 ; proof end; end; :: deftheorem Def5 defines aleph CARD_1:def 5 : for A being Ordinal for b2 being set holds ( b2 = aleph A iff ex S being Sequence st ( b2 = 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 H3( succ A) = H2(A,H3(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 H1( Ordinal, Sequence) -> Cardinal = card (sup$2);
deffunc H2( Ordinal, set ) -> Cardinal = nextcard $2; deffunc H3( Ordinal) -> set = aleph$1;
A1: for A being Ordinal
for x being object holds
( x = H3(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) = H2(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
S . C = H1(C,S | C) ) ) ) by Def5;
H3( 0 ) = card omega from hence aleph 0 = card omega ; :: thesis: ( ( for A being Ordinal holds H3( succ A) = H2(A,H3(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 H3( succ A) = H2(A,H3(A)) from :: 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 = H3(B) ; :: thesis: aleph A = card (sup S)
thus H3(A) = H1(A,S) from ORDINAL2:sch 10(A1, A2, A3, A4); :: thesis: verum
end;
end;

deffunc H1( Ordinal) -> set = aleph $1; registration let A be Ordinal; coherence proof end; end; theorem :: CARD_1:19 for A being Ordinal holds aleph (succ A) = nextcard () 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 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 ; 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 correctness coherence for b1 being number st b1 is natural holds b1 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{ P1[ set ] } :
for M being Cardinal holds P1[M]
provided
A1: P1[ {} ] and
A2: for M being Cardinal st P1[M] holds
P1[ nextcard M] and
A3: for M being Cardinal st M <> {} & M is limit_cardinal & ( for N being Cardinal st N in M holds
P1[N] ) holds
P1[M]
proof end;

scheme :: CARD_1:sch 2
CardinalCompInd{ P1[ set ] } :
for M being Cardinal holds P1[M]
provided
A1: for M being Cardinal st ( for N being Cardinal st N in M holds
P1[N] ) holds
P1[M]
proof end;

theorem Th44: :: CARD_1:46
proof end;

registration
coherence
for b1 being number st b1 = omega holds
b1 is cardinal
by Th44;
end;

theorem :: CARD_1:47

registration
coherence
proof end;
end;

registration
cluster -> finite for Element of omega ;
coherence
for b1 being Element of omega holds b1 is finite
by Th38;
end;

registration
existence
ex b1 being Cardinal st b1 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 ;
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
coherence
not omega is finite
proof end;
end;

registration
existence
ex b1 being set st b1 is infinite
proof end;
end;

registration
let X be infinite set ;
coherence
not card X is finite
proof end;
end;

theorem Th47: :: CARD_1:49
1 =
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 b1 being object st
( not b1 is zero & b1 is natural )
proof end;
existence
not for b1 being Nat holds b1 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 b1 being set st b1 is natural holds
b1 is finite
;
end;

:: from CARD_4, CARD_5 etc. 2008.02.21, A.T.
registration
let A be infinite set ;
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 b1 being Subset of X st b1 is infinite
proof end;
end;

:: from NECKLA_2, 2008.06.28, A.T.
registration
coherence
for b1 being number st b1 is finite & b1 is ordinal holds
b1 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 ;
coherence
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 b1 being set st b1 is N -element
proof end;
end;

registration
cluster 0 -element -> empty for set ;
coherence
for b1 being set st b1 is 0 -element holds
b1 is empty
;
cluster empty -> 0 -element for set ;
coherence
for b1 being set st b1 is empty holds
b1 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;
existence
ex b1 being Function st b1 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 b1 being set st b1 is 1 -element holds
( b1 is trivial & not b1 is empty )
proof end;
cluster non empty trivial -> 1 -element for set ;
coherence
for b1 being set st b1 is trivial & not b1 is empty holds
b1 is 1 -element
proof end;
end;

registration
let X be non empty set ;
cluster 1 -element for Element of bool X;
existence
ex b1 being Subset of X st b1 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 b1 being set st b1 is k -element holds
not b1 is empty
;
end;

registration
let k be natural Number ;
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 ;
coherence by ORDINAL3:8;
end;

registration
let c be Cardinal;
cluster cardinal for Element of bool c;
existence
ex b1 being Subset of c st b1 is cardinal
proof end;
end;