### The Mizar article:

### Cardinal Numbers

**by****Grzegorz Bancerek**

- Received September 19, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: CARD_1
- [ MML identifier index ]

environ vocabulary ORDINAL1, RELAT_1, FUNCT_1, BOOLE, WELLORD1, TARSKI, WELLORD2, ORDINAL2, FINSET_1, CARD_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, FUNCT_1, WELLORD1, ORDINAL1, ORDINAL2, WELLORD2, FINSET_1; constructors NAT_1, WELLORD1, WELLORD2, FINSET_1, XREAL_0, MEMBERED, XBOOLE_0; clusters FUNCT_1, ORDINAL1, FINSET_1, NAT_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions TARSKI, FUNCT_1, FINSET_1, ORDINAL2, WELLORD2, XBOOLE_0; theorems TARSKI, FUNCT_1, ZFMISC_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2, NAT_1, AXIOMS, REAL_1, RELAT_1, FINSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes ORDINAL1, ORDINAL2, FUNCT_1, NAT_1, FINSET_1, XBOOLE_0; begin reserve A,B,C for Ordinal, X,X1,Y,Y1,Z,a,b,b1,b2,x,y,z for set, R for Relation, f,g,h for Function, k,m,n for Nat; Lm1: A c= B implies succ A c= succ B proof assume A1: A c= B; let x; assume x in succ A; then A2: x in A or x = A by ORDINAL1:13; B in succ B by ORDINAL1:10; then (x in B or x in succ B) & B c= succ B by A1,A2,ORDINAL1:22,def 2; hence thesis; end; definition let IT be set; attr IT is cardinal means :Def1: ex B st IT = B & for A st A,B are_equipotent holds B c= A; end; definition cluster cardinal set; existence proof consider A; defpred P[Ordinal] means $1,A are_equipotent; A1: ex A st P[A]; consider B such that A2: P[B] & for C st P[C] holds B c= C from Ordinal_Min(A1); reconsider IT = B as set; take IT,B; thus IT = B; let C; assume C,B are_equipotent; then C,A are_equipotent by A2,WELLORD2:22; hence B c= C by A2; end; end; definition mode Cardinal is cardinal set; end; definition cluster cardinal -> ordinal set; coherence proof let M be set; assume M is cardinal; then ex B st M = B & for A st A,B are_equipotent holds B c= A by Def1; hence thesis; end; end; reserve M,N for Cardinal; canceled 3; theorem Th4: for X ex A st X,A are_equipotent proof let X; consider R such that A1: R well_orders X by WELLORD2:26; set Q = R|_2 X; A2: field Q = X & Q is well-ordering by A1,WELLORD2:25; take A = order_type_of Q; Q,RelIncl A are_isomorphic by A2,WELLORD2:def 2; then consider f such that A3: f is_isomorphism_of Q,RelIncl A by WELLORD1:def 8; A4: dom f = field Q & rng f = field RelIncl A & f is one-to-one & for a,b holds [a,b] in Q iff a in field Q & b in field Q & [f.a,f.b] in RelIncl A by A3,WELLORD1:def 7; take f; thus f is one-to-one & dom f = X & rng f = A by A1,A4,WELLORD2:25,def 1; end; definition let M,N; redefine pred M c= N; synonym M <=` N; pred M in N; synonym M <` N; end; canceled 3; theorem Th8: M = N iff M,N are_equipotent proof thus M = N implies M,N are_equipotent; consider A such that A1: M = A & for C st C,A are_equipotent holds A c= C by Def1; consider B such that A2: N = B & for C st C,B are_equipotent holds B c= C by Def1; assume A3: M,N are_equipotent; then A4: B c= A & N,M are_equipotent by A1,A2; A c= B by A1,A2,A3; hence thesis by A1,A2,A4,XBOOLE_0:def 10; end; canceled 4; theorem M <` N iff M <=` N & M <> N proof M c< N iff M c= N & M <> N by XBOOLE_0:def 8; hence thesis by ORDINAL1:21,def 2; end; theorem M <` N iff not N <=` M by ORDINAL1:7,26; definition let X; canceled 3; func Card X -> Cardinal means :Def5: X,it are_equipotent; existence proof defpred P[Ordinal] means $1,X are_equipotent; A1: ex A st P[A] by Th4; consider A such that A2: P[A] & for B st P[B] holds A c= B from Ordinal_Min(A1); A is cardinal proof take A; thus A = A; let B; assume B,A are_equipotent; then X,B are_equipotent by A2,WELLORD2:22; hence A c= B by A2; end; then reconsider M = A as Cardinal; take M; thus X,M are_equipotent by A2; end; uniqueness proof let M,N such that A3: X,M are_equipotent and A4: X,N are_equipotent; M,N are_equipotent by A3,A4,WELLORD2:22; hence thesis by Th8; end; end; canceled 6; theorem Th21: X,Y are_equipotent iff Card X = Card Y proof A1: X,Card X are_equipotent & Y,Card Y are_equipotent by Def5; thus X,Y are_equipotent implies Card X = Card Y proof assume X,Y are_equipotent; then Card X,Y are_equipotent by A1,WELLORD2:22; hence thesis by Def5; end; assume Card X = Card Y; hence X,Y are_equipotent by A1,WELLORD2:22; end; theorem Th22: R is well-ordering implies field R,order_type_of R are_equipotent proof assume R is well-ordering; then R,RelIncl order_type_of R are_isomorphic by WELLORD2:def 2; then consider f such that A1: f is_isomorphism_of R,RelIncl order_type_of R by WELLORD1:def 8; take f; field RelIncl order_type_of R = order_type_of R by WELLORD2:def 1; hence thesis by A1,WELLORD1:def 7; end; theorem Th23: X c= M implies Card X <=` M proof defpred P[Ordinal] means $1 c= M & X,$1 are_equipotent; reconsider m = M as Ordinal; assume X c= M; then A1: order_type_of RelIncl X c= m & RelIncl X is well-ordering & field RelIncl X = X by WELLORD2:9,17,def 1; then X,order_type_of RelIncl X are_equipotent by Th22; then A2: ex A st P[A] by A1; consider A such that A3: P[A] & for B st P[B] holds A c= B from Ordinal_Min(A2); A is cardinal proof take A; thus A = A; let B; assume B,A are_equipotent; then A4: X,B are_equipotent by A3,WELLORD2:22; assume A5: not A c= B; then m c= B by A3,A4; hence contradiction by A3,A5,XBOOLE_1:1; end; then reconsider A as Cardinal; Card X = A by A3,Def5; hence Card X c= M by A3; end; theorem Th24: Card A c= A proof A1: ex B st Card A = B & for C st C,B are_equipotent holds B c= C by Def1; A,Card A are_equipotent by Def5; hence thesis by A1; end; theorem X in M implies Card X <` M proof assume A1: X in M; then reconsider A = X as Ordinal by ORDINAL1:23; Card A c= A & Card X = Card A by Th24; hence Card X in M by A1,ORDINAL1:22; end; theorem Th26: Card X <=` Card Y iff ex f st f is one-to-one & dom f = X & rng f c= Y proof thus Card X <=` Card Y implies ex f st f is one-to-one & dom f = X & rng f c= Y proof assume A1: Card X c= Card Y; A2: X,Card X are_equipotent & Y,Card Y are_equipotent by Def5; then consider f such that A3: f is one-to-one & dom f = X & rng f = Card X by WELLORD2:def 4; consider g such that A4: g is one-to-one & dom g = Y & rng g = Card Y by A2,WELLORD2:def 4; take h = g"*f; g" is one-to-one by A4,FUNCT_1:62; hence h is one-to-one by A3,FUNCT_1:46; rng g = dom(g") & dom g = rng(g") by A4,FUNCT_1:55; hence dom h = X & rng h c= Y by A1,A3,A4,RELAT_1:45,46; end; given f such that A5: f is one-to-one & dom f = X & rng f c= Y; Y,Card Y are_equipotent by Def5; then consider g such that A6: g is one-to-one & dom g = Y & rng g = Card Y by WELLORD2:def 4; A7: X,rng(g*f) are_equipotent proof take g*f; thus g*f is one-to-one by A5,A6,FUNCT_1:46; thus dom(g*f) = X by A5,A6,RELAT_1:46; thus thesis; end; rng(g*f) c= Card Y by A6,RELAT_1:45; then A8: Card rng(g*f) <=` Card Y by Th23; X,Card X are_equipotent & rng(g*f),Card rng(g*f) are_equipotent by Def5; then Card X,X are_equipotent & X,Card rng(g*f) are_equipotent by A7,WELLORD2:22; then Card X,Card rng(g*f) are_equipotent by WELLORD2:22; hence Card X <=` Card Y by A8,Th8; end; theorem Th27: X c= Y implies Card X <=` Card Y proof assume A1: X c= Y; ex f st f is one-to-one & dom f = X & rng f c= Y proof take id X; thus thesis by A1,FUNCT_1:52,RELAT_1:71; end; hence thesis by Th26; end; theorem Card X <=` Card Y iff ex f st dom f = Y & X c= rng f proof thus Card X <=` Card Y implies ex f st dom f = Y & X c= rng f proof assume Card X <=` Card Y; then consider f such that A1: f is one-to-one & dom f = X & rng f c= Y by Th26; defpred P[set,set] means $1 in rng f & $2 = f".$1 or not $1 in rng f & $2 = 0; A2: for x st x in Y ex y st P[x,y] proof let x such that x in Y; not x in rng f implies thesis; hence thesis; end; A3: for x,y,z st x in Y & P[x,y] & P[x,z] holds y = z; consider g such that A4: dom g = Y & for y st y in Y holds P[y,g.y] from FuncEx(A3,A2); take g; thus dom g = Y by A4; let x; assume x in X; then A5: f".(f.x) = x & f.x in rng f by A1,FUNCT_1:56,def 5; then x = g.(f.x) by A1,A4; hence x in rng g by A1,A4,A5,FUNCT_1:def 5; end; given f such that A6: dom f = Y & X c= rng f; deffunc f(set) = f"{$1}; consider g such that A7: dom g = X & for x st x in X holds g.x = f(x) from Lambda; A8: X = {} implies thesis proof assume X = {}; then X c= Y by XBOOLE_1:2; hence thesis by Th27; end; X <> {} implies thesis proof assume X <> {}; then reconsider M = rng g as non empty set by A7,RELAT_1:65; for Z st Z in M holds Z <> {} proof let Z; assume Z in M; then consider x such that A9: x in dom g & Z = g.x by FUNCT_1:def 5; A10: Z = f"{x} & x in rng f by A6,A7,A9; consider y such that A11: y in dom f & x = f.y by A6,A7,A9,FUNCT_1:def 5; x in {x} by TARSKI:def 1; hence thesis by A10,A11,FUNCT_1:def 13; end; then consider F being Function such that A12: dom F = M & for Z st Z in M holds F.Z in Z by WELLORD2:28; A13: dom(F*g) = X by A7,A12,RELAT_1:46; A14: F*g is one-to-one proof let x,y; assume A15: x in dom(F*g) & y in dom(F*g) & (F*g).x = (F*g).y; then A16: g.x = f"{x} & g.y = f"{y} & (F*g).x = F.(g.x) & (F*g).y = F. (g.y) by A7,A13,FUNCT_1:23; then F.(f"{x}) = F.(f"{y}) & f"{x} in M & f"{y} in M by A7,A13,A15,FUNCT_1:def 5; then F.(f"{x}) in f"{x} & F.(f"{y}) in f"{y} by A12; then f.(F.(f"{x})) in {x} & f.(F.(f"{y})) in {y} by FUNCT_1:def 13; then f.(F.(f"{x})) = x & f.(F.(f"{y})) = y by TARSKI:def 1; hence thesis by A15,A16; end; rng(F*g) c= Y proof let x; assume x in rng(F*g); then consider y such that A17: y in dom(F*g) & x = (F*g).y by FUNCT_1:def 5; A18: g.y = f"{y} & x = F.(g.y) by A7,A13,A17,FUNCT_1:23; then f"{y} in M by A7,A13,A17,FUNCT_1:def 5; then x in f"{y} by A12,A18; hence x in Y by A6,FUNCT_1:def 13; end; hence thesis by A13,A14,Th26; end; hence thesis by A8; end; theorem Th29: not X,bool X are_equipotent proof given f such that A1: f is one-to-one & dom f = X & rng f = bool X; defpred P[set] means for Y st Y = f.$1 holds not $1 in Y; consider Z such that A2: a in Z iff a in X & P[a] from Separation; Z c= X proof let a; thus thesis by A2; end; then consider a such that A3: a in X & Z = f.a by A1,FUNCT_1:def 5; not a in Z by A2,A3; then ex Y st Y = f.a & a in Y by A2,A3; hence contradiction by A2,A3; end; theorem Th30: Card X <` Card bool X proof deffunc f(set) = {$1}; consider f such that A1: dom f = X & for x st x in X holds f.x = f(x) from Lambda; A2: f is one-to-one proof let x,y; assume A3: x in dom f & y in dom f & f.x = f.y; then f.x = { x } & f.y = { y } by A1; hence thesis by A3,ZFMISC_1:6; end; rng f c= bool X proof let x; assume x in rng f; then consider y such that A4: y in dom f & x = f.y by FUNCT_1:def 5; A5: f.y = { y } by A1,A4; { y } c= X proof let z; assume z in { y }; hence thesis by A1,A4,TARSKI:def 1; end; hence thesis by A4,A5; end; then A6: Card X <=` Card bool X by A1,A2,Th26; not X,bool X are_equipotent by Th29; then Card X <> Card bool X by Th21; then Card X c< Card bool X by A6,XBOOLE_0:def 8; hence thesis by ORDINAL1:21; end; definition let X; func nextcard X -> Cardinal means :Def6: Card X <` it & for M st Card X <` M holds it <=` M; existence proof defpred P[Ordinal] means ex M st $1 = M & Card X <` M; Card X <` Card bool X & Card bool X = Card bool X by Th30; then A1: ex A st P[A]; consider A such that A2: P[A] and A3: for B st P[B] holds A c= B from Ordinal_Min(A1); consider M such that A4: A = M & Card X <` M by A2; take M; thus Card X <` M by A4; let N; assume Card X <` N; hence M c= N by A3,A4; end; uniqueness proof let M1,M2 be Cardinal such that A5: Card X <` M1 & for M st Card X <` M holds M1 <=` M and A6: Card X <` M2 & for M st Card X <` M holds M2 <=` M; M1 <=` M2 & M2 <=` M1 by A5,A6; hence thesis by XBOOLE_0:def 10; end; end; canceled; theorem Th32: M <` nextcard M proof Card M <` nextcard M & M = Card M by Def5,Def6; hence thesis; end; theorem Card {} <` nextcard X proof {} c= X by XBOOLE_1:2; then Card {} <=` Card X & Card X <` nextcard X by Def6,Th27; hence thesis by ORDINAL1:22; end; theorem Th34: Card X = Card Y implies nextcard X = nextcard Y proof assume A1: Card X = Card Y; Card X <` nextcard X & for N st Card X <` N holds nextcard X <=` N by Def6; hence thesis by A1,Def6; end; theorem Th35: X,Y are_equipotent implies nextcard X = nextcard Y proof assume X,Y are_equipotent; then Card X = Card Y by Th21; hence thesis by Th34; end; theorem A in nextcard A proof assume not A in nextcard A; then nextcard A c= A & A,Card A are_equipotent by Def5,ORDINAL1:26; then Card nextcard A <=` Card A & Card nextcard A = nextcard A & nextcard Card A = nextcard A & Card A <` nextcard Card A by Def5,Th27,Th32,Th35; hence contradiction by ORDINAL1:7; end; reserve L,L1 for T-Sequence; definition let M; attr M is limit means :Def7: not ex N st M = nextcard N; synonym M is_limit_cardinal; end; definition let A; func alef A -> set means :Def8: ex L st it = last L & dom L = succ A & L.{} = Card NAT & (for B st succ B in succ A holds L.succ B = nextcard union { L.B }) & for B st B in succ A & B <> {} & B is_limit_ordinal holds L.B = Card sup(L|B); correctness proof deffunc C(Ordinal,set) = nextcard union {$2}; deffunc D(Ordinal,T-Sequence) = Card sup $2; set B = Card NAT; thus (ex x,L st x = last L & dom L = succ A & L.{} = B & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) & for x1,x2 being set st (ex L st x1 = last L & dom L = succ A & L.{} = B & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A & L.{} = B & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 from TS_Def; end; end; Lm2: now deffunc F(Ordinal) = alef $1; deffunc C(Ordinal,set) = nextcard union { $2 }; deffunc D(Ordinal,T-Sequence) = Card sup $2; A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.{} = Card NAT & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) by Def8; F({}) = Card NAT from TS_Result0(A1); hence alef 0 = Card NAT; thus for A holds F(succ A) = C(A,F(A)) from TS_ResultS(A1); thus A <> {} & A is_limit_ordinal implies for L st dom L = A & for B st B in A holds L.B = alef B holds alef A = Card sup L proof assume A2: A <> {} & A is_limit_ordinal; let L such that A3: dom L = A and A4: for B st B in A holds L.B = F(B); thus F(A) = D(A,L) from TS_ResultL(A1,A2,A3,A4); end; end; deffunc f(Ordinal) = alef $1; definition let A; cluster alef A -> cardinal; coherence proof A1: now given B such that A2: A = succ B; alef A = nextcard union {alef B} by A2,Lm2; hence thesis; end; now assume A3: A <> {} & for B holds A <> succ B; then A4: A is_limit_ordinal by ORDINAL1:42; consider L such that A5: dom L = A & for B st B in A holds L.B = f(B) from TS_Lambda; alef A = Card sup L by A3,A4,A5,Lm2; hence alef A is Cardinal; end; hence thesis by A1,Lm2; end; end; canceled; theorem alef 0 = Card NAT by Lm2; theorem Th39: alef succ A = nextcard alef A proof thus alef succ A = nextcard union { alef A } by Lm2 .= nextcard alef A by ZFMISC_1:31; end; theorem A <> {} & A is_limit_ordinal implies for L st dom L = A & for B st B in A holds L.B = alef B holds alef A = Card sup L by Lm2; theorem Th41: A in B iff alef A <` alef B proof defpred P[Ordinal] means for A st A in $1 holds alef A <` alef $1; A1: P[{}]; A2: for B st P[B] holds P[succ B] proof let B such that A3: P[B]; let A; assume A4: A in succ B; A5: alef succ B = nextcard alef B by Th39; A6: A c< B iff A c= B & A <> B by XBOOLE_0:def 8; now assume A in B; then alef A <` alef B & alef B <` nextcard alef B by A3,Th32; hence thesis by A5,ORDINAL1:19; end; hence thesis by A4,A5,A6,Th32,ORDINAL1:21,34; end; A7: for B st B <> {} & B is_limit_ordinal & for C st C in B holds P[C] holds P[B] proof let B such that A8: B <> {} & B is_limit_ordinal and for C st C in B for A st A in C holds alef A <` alef C; consider L such that A9: dom L = B and A10: for C st C in B holds L.C = f(C) from TS_Lambda; A11: alef B = Card sup L by A8,A9,A10,Lm2; let A; assume A in B; then succ A in B by A8,ORDINAL1:41; then L.succ A in rng L & L.succ A = alef succ A & alef succ A = alef succ A by A9,A10,FUNCT_1:def 5; then alef succ A in sup rng L & sup rng L = sup L by ORDINAL2:27,35; then alef succ A c= sup L & Card alef succ A = alef succ A by Def5,ORDINAL1:def 2; then A12: alef succ A <=` alef B by A11,Th27; alef succ A = nextcard alef A & alef A <` nextcard alef A by Th32,Th39; hence thesis by A12; end; A13: for B holds P[B] from Ordinal_Ind(A1,A2,A7); hence A in B implies alef A <` alef B; assume A14: alef A <` alef B; then A15: not B in A by A13; alef A <> alef B by A14; hence thesis by A15,ORDINAL1:24; end; theorem Th42: alef A = alef B implies A = B proof assume A1: alef A = alef B; A2: now assume A in B; then alef A <` alef B by Th41; hence contradiction by A1; end; now assume B in A; then alef B <` alef A by Th41; hence contradiction by A1; end; hence thesis by A2,ORDINAL1:24; end; theorem A c= B iff alef A <=` alef B proof (A c< B iff A <> B & A c= B) & (alef A c< alef B iff alef A <> alef B & alef A c= alef B) by XBOOLE_0:def 8; then (A in B iff alef A <` alef B) & (alef A = alef B implies A = B) & (alef A <=` alef B iff alef A = alef B or alef A <` alef B) & (A c= B iff A = B or A in B) by Th41,Th42,ORDINAL1:21,def 2; hence thesis; end; theorem X c= Y & Y c= Z & X,Z are_equipotent implies X,Y are_equipotent & Y,Z are_equipotent proof assume X c= Y & Y c= Z & X,Z are_equipotent; then Card X <=` Card Y & Card Y <=` Card Z & Card X = Card Z by Th21,Th27; then Card X = Card Y & Card Y = Card Z by XBOOLE_0:def 10; hence X,Y are_equipotent & Y,Z are_equipotent by Th21; end; theorem bool Y c= X implies Card Y <` Card X & not Y,X are_equipotent proof assume bool Y c= X; then Card Y <` Card bool Y & Card bool Y <=` Card X by Th27,Th30; hence Card Y <` Card X; then Card Y <> Card X; hence thesis by Th21; end; theorem X,{} are_equipotent iff X = {} proof thus X,{} are_equipotent implies X = {} proof given f such that A1: f is one-to-one & dom f = X & rng f = {}; thus thesis by A1,RELAT_1:65; end; thus thesis; end; theorem Card {} = {} proof {} is cardinal proof take {}; thus {} = {}; let A such that A,{} are_equipotent; thus thesis by XBOOLE_1:2; end; then reconsider M = {} as Cardinal; {},M are_equipotent; hence thesis by Def5; end; theorem Th48: X,{x} are_equipotent iff ex x st X = { x } proof thus X,{x} are_equipotent implies ex x st X = { x } proof assume X,{x} are_equipotent; then consider f such that A1: f is one-to-one & dom f = { x } & rng f = X by WELLORD2:def 4; rng f = { f.x } by A1,FUNCT_1:14; hence thesis by A1; end; given y such that A2: X = { y }; deffunc f(set) = x; consider f such that A3: dom f = X & for y st y in X holds f.y = f(y) from Lambda; take f; thus f is one-to-one proof let a,b; assume a in dom f & b in dom f & f.a = f.b; then a = y & b = y by A2,A3,TARSKI:def 1; hence thesis; end; thus dom f = X by A3; thus rng f c= { x } proof let a; assume a in rng f; then consider b such that A4: b in dom f & a = f.b by FUNCT_1:def 5; f.b = x by A3,A4; hence thesis by A4,TARSKI:def 1; end; let a; assume a in { x }; then A5: a = x & y in { y } by TARSKI:def 1; then f.y = x by A2,A3; hence a in rng f by A2,A3,A5,FUNCT_1:def 5; end; theorem Th49: Card X = Card { x } iff ex x st X = { x } proof (Card X = Card { x } iff X,{x} are_equipotent) & (X,{x} are_equipotent iff ex x st X = { x }) by Th21,Th48; hence thesis; end; theorem Card { x } = one proof A1: one = {} \/ { {} } by ORDINAL1:def 1,ORDINAL2:def 4 .= { {} }; one is cardinal proof take IT = one; thus one = IT; let A; assume A,IT are_equipotent; then consider y such that A2: A = { y } by A1,Th48; A3: y in A by A2,TARSKI:def 1; then reconsider y as Ordinal by ORDINAL1:23; y c= A by A3,ORDINAL1:def 2; then y = {} or y = A by A2,ZFMISC_1:39; hence IT c= A by A1,A2,A3; end; then reconsider M = one as Cardinal; { x },M are_equipotent by A1,Th48; hence thesis by Def5; end; theorem Th51: 0 = {}; theorem Th52: succ n = n + 1 proof A1: n = {k: k < n} & n+1 = {m: m < n+1} by AXIOMS:30; thus succ n c= n+1 proof let x; assume x in succ n; then A2: (x in n or x = n) & n < n+1 by NAT_1:38,ORDINAL1:13; now assume x in n; then consider k such that A3: x = k & k < n by A1; k < n+1 by A3,NAT_1:38; hence thesis by A1,A3; end; hence thesis by A1,A2; end; let x; assume x in n+1; then consider k such that A4: x = k & k < n+1 by A1; k <= n by A4,NAT_1:38; then k = n or k < n by REAL_1:def 5; then x = n or x in n by A1,A4; hence thesis by ORDINAL1:13; end; canceled; theorem A is natural implies ex n st n = A proof assume A in omega; hence thesis; end; canceled; theorem Th56: n <= m iff n c= m proof defpred P[Nat] means for m holds $1 <= m iff $1 c= m; A1: P[0] by NAT_1:18,XBOOLE_1:2; A2: for n st P[n] holds P[n+1] proof let n such that A3: P[n]; let m; thus n+1 <= m implies (n+1) c= m proof assume n+1 <= m; then consider k such that A4: m = n+1+k by NAT_1:28; n <= n+k by NAT_1:29; then n c= (n+k) by A3; then succ n c= succ (n+k) & (n+1) = succ n & (n+k+1) = succ (n+k) by Lm1,Th52; hence thesis by A4,XCMPLX_1:1; end; assume A5: (n+1) c= m; (n+1) = succ n by Th52; then n in m by A5,ORDINAL1:33; then n c= m & n <> m by ORDINAL1:def 2; then n <= m & n <> m by A3; then n < m by REAL_1:def 5; hence thesis by NAT_1:38; end; for n holds P[n] from Ind(A1,A2); hence thesis; end; canceled; theorem Th58: X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1 are_equipotent implies X \/ X1,Y \/ Y1 are_equipotent proof assume A1: X /\ X1 = {} & Y /\ Y1 = {}; given f such that A2: f is one-to-one & dom f = X & rng f = Y; given g such that A3: g is one-to-one & dom g = X1 & rng g = Y1; defpred P[set,set] means $1 in X & $2 = f.$1 or $1 in X1 & $2 = g.$1; A4: for x st x in X \/ X1 ex y st P[x,y] proof let x; assume x in X \/ X1; then x in X or x in X1 by XBOOLE_0:def 2; hence thesis; end; A5: for x,y,z st x in X \/ X1 & P[x,y] & P[x,z] holds y = z by A1,XBOOLE_0:def 3; consider h such that A6: dom h = X \/ X1 and A7: for x st x in X \/ X1 holds P[x,h.x] from FuncEx(A5,A4); take h; thus h is one-to-one proof let x,y; assume A8: x in dom h & y in dom h & h.x = h.y; then A9: (x in X & h.x = f.x or x in X1 & h.x = g.x) & (y in X & h.y = f.y or y in X1 & h.y = g.y) by A6,A7; A10: now assume x in X & y in X1; then not x in X1 & not y in X & f.x in Y & g.y in Y1 by A1,A2,A3,FUNCT_1:def 5,XBOOLE_0:def 3; hence contradiction by A1,A8,A9,XBOOLE_0:def 3; end; now assume y in X & x in X1; then not y in X1 & not x in X & f.y in Y & g.x in Y1 by A1,A2,A3,FUNCT_1:def 5,XBOOLE_0:def 3; hence contradiction by A1,A8,A9,XBOOLE_0:def 3; end; hence thesis by A2,A3,A8,A9,A10,FUNCT_1:def 8; end; thus dom h = X \/ X1 by A6; thus rng h c= Y \/ Y1 proof let x; assume x in rng h; then consider y such that A11: y in dom h & x = h.y by FUNCT_1:def 5; A12: y in X & x = f.y or y in X1 & x = g.y by A6,A7,A11; A13: now assume y in X; then x in Y by A1,A2,A12,FUNCT_1:def 5,XBOOLE_0:def 3; hence x in Y \/ Y1 by XBOOLE_0:def 2; end; now assume y in X1; then x in Y1 by A1,A3,A12,FUNCT_1:def 5,XBOOLE_0:def 3; hence x in Y \/ Y1 by XBOOLE_0:def 2; end; hence thesis by A6,A11,A13,XBOOLE_0:def 2; end; let x such that A14: x in Y \/ Y1; A15: now assume x in Y; then consider y such that A16: y in dom f & x = f.y by A2,FUNCT_1:def 5; A17: y in X \/ X1 by A2,A16,XBOOLE_0:def 2; then P[y,h.y] by A7; hence x in rng h by A1,A2,A6,A16,A17,FUNCT_1:def 5,XBOOLE_0:def 3; end; now assume x in Y1; then consider y such that A18: y in dom g & x = g.y by A3,FUNCT_1:def 5; A19: y in X \/ X1 by A3,A18,XBOOLE_0:def 2; then P[y,h.y] by A7; hence x in rng h by A1,A3,A6,A18,A19,FUNCT_1:def 5,XBOOLE_0:def 3; end; hence thesis by A14,A15,XBOOLE_0:def 2; end; theorem Th59: x in X & y in X implies X \ { x },X \ { y } are_equipotent proof assume A1: x in X & y in X; defpred P[set,set] means $1 = y & $2 = x or $1 <> y & $1 = $2; A2: for a st a in X \ { x } ex b st P[a,b] proof let a such that a in X \ { x }; a = y implies thesis; hence thesis; end; A3: for a,b1,b2 st a in X \ { x } & P[a,b1] & P[a,b2] holds b1 = b2; consider f such that A4: dom f = X \ { x } & for a st a in X \ { x } holds P[a,f.a] from FuncEx(A3, A2); take f; thus f is one-to-one proof let b1,b2; assume A5: b1 in dom f & b2 in dom f & f.b1 = f.b2 & b1 <> b2; then P[b1,f.b1] & P[b2,f.b2] & not b1 in { x } & not b2 in { x } by A4,XBOOLE_0:def 4; hence thesis by A5,TARSKI:def 1; end; thus dom f = X \ { x } by A4; thus rng f c= X \ { y } proof let z; assume z in rng f; then consider a such that A6: a in dom f & z = f.a by FUNCT_1:def 5; A7: now assume a = y; then not y in { x } & z = x by A4,A6,XBOOLE_0:def 4; then y <> z & z in X by A1,TARSKI:def 1; then not z in { y } & z in X by TARSKI:def 1; hence z in X \ { y } by XBOOLE_0:def 4; end; now assume a <> y; then not a in { y } & a = z & a in X by A4,A6,TARSKI:def 1,XBOOLE_0: def 4; hence z in X \ { y } by XBOOLE_0:def 4; end; hence thesis by A7; end; let z; assume z in X \ { y }; then A8: z in X & not z in { y } by XBOOLE_0:def 4; then A9: z <> y by TARSKI:def 1; A10: now assume A11: z = x; then not y in { x } by A9,TARSKI:def 1; then A12: y in dom f by A1,A4,XBOOLE_0:def 4; then z = f.y by A4,A11; hence z in rng f by A12,FUNCT_1:def 5; end; now assume z <> x; then not z in { x } by TARSKI:def 1; then A13: z in X \ { x } by A8,XBOOLE_0:def 4; then z = f.z by A4,A9; hence z in rng f by A4,A13,FUNCT_1:def 5; end; hence z in rng f by A10; end; theorem Th60: X c= dom f & f is one-to-one implies X,f.:X are_equipotent proof assume A1: X c= dom f & f is one-to-one; take g = f|X; thus g is one-to-one by A1,FUNCT_1:84; thus dom g = X by A1,RELAT_1:91; thus rng g = f.:X by RELAT_1:148; end; theorem Th61: X,Y are_equipotent & x in X & y in Y implies X \ { x },Y \ { y } are_equipotent proof given f such that A1: f is one-to-one & dom f = X & rng f = Y; assume A2: x in X & y in Y; X \ { x } c= X by XBOOLE_1:36; then A3: X \ { x },f.:(X \ { x }) are_equipotent by A1,Th60; A4: f.:(X \ { x }) = f.:X \ f.:{ x } by A1,FUNCT_1:123 .= Y \ f.:{ x } by A1,RELAT_1:146 .= Y \ { f.x } by A1,A2,FUNCT_1:117; f.x in Y by A1,A2,FUNCT_1:def 5; then Y \ { f.x },Y \ { y } are_equipotent by A2,Th59; hence thesis by A3,A4,WELLORD2:22; end; canceled 2; theorem Th64: n,m are_equipotent implies n = m proof defpred P[Nat] means ex n st n,$1 are_equipotent & n <> $1; assume n,m are_equipotent & n <> m; then A1: ex m st P[m]; consider m such that A2: P[m] and A3: for k st P[k] holds m <= k from Min(A1); consider n such that A4: n,m are_equipotent & n <> m by A2; consider f such that A5: f is one-to-one & dom f = n & rng f = m by A4,WELLORD2:def 4; m <> 0 by A4,A5,RELAT_1:65; then consider m1 being Nat such that A6: m = m1+1 by NAT_1:22; A7: not m1 in m1; A8: m1 \/ {m1} = succ m1 by ORDINAL1:def 1 .= m by A6,Th52; then A9: m \ {m1} = m1 \ {m1} by XBOOLE_1:40 .= m1 by A7,ZFMISC_1:65; n <> 0 by A4,A5,RELAT_1:65; then consider n1 being Nat such that A10: n = n1+1 by NAT_1:22; A11: not n1 in n1; A12: n1 \/ {n1} = succ n1 by ORDINAL1:def 1 .= n by A10,Th52; then A13: n \ {n1} = n1 \ {n1} by XBOOLE_1:40 .= n1 by A11,ZFMISC_1:65; n1 in {n1} & m1 in {m1} by TARSKI:def 1; then n1 in n & m1 in m by A8,A12,XBOOLE_0:def 2; then n1,m1 are_equipotent by A4,A9,A13,Th61; then m <= m1 by A3,A4,A6,A10; hence contradiction by A6,REAL_1:69; end; theorem Th65: x in omega implies x is cardinal proof assume that A1: x in omega and A2: for B st x = B ex C st C,B are_equipotent & not B c= C; reconsider A = x as Ordinal by A1,ORDINAL1:23; consider B such that A3: B,A are_equipotent & not A c= B by A2; B in A by A3,ORDINAL1:26; then B in omega by A1,ORDINAL1:19; hence contradiction by A1,A3,Th64; end; definition cluster -> cardinal Nat; correctness by Th65; end; theorem Th66: for n being Nat holds n = Card n by Def5; canceled; theorem X,Y are_equipotent & X is finite implies Y is finite proof assume X,Y are_equipotent; then consider f such that A1: f is one-to-one & dom f = X & rng f = Y by WELLORD2:def 4; given p being Function such that A2: rng p = X and A3: dom p in omega; take f*p; thus rng(f*p) = Y by A1,A2,RELAT_1:47; thus dom(f*p) in omega by A1,A2,A3,RELAT_1:46; end; theorem Th69: n is finite & Card n is finite proof thus n is finite proof rng id n = n & dom id n = n by RELAT_1:71; hence thesis by FINSET_1:def 1; end; hence thesis by Th66; end; canceled; theorem Th71: Card n = Card m implies n = m proof assume A1: Card n = Card m; Card n = n & Card m = m by Th66; hence thesis by A1; end; theorem Th72: Card n <=` Card m iff n <= m proof (Card n <=` Card m iff Card n c= Card m) & Card n = n & Card m = m & ( n c= m iff n <= m) by Th56,Th66; hence thesis; end; theorem Th73: Card n <` Card m iff n < m proof Card n c< Card m iff Card n c= Card m & Card n <> Card m by XBOOLE_0:def 8; then (Card n <=` Card m & Card n <> Card m iff Card n <` Card m) & (Card n = Card m iff n = m) & (n <= m & n <> m iff n < m) & (Card n <=` Card m iff n <= m) by Th71,Th72,ORDINAL1:21,def 2,REAL_1:def 5; hence thesis; end; theorem Th74: X is finite implies ex n st X,n are_equipotent proof defpred P[set] means ex n st $1,n are_equipotent; assume A1: X is finite; A2: P[{}] by Th51; A3: for Z,Y st Z in X & Y c= X & P[Y] holds P[Y \/ {Z}] proof let Z,Y such that Z in X & Y c= X; given n such that A4: Y,n are_equipotent; A5: Z in Y implies thesis proof assume Z in Y; then A6: { Z } c= Y by ZFMISC_1:37; take n; thus thesis by A4,A6,XBOOLE_1:12; end; not Z in Y implies thesis proof assume A7: not Z in Y; take m = n+1; A8: m = succ n by Th52 .= n \/ { n } by ORDINAL1:def 1; A9: { Z },{ n } are_equipotent by Th48; A10: now assume n meets { n }; then consider x being set such that A11: x in n & x in { n } by XBOOLE_0:3; x = n by A11,TARSKI:def 1; hence contradiction by A11; end; now consider x being Element of Y /\ { Z }; assume Y /\ { Z } <> {}; then x in Y & x in { Z } by XBOOLE_0:def 3; hence contradiction by A7,TARSKI:def 1; end; then Y misses { Z } by XBOOLE_0:def 7; hence thesis by A4,A8,A9,A10,Th58; end; hence thesis by A5; end; thus P[X] from Finite(A1,A2,A3); end; canceled; theorem Th76: nextcard Card n = Card(n+1) proof n < n+1 & Card Card n = Card n by Def5,NAT_1:38; then A1: Card Card n <` Card(n+1) by Th73; for M st Card Card n <` M holds Card(n+1) <=` M proof let M such that A2: Card Card n in M; Card n = n & M = M by Th66; then succ n c= M & (n+1) = succ n & Card(n+1) = (n+1) by A2,Def5,Th52,ORDINAL1:33; hence Card(n+1) c= M; end; hence thesis by A1,Def6; end; definition let X be finite set; redefine canceled 2; func Card X -> Nat means Card it = Card X; coherence proof consider n such that A1: X,n are_equipotent by Th74; n = Card n by Th66 .= Card X by A1,Th21; hence thesis; end; compatibility by Def5; synonym card X; end; canceled; theorem card {} = 0 by Def5; theorem card { x } = 1 proof { k : k < 1} = { 0 } proof thus { k : k < 1} c= { 0 } proof let x; assume x in { k : k < 1}; then consider k such that A1: x = k and A2: k < 1; k < 0 + 1 by A2; then k <= 0 by NAT_1:38; then k = 0 by NAT_1:19; hence x in { 0 } by A1,TARSKI:def 1; end; let x; assume x in { 0 }; then x = 0 by TARSKI:def 1; hence thesis; end; then 1 = { 0 } by AXIOMS:30; then Card 1 = Card { x } by Th49; hence thesis by Def5; end; theorem for X,Y being finite set holds X c= Y implies card X <= card Y proof let X,Y be finite set; assume X c= Y; then Card X <=` Card Y & Card card X = Card X & Card card Y = Card Y & Card card X = card X & Card card Y = card Y by Def5,Th27; hence card X <= card Y by Th56; end; theorem for X,Y being finite set holds X,Y are_equipotent implies card X = card Y by Th21; theorem X is finite implies nextcard X is finite proof assume X is finite; then reconsider X as finite set; Card X = Card card X & X,Card X are_equipotent by Def5; then Card((card X)+1) = nextcard Card X & nextcard Card X = nextcard X by Th35,Th76; hence thesis by Th69; end; scheme Cardinal_Ind { Sigma[set] }: for M holds Sigma[M] provided A1: Sigma[{}] and A2: for M st Sigma[M] holds Sigma[nextcard M] and A3: for M st M <> {} & M is_limit_cardinal & for N st N <` M holds Sigma[N] holds Sigma[M] proof defpred P[Ordinal] means $1 is Cardinal implies Sigma[$1]; A4: for A st for B st B in A holds P[B] holds P[A] proof let A such that A5: for B st B in A holds P[B] and A6: A is Cardinal; reconsider M = A as Cardinal by A6; A7: now assume not M is_limit_cardinal; then consider N such that A8: M = nextcard N by Def7; N in M & N = N by A8,Th32; then Sigma[ N] by A5; hence Sigma[M] by A2,A8; end; now assume A9: M <> {} & M is_limit_cardinal; for N st N <` M holds Sigma[N] by A5; hence Sigma[M] by A3,A9; end; hence Sigma[A] by A1,A7; end; A10: for A holds P[A] from Transfinite_Ind(A4); let M; thus thesis by A10; end; scheme Cardinal_CompInd { Sigma[set] }: for M holds Sigma[M] provided A1: for M st for N st N <` M holds Sigma[N] holds Sigma[M] proof defpred P[Ordinal] means $1 is Cardinal implies Sigma[$1]; A2: for A st for B st B in A holds P[B] holds P[A] proof let A such that A3: for B st B in A holds B is Cardinal implies Sigma[B]; assume A is Cardinal; then reconsider M = A as Cardinal; for N st N <` M holds Sigma[N] by A3; hence Sigma[A] by A1; end; A4: for A holds P[A] from Transfinite_Ind(A2); let M; thus thesis by A4; end; theorem Th83: alef 0 = omega proof thus alef 0 c= omega by Lm2,Th24; thus omega c= alef 0 proof let x; assume A1: x in omega; then reconsider A = x as Ordinal by ORDINAL1:23; consider n such that A2: A = n by A1; A3: succ n c= omega & (n+1) = succ n by Th52,ORDINAL1:33; then Card (n+1) c= Card omega & n in succ n & Card (n+1) = (n+1) by Def5,Th27,ORDINAL1:10; hence x in alef 0 by A2,A3,Lm2; end; end; theorem Card omega = omega by Lm2,Th83; theorem Card omega is_limit_cardinal proof given N such that A1: Card omega = nextcard N; A2: N in omega by A1,Lm2,Th32,Th83; then A3: succ N in omega & N is natural by ORDINAL1:41,ORDINAL2:19,def 21; consider n such that A4: N = n by A2; nextcard Card n = Card(n+1) & Card n = n & Card(n+1) = (n+1) & (n+1) = succ n & N = N by Th52,Th66,Th76; hence contradiction by A1,A3,A4,Lm2,Th83; end; definition cluster -> finite Nat; coherence by Th69; end; definition cluster finite Cardinal; existence proof consider n being Nat; take n; thus thesis; end; end; theorem for M being finite Cardinal ex n st M = Card n proof let M be finite Cardinal; Card M = M & Card M = Card card M by Def5; hence thesis; end; definition let X be finite set; cluster Card X -> finite; coherence; end;

Back to top