Copyright (c) 1990 Association of Mizar Users
environ vocabulary ORDINAL1, CARD_1, FUNCT_1, RELAT_1, BOOLE, TARSKI, FUNCT_2, MCART_1, ORDINAL2, ORDINAL3, FUNCOP_1, FINSET_1, FINSEQ_1, ARYTM_1, CARD_2; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, MCART_1, ORDINAL2, ORDINAL3, WELLORD2, REAL_1, NAT_1, FINSEQ_1, CARD_1, FINSET_1, FUNCOP_1; constructors DOMAIN_1, ORDINAL3, WELLORD2, REAL_1, NAT_1, FINSEQ_1, FUNCOP_1, XREAL_0, XBOOLE_0; clusters SUBSET_1, ORDINAL1, CARD_1, FINSEQ_1, FINSET_1, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0; theorems TARSKI, ENUMSET1, FUNCT_1, FUNCT_2, MCART_1, ORDINAL1, ORDINAL2, WELLORD2, ORDINAL3, CARD_1, REAL_1, NAT_1, FINSEQ_1, FINSET_1, ZFMISC_1, RLVECT_1, FUNCT_5, AXIOMS, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1, FUNCT_1, FINSET_1, PARTFUN1; begin reserve A,B for Ordinal, K,M,N for Cardinal, x,x1,x2,y,y1,y2,z,u,X,Y,Z,X1,X2,Y1,Y2 for set, f,g for Function; canceled; theorem Th2: Card X <=` Card Y iff ex f st X c= f.:Y proof thus Card X <=` Card Y implies ex f st X c= f.:Y proof assume Card X <=` Card Y; then consider f such that A1: dom f = Y & X c= rng f by CARD_1:28; take f; thus X c= f.:Y by A1,RELAT_1:146; end; given f such that A2: X c= f.:Y; deffunc F(set) = f.$1; deffunc G(set) = $1; defpred C[set] means $1 in dom f; consider g such that A3: dom g = Y & for x st x in Y holds (C[x] implies g.x = F(x)) & (not C[x] implies g.x = G(x)) from LambdaC; X c= rng g proof let x; assume x in X; then consider y such that A4: y in dom f & y in Y & x = f.y by A2,FUNCT_1:def 12; y in dom g & x = g.y by A3,A4; hence thesis by FUNCT_1:def 5; end; hence thesis by A3,CARD_1:28; end; theorem Card (f.:X) <=` Card X by Th2; theorem Card X <` Card Y implies Y \ X <> {} proof assume A1: Card X <` Card Y & Y \ X = {}; then Y c= X by XBOOLE_1:37; then Card Y <=` Card X by CARD_1:27; hence contradiction by A1,CARD_1:14; end; theorem Th5: x in X & X,Y are_equipotent implies Y <> {} & ex x st x in Y proof assume A1: x in X; given f such that A2: f is one-to-one & dom f = X & rng f = Y; f.x in Y by A1,A2,FUNCT_1:def 5; hence Y <> {}; take f.x; thus thesis by A1,A2,FUNCT_1:def 5; end; theorem bool X,bool Card X are_equipotent & Card bool X = Card bool Card X proof X,Card X are_equipotent by CARD_1:def 5; then consider f such that A1: f is one-to-one & dom f = X & rng f = Card X by WELLORD2:def 4; deffunc g(set) = f.:$1; consider g such that A2: dom g = bool X & for x st x in bool X holds g.x = g(x) from Lambda; thus bool X,bool Card X are_equipotent proof take g; thus g is one-to-one proof let x,y; assume A3: x in dom g & y in dom g & g.x = g.y; then A4: x = x & y = y & g.x = f.:x & g.y = f.:y by A2; A5: x c= y proof let z; assume A6: z in x; then f.z in f.:x by A1,A2,A3,FUNCT_1:def 12; then ex u st u in dom f & u in y & f.z = f.u by A3,A4,FUNCT_1:def 12; hence thesis by A1,A2,A3,A6,FUNCT_1:def 8; end; y c= x proof let z; assume A7: z in y; then f.z in f.:y by A1,A2,A3,FUNCT_1:def 12; then ex u st u in dom f & u in x & f.z = f.u by A3,A4,FUNCT_1:def 12; hence thesis by A1,A2,A3,A7,FUNCT_1:def 8; end; hence thesis by A5,XBOOLE_0:def 10; end; thus dom g = bool X by A2; thus rng g c= bool Card X proof let x; assume x in rng g; then consider y such that A8: y in dom g & x = g.y by FUNCT_1:def 5; g.y = f.:y & f.:y c= rng f by A2,A8,RELAT_1:144; hence thesis by A1,A8; end; let x; assume x in bool Card X; then A9: x c= Card X & f"x c= dom f by RELAT_1:167; then f.:(f"x) = x & f"x in bool X & f"x = f"x by A1,FUNCT_1:147; then g.(f"x) = x & x = x by A2; hence x in rng g by A1,A2,A9,FUNCT_1:def 5; end; hence thesis by CARD_1:21; end; deffunc g(set) = $1`1; theorem Z in Funcs(X,Y) implies Z,X are_equipotent & Card Z = Card X proof assume Z in Funcs(X,Y); then consider f such that A1: Z = f & dom f = X & rng f c= Y by FUNCT_2:def 2; thus Z,X are_equipotent proof consider g such that A2: dom g = Z & for x st x in Z holds g.x = g(x) from Lambda; take g; thus g is one-to-one proof let x,y; assume A3: x in dom g & y in dom g; then (ex x1,x2 being set st [x1,x2] = x) & (ex x1,x2 being set st [x1,x2] = y) by A1,A2,RELAT_1:def 1; then A4: x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:8; then x`1 in dom f & y`1 in dom f & x`2 = f.(x`1) & y`2 = f.(y`1) & g.x = x`1 & g.y = y`1 by A1,A2,A3,FUNCT_1:8; hence thesis by A4; end; thus dom g = Z by A2; thus rng g c= X proof let x; assume x in rng g; then consider y such that A5: y in dom g & x = g.y by FUNCT_1:def 5; ex x1,x2 being set st [x1,x2] = y by A1,A2,A5,RELAT_1:def 1; then x = y`1 & y = [y`1,y`2] by A2,A5,MCART_1:8; hence x in X by A1,A2,A5,FUNCT_1:8; end; let x; assume x in X; then A6: [x,f.x] in Z by A1,FUNCT_1:def 4; then g.[x,f.x] = [x,f.x]`1 by A2 .= x by MCART_1:7; hence x in rng g by A2,A6,FUNCT_1:def 5; end; hence Card Z = Card X by CARD_1:21; end; OLambdaC{A()->set,C[set],F,G(set)->set}: ex f being Function st dom f = A() & for x being Ordinal st x in A() holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) proof defpred P[set,set] means (C[$1] implies $2 = F($1)) & (not C[$1] implies $2 = G($1)); A1: for x,y1,y2 being set st x in A() & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x being set st x in A() ex y st P[x,y] proof let x be set; not C[x] implies ex y st (C[x] implies y = F(x)) & (not C[x] implies y = G(x)); hence thesis; end; consider f being Function such that A3: dom f = A() & for x being set st x in A() holds P[x,f.x] from FuncEx(A1,A2); take f; thus thesis by A3; end; Lm1: x1 <> x2 implies A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & Card(A+^B) = Card([:A,{x1}:] \/ [:B,{x2}:]) proof assume A1: x1 <> x2; defpred C[set] means $1 in A; deffunc F(set) = [$1,x1]; deffunc G(Ordinal) = [$1-^A,x2]; consider f such that A2: dom f = A+^B and A3: for x being Ordinal holds x in A+^B implies (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) from OLambdaC; thus A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent proof take f; thus f is one-to-one proof let x,y; assume A4: x in dom f & y in dom f & f.x = f.y; then reconsider C1 = x, C2 = y as Ordinal by A2,ORDINAL1:23; A5: x = C1 & y = C2; now per cases; suppose x in A & y in A; then f.C1 = [x,x1] & f.C2 = [y,x1] & [x,x1]`1 = C1 by A2,A3,A4,MCART_1:7; hence thesis by A4,MCART_1:7; suppose not x in A & not y in A; then f.x = [C1-^A,x2] & f.y = [C2-^A,x2] & [C1-^A,x2]`1 = C1-^A & [C2-^A,x2]`1 = C2-^A & A c= C1 & A c= C2 by A2,A3,A4,MCART_1:7,ORDINAL1:26; then C1-^A = C2-^A & C1 = A+^(C1-^A) & C2 = A+^(C2-^A) by A4,ORDINAL3:def 6; hence thesis; suppose x in A & not y in A; then f.x = [x,x1] & f.y = [C2-^A,x2] & [x,x1]`2 = x1 & x1 <> x2 by A1,A2,A3,A4,A5,MCART_1:7; hence thesis by A4,MCART_1:7; suppose not x in A & y in A; then f.y = [y,x1] & f.x = [C1-^A,x2] & [y,x1]`2 = x1 & x1 <> x2 by A1,A2,A3,A4,A5,MCART_1:7; hence thesis by A4,MCART_1:7; end; hence thesis; end; thus dom f = A+^B by A2; thus rng f c= [:A,{x1}:] \/ [:B,{x2}:] proof let x; assume x in rng f; then consider y such that A6: y in dom f & x = f.y by FUNCT_1:def 5; A7: x1 in {x1} & x2 in {x2} by TARSKI:def 1; reconsider C = y as Ordinal by A2,A6,ORDINAL1:23; now per cases; suppose y in A; then x = [C,x1] & [C,x1] in [:A,{x1}:] by A2,A3,A6,A7,ZFMISC_1:106 ; hence thesis by XBOOLE_0:def 2; suppose not y in A; then A8: x = [C-^A,x2] & A c= C by A2,A3,A6,ORDINAL1:26; then A+^(C-^A) = C by ORDINAL3:def 6; then C-^A in B by A2,A6,ORDINAL3:25; then [C-^A,x2] in [:B,{x2}:] by A7,ZFMISC_1:106; hence thesis by A8,XBOOLE_0:def 2; end; hence thesis; end; let x such that A9: x in [:A,{x1}:] \/ [:B,{x2}:]; A10: now assume x in [:A,{x1}:]; then consider y,z such that A11: y in A & z in {x1} & x = [y,z] by ZFMISC_1:103; A12: y is Ordinal by A11,ORDINAL1:23; A13: A c= A+^B by ORDINAL3:27; then y in A+^B & z = x1 by A11,TARSKI:def 1; then x = f.y by A3,A11,A12; hence thesis by A2,A11,A13,FUNCT_1:def 5; end; now assume x in [:B,{x2}:]; then consider y,z such that A14: y in B & z in {x2} & x = [y,z] by ZFMISC_1:103; reconsider y as Ordinal by A14,ORDINAL1:23; A c= A+^y by ORDINAL3:27; then A15: (A+^y) = A+^y & A+^y in A+^B & not A+^y in A & A+^y-^A = y & z = x2 by A14,ORDINAL1:7,ORDINAL2:49,ORDINAL3:65,TARSKI:def 1; then x = f.(A+^y) by A3,A14; hence thesis by A2,A15,FUNCT_1:def 5; end; hence thesis by A9,A10,XBOOLE_0:def 2; end; hence thesis by CARD_1:21; end; deffunc plus(set,set) = [:$1,{0}:] \/ [:$2,{1}:]; Lm2: [:X,Y:],[:Y,X:] are_equipotent & Card [:X,Y:] = Card [:Y,X:] proof deffunc f(set) = [$1`2,$1`1]; consider f such that A1: dom f = [:X,Y:] & for x st x in [:X,Y:] holds f.x = f(x) from Lambda; thus [:X,Y:],[:Y,X:] are_equipotent proof take f; thus f is one-to-one proof let x,y; assume x in dom f & y in dom f; then A2: x = [x`1,x`2] & y = [y`1,y`2] & f.x = [x`2,x`1] & f.y = [y`2,y`1] by A1,MCART_1:23; assume f.x = f.y; then x`1 = y`1 & x`2 = y`2 by A2,ZFMISC_1:33; hence x = y by A2; end; thus dom f = [:X,Y:] by A1; thus rng f c= [:Y,X:] proof let x; assume x in rng f; then consider y such that A3: y in dom f & x = f.y by FUNCT_1:def 5; x = [y`2,y`1] & y`1 in X & y`2 in Y by A1,A3,MCART_1:10; hence thesis by ZFMISC_1:106; end; let x; assume x in [:Y,X:]; then A4: x = [x`1,x`2] & x`1 in Y & x`2 in X by MCART_1:10,23; then [x`2,x`1] in [:X,Y:] & [x`2,x`1]`1 = x`2 & [x`2,x`1]`2 = x`1 by MCART_1:7,ZFMISC_1:106; then f.[x`2,x`1] in rng f & f.[x`2,x`1] = x by A1,A4,FUNCT_1:def 5; hence thesis; end; hence thesis by CARD_1:21; end; definition let M,N; func M +` N -> Cardinal equals :Def1: Card( M +^ N); correctness; commutativity proof let C be Cardinal; let M,N; assume C = Card( M +^ N); hence C = Card plus( N, M) by Lm1 .= Card( N +^ M) by Lm1; end; func M *` N -> Cardinal equals :Def2: Card [:M,N:]; correctness; commutativity by Lm2; func exp(M,N) -> Cardinal equals :Def3: Card Funcs(N,M); correctness; end; canceled 3; theorem [:X,Y:],[:Y,X:] are_equipotent & Card [:X,Y:] = Card [:Y,X:] by Lm2; theorem Th12: [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & Card [:[:X,Y:],Z:] = Card [:X,[:Y,Z:]:] proof deffunc f(set) = [$1`1`1,[$1`1`2,$1`2]]; consider f such that A1: dom f = [:[:X,Y:],Z:] & for x st x in [:[:X,Y:],Z:] holds f.x = f(x) from Lambda; thus [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent proof take f; thus f is one-to-one proof let x,y; assume x in dom f & y in dom f; then A2: x = [x`1,x`2] & y = [y`1,y`2] & x`1 in [:X,Y:] & y`1 in [:X,Y:] & f.x = [x`1`1,[x`1`2,x`2]] & f.y = [y`1`1,[y`1`2,y`2]] by A1,MCART_1:10,23; assume f.x = f.y; then A3: x`1`1 = y`1`1 & [x`1`2,x`2] = [y`1`2,y`2] & x`1 = [x`1`1,x`1`2] & y`1 = [y`1`1,y`1`2] by A2,MCART_1:23,ZFMISC_1:33; then x`1`2 = y`1`2 & x`2 = y`2 by ZFMISC_1:33; hence thesis by A2,A3; end; thus dom f = [:[:X,Y:],Z:] by A1; thus rng f c= [:X,[:Y,Z:]:] 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: y = [y`1,y`2] & y`1 in [:X,Y:] & y`2 in Z by A1,A4,MCART_1:10,23; then A6: y`1 = [y`1`1,y`1`2] & y`1`1 in X & y`1`2 in Y & x = [y`1`1,[y`1`2,y`2]] by A1,A4,MCART_1:10,23; then [y`1`2,y`2] in [:Y,Z:] by A5,ZFMISC_1:106; hence thesis by A6,ZFMISC_1:106; end; let x; assume x in [:X,[:Y,Z:]:]; then A7: x = [x`1,x`2] & x`1 in X & x`2 in [:Y,Z:] by MCART_1:10,23; then A8: x`2 = [x`2`1,x`2`2] & x`2`1 in Y & x`2`2 in Z by MCART_1:10,23; then A9: [x`1,x`2`1] in [:X,Y:] & [x`1,x`2`1]`1 = x`1 & [x`1,x`2`1]`2 = x`2 `1 by A7,MCART_1:7,ZFMISC_1:106; then A10: [[x`1,x`2`1],x`2`2] in [:[:X,Y:],Z:] & [[x`1,x`2`1],x`2`2]`1 = [x`1,x`2`1] & [[x`1,x`2`1],x`2`2]`2 = x`2`2 by A8,MCART_1:7,ZFMISC_1:106; then x = f.[[x`1,x`2`1],x`2`2] by A1,A7,A8,A9; hence thesis by A1,A10,FUNCT_1:def 5; end; hence thesis by CARD_1:21; end; theorem Th13: X,[:X,{x}:] are_equipotent & Card X = Card [:X,{x}:] proof deffunc f(set) = [$1,x]; consider f such that A1: dom f = X & for y st y in X holds f.y = f(y) from Lambda; thus X,[:X,{x}:] are_equipotent proof take f; thus f is one-to-one proof let y,z; assume A2: y in dom f & z in dom f & f.y = f.z; then f.y = [y,x] & f.z = [z,x] & [y,x]`1 = y by A1,MCART_1:7; hence thesis by A2,MCART_1:7; end; thus dom f = X by A1; thus rng f c= [:X,{x}:] proof let y; assume y in rng f; then consider z such that A3: z in dom f & y = f.z by FUNCT_1:def 5; y = [z,x] & x in {x} by A1,A3,TARSKI:def 1; hence thesis by A1,A3,ZFMISC_1:106; end; let y; assume y in [:X,{x}:]; then consider y1,y2 being set such that A4: y1 in X & y2 in {x} & y = [y1,y2] by ZFMISC_1:103; y2 = x by A4,TARSKI:def 1; then y = f.y1 by A1,A4; hence thesis by A1,A4,FUNCT_1:def 5; end; hence thesis by CARD_1:21; end; Lm3: [:X,Y:],[:Card X,Y:] are_equipotent proof X,Card X are_equipotent by CARD_1:def 5; then consider f such that A1: f is one-to-one & dom f = X & rng f = Card X by WELLORD2:def 4; deffunc g(set) = [f.$1`1,$1`2]; consider g such that A2: dom g = [:X,Y:] & for x st x in [:X,Y:] holds g.x = g(x) from Lambda; take g; thus g is one-to-one proof let x,y; assume x in dom g & y in dom g; then A3: x = [x`1,x`2] & y = [y`1,y`2] & g.x = [f.x`1,x`2] & g.y = [f.y`1,y`2] & x`1 in X & y`1 in X by A2,MCART_1:10,23; assume g.x = g.y; then f.x`1 = f.y`1 & x`2 = y`2 by A3,ZFMISC_1:33; hence thesis by A1,A3,FUNCT_1:def 8; end; thus dom g = [:X,Y:] by A2; thus rng g c= [:Card X,Y:] proof let y; assume y in rng g; then consider x such that A4: x in dom g & y = g.x by FUNCT_1:def 5; x`1 in X by A2,A4,MCART_1:10; then y = [f.x`1,x`2] & f.x`1 in Card X & x`2 in Y by A1,A2,A4,FUNCT_1:def 5,MCART_1:10; hence thesis by ZFMISC_1:106; end; let y; assume y in [:Card X,Y:]; then A5: y`1 in Card X & y`2 in Y & y = [y`1,y`2] by MCART_1:10,23; then consider x such that A6: x in X & y`1 = f.x by A1,FUNCT_1:def 5; A7: [x,y`2] in [:X,Y:] & [x,y`2]`1 = x & [x,y`2]`2 = y`2 by A5,A6,MCART_1:7,ZFMISC_1:106; then g.[x,y`2] = y by A2,A5,A6; hence y in rng g by A2,A7,FUNCT_1:def 5; end; theorem Th14: [:X,Y:],[:Card X,Y:] are_equipotent & [:X,Y:],[:X,Card Y:] are_equipotent & [:X,Y:],[:Card X,Card Y:] are_equipotent & Card [:X,Y:] = Card [:Card X,Y:] & Card [:X,Y:] = Card [:X,Card Y:] & Card [:X,Y:] = Card [:Card X,Card Y:] proof [:Y,X:],[:Card Y,X:] are_equipotent & [:X,Y:],[:Y,X:] are_equipotent by Lm2,Lm3; then [:X,Y:],[:Card Y,X:] are_equipotent & [:Card Y,X:],[:X,Card Y:] are_equipotent by Lm2,WELLORD2:22; hence A1: [:X,Y:],[:Card X,Y:] are_equipotent & [:X,Y:],[:X,Card Y:] are_equipotent by Lm3,WELLORD2:22; [:X,Card Y:],[:Card X,Card Y:] are_equipotent by Lm3; hence [:X,Y:],[:Card X,Card Y:] are_equipotent by A1,WELLORD2:22; hence thesis by A1,CARD_1:21; end; theorem Th15: X1,Y1 are_equipotent & X2,Y2 are_equipotent implies [:X1,X2:],[:Y1,Y2:] are_equipotent & Card [:X1,X2:] = Card [:Y1,Y2:] proof assume X1,Y1 are_equipotent & X2,Y2 are_equipotent; then [:X1,X2:],[:Card X1,Card X2:] are_equipotent & [:Y1,Y2:],[:Card Y1,Card Y2:] are_equipotent & Card X1 = Card Y1 & Card X2 = Card Y2 by Th14,CARD_1:21; hence [:X1,X2:],[:Y1,Y2:] are_equipotent by WELLORD2:22; hence thesis by CARD_1:21; end; theorem x1 <> x2 implies A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & Card(A+^B) = Card([:A,{x1}:] \/ [:B,{x2}:]) by Lm1; theorem Th17: x1 <> x2 implies K+`M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K+`M = Card([:K,{x1}:] \/ [:M,{x2}:]) proof assume x1 <> x2; then Card([:K,{x1}:] \/ [:M,{x2}:]) = Card( K +^ M) by Lm1 .= K+`M by Def1; hence thesis by CARD_1:def 5; end; theorem Th18: A*^B,[:A,B:] are_equipotent & Card(A*^B) = Card [:A,B:] proof defpred P[set,set] means ex O1, O2 being Ordinal st O1 = $1`1 & O2 = $1`2 & $2 = O1*^B+^O2; A1: for x,y1,y2 st x in [:A,B:] & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x st x in [:A,B:] ex y st P[x,y] proof let x; assume x in [:A,B:]; then x = [x`1,x`2] & x`1 in A & x`2 in B by MCART_1:10,23; then reconsider x1 = x`1, x2 = x`2 as Ordinal by ORDINAL1:23; take x1*^B+^x2; take x1, x2; thus thesis; end; consider f such that A3: dom f = [:A,B:] & for x st x in [:A,B:] holds P[x,f.x] from FuncEx(A1, A2); A4: [:A,B:],A*^B are_equipotent proof take f; thus f is one-to-one proof let x,y; assume A5: x in dom f & y in dom f; then A6: x = [x`1,x`2] & y = [y`1,y`2] & x`1 in A & x`2 in B & y`1 in A & y`2 in B by A3,MCART_1:10,23; then reconsider x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2 as Ordinal by ORDINAL1:23; consider O1, O2 being Ordinal such that A7: O1 = x`1 & O2 = x`2 & f.x = O1*^B+^O2 by A3,A5; consider O3, O4 being Ordinal such that A8: O3 = y`1 & O4 = y`2 & f.y = O3*^B+^O4 by A3,A5; assume f.x = f.y; then x1 = y1 & x2 = y2 by A6,A7,A8,ORDINAL3:56; hence x = y by A6; end; thus dom f = [:A,B:] by A3; thus rng f c= A*^B proof let y; assume y in rng f; then consider x such that A9: x in dom f & y = f.x by FUNCT_1:def 5; A10: x`1 in A & x`2 in B by A3,A9,MCART_1:10; consider x1, x2 being Ordinal such that A11: x1 = x`1 & x2 = x`2 & f.x = x1*^B+^x2 by A3,A9; y = x1*^B+^x2 & one*^B = B & x1+^one = succ x1 by A9,A11,ORDINAL2:48,56; then A12: y in x1*^B+^one*^B & x1*^B+^one*^B = (succ x1)*^B & succ x1 c= A by A10,A11,ORDINAL1:33,ORDINAL2:49,ORDINAL3:54; then x1*^B+^one*^B c= A*^B by ORDINAL2:58; hence thesis by A12; end; let y; assume A13: y in A*^B; then reconsider C = y as Ordinal by ORDINAL1:23; A14: C = (C div^ B)*^B+^(C mod^ B) & C div^ B in A & C mod^ B in B by A13,ORDINAL3:78,80; then A15: [C div^ B,C mod^ B] in [:A,B:] & [C div^ B,C mod^ B]`1 = C div^ B & [C div^ B,C mod^ B]`2 = C mod^ B & (C div^ B) = C div^ B & C mod^ B = C mod^ B by MCART_1:7,ZFMISC_1:106; then consider O1, O2 being Ordinal such that A16: O1 = [C div^ B,C mod^ B]`1 & O2 = [C div^ B,C mod^ B]`2 & f.[C div^ B,C mod^ B] = O1*^B+^O2 by A3; thus thesis by A3,A14,A15,A16,FUNCT_1:def 5; end; hence A*^B,[:A,B:] are_equipotent; thus thesis by A4,CARD_1:21; end; deffunc plus(set,set) = [:$1,{0}:] \/ [:$2,{1}:]; deffunc plus(set,set,set,set) = [:$1,{$3}:] \/ [:$2,{$4}:]; Lm4: 2 = {{},one} proof 2 = succ (0+1) .= succ one by ORDINAL2:def 4; hence 2 = {{}} \/ {one} by ORDINAL1:def 1,ORDINAL3:18 .= {{},one} by ENUMSET1:41; end; theorem 0 = Card {} & 1 = Card one & 2 = Card succ one proof thus 0 = Card {} by CARD_1:47; thus 1 = Card one by CARD_1:79,ORDINAL3:18; thus 2 = Card {{},one} by Lm4,CARD_1:def 5 .= Card(one \/ {one}) by ENUMSET1:41,ORDINAL3:18 .= Card succ one by ORDINAL1:def 1; end; theorem Th20: 1 = one proof thus 1 = Card {{}} by CARD_1:79 .= one by CARD_1:50; end; canceled; theorem Th22: 2 = {{},one} & 2 = succ one proof A1: 2 = succ (0+1) .= succ one by ORDINAL2:def 4; thus 2 = {{},one} by Lm4; thus thesis by A1; end; theorem Th23: X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 implies [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & Card ([:X1,{x1}:] \/ [:X2,{x2}:]) = Card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) proof assume A1: X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2; {x1},{y1} are_equipotent & {x2},{y2} are_equipotent by CARD_1:48; then A2: [:X1,{x1}:],[:Y1,{y1}:] are_equipotent & [:X2,{x2}:],[:Y2,{y2}:] are_equipotent by A1,Th15; A3: now assume [:X1,{x1}:] meets [:X2,{x2}:]; then consider x being set such that A4: x in [:X1,{x1}:] & x in [:X2,{x2}:] by XBOOLE_0:3; x`2 in {x1} & x`2 in {x2} by A4,MCART_1:10; then x`2 = x1 & x`2 = x2 by TARSKI:def 1; hence contradiction by A1; end; now assume [:Y1,{y1}:] meets [:Y2,{y2}:]; then consider y being set such that A5: y in [:Y1,{y1}:] & y in [:Y2,{y2}:] by XBOOLE_0:3; y`2 in {y1} & y`2 in {y2} by A5,MCART_1:10; then y`2 = y1 & y`2 = y2 by TARSKI:def 1; hence contradiction by A1; end; hence [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent by A2,A3,CARD_1:58; hence thesis by CARD_1:21; end; theorem Th24: Card(A+^B) = Card A +` Card B proof A1: Card A +^ Card B,plus( Card A, Card B) are_equipotent & A+^B,plus(A,B) are_equipotent by Lm1; A,Card A are_equipotent & B,Card B are_equipotent & Card A = Card A & Card B = Card B & 0 <> 1 by CARD_1:def 5; then plus( Card A, Card B),Card A +^ Card B are_equipotent & plus(A,B),plus( Card A, Card B) are_equipotent by Lm1,Th23; then plus(A,B),Card A +^ Card B are_equipotent by WELLORD2:22; then Card A +` Card B = Card( Card A +^ Card B) & A+^B,Card A +^ Card B are_equipotent by A1,Def1,WELLORD2:22; hence thesis by CARD_1:21; end; theorem Th25: Card(A*^B) = Card A *` Card B proof thus Card (A*^B) = Card [:A,B:] by Th18 .= Card [:Card A,Card B:] by Th14 .= Card A *` Card B by Def2; end; theorem [:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent & Card([:X,{0}:] \/ [:Y,{1}:]) = Card([:Y,{0}:] \/ [:X,{1}:]) by Th23; theorem Th27: [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & Card ([:X1,X2:] \/ [:Y1,Y2:]) = Card ([:X2,X1:] \/ [:Y2,Y1:]) proof deffunc f(set) = [$1`2,$1`1]; consider f such that A1: dom f = [:X1,X2:] \/ [:Y1,Y2:] & for x st x in [:X1,X2:] \/ [:Y1,Y2:] holds f.x = f(x) from Lambda; thus [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent proof take f; thus f is one-to-one proof let x1,x2; assume A2: x1 in dom f & x2 in dom f & f.x1 = f.x2; then (x1 in [:X1,X2:] or x1 in [:Y1,Y2:]) & f.x1 = [x1`2,x1`1] & (x2 in [:X1,X2:] or x2 in [:Y1,Y2:]) & f.x2 = [x2`2,x2`1] by A1,XBOOLE_0:def 2; then x1 = [x1`1,x1`2] & x2 = [x2`1,x2`2] & x1`1 = x2`1 & x1`2 = x2`2 by A2,MCART_1:23,ZFMISC_1:33; hence x1 = x2; end; thus dom f = [:X1,X2:] \/ [:Y1,Y2:] by A1; thus rng f c= [:X2,X1:] \/ [:Y2,Y1:] proof let x; assume x in rng f; then consider y such that A3: y in dom f & x = f.y by FUNCT_1:def 5; y in [:X1,X2:] or y in [:Y1,Y2:] by A1,A3,XBOOLE_0:def 2; then (y`1 in X1 & y`2 in X2 or y`1 in Y1 & y`2 in Y2)& x = [y`2,y`1] by A1,A3,MCART_1:10; then x in [:X2,X1:] or x in [:Y2,Y1:] by ZFMISC_1:106; hence thesis by XBOOLE_0:def 2; end; let x; assume x in [:X2,X1:] \/ [:Y2,Y1:]; then x in [:X2,X1:] or x in [:Y2,Y1:] by XBOOLE_0:def 2; then A4: (x`1 in X2 & x`2 in X1 or x`1 in Y2 & x`2 in Y1) & x = [x`1,x`2] by MCART_1:10,23; then [x`2,x`1] in [:X1,X2:] or [x`2,x`1] in [:Y1,Y2:] by ZFMISC_1:106; then A5: [x`2,x`1] in [:X1,X2:] \/ [:Y1,Y2:] & [x`2,x`1]`1 = x`2 & [x`2,x`1]`2 = x`1 by MCART_1:7,XBOOLE_0:def 2; then f.[x`2,x`1] = x by A1,A4; hence thesis by A1,A5,FUNCT_1:def 5; end; hence thesis by CARD_1:21; end; theorem Th28: x <> y implies Card X +` Card Y = Card([:X,{x}:] \/ [:Y,{y}:]) proof assume A1: x <> y; X,Card X are_equipotent & Y,Card Y are_equipotent & 0 <> 1 by CARD_1:def 5; then A2: Card plus(X,Y,x,y) = Card plus(Card X,Card Y,x,y) by A1,Th23; thus Card X +` Card Y = Card( Card X +^ Card Y) by Def1 .= Card([:X,{x}:] \/ [:Y,{y}:]) by A1,A2,Lm1; end; theorem M+`0 = M proof A1: [:{},{1}:] = {} & [:{},{0}:] = {} by ZFMISC_1:113; thus M+`0 = Card( M +^ {}) by Def1 .= Card plus(M,{}) by Lm1 .= Card M by A1,Th13 .= M by CARD_1:def 5; end; Lm5: x <> y implies [:X,{x}:] misses [:Y,{y}:] proof assume A1: x <> y; assume not thesis; then consider z being set such that A2: z in [:X,{x}:] & z in [:Y,{y}:] by XBOOLE_0:3; z`2 = x & z`2 = y by A2,MCART_1:13; hence contradiction by A1; end; canceled; theorem Th31: (K+`M)+`N = K+`(M+`N) proof A1: K+`M+`N,[:K+`M,{0}:] \/ [:N,{2}:] are_equipotent & K+`M,[:K,{0}:] \/ [:M,{1}:] are_equipotent & K+`(M+`N),[:K,{0}:] \/ [:M+`N,{2}:] are_equipotent & M+`N,[:M,{1}:] \/ [:N,{2}:] are_equipotent & K+`M,[:K+`M,{0}:] are_equipotent & M+`N,[:M+`N,{2}:] are_equipotent by Th13,Th17; A2: [:K+`M,{0}:] misses [:N,{2}:] by Lm5; [:K,{0}:] misses [:N,{2}:] & [:M,{1}:] misses [:N,{2}:] by Lm5; then [:K,{0}:] /\ [:N,{2}:] = {} & [:M,{1}:] /\ [:N,{2}:] = {} by XBOOLE_0:def 7; then ([:K,{0}:] \/ [:M,{1}:]) /\ [:N,{2}:] = {} \/ {} by XBOOLE_1:23 .= {} ; then A3: ([:K,{0}:] \/ [:M,{1}:]) misses [:N,{2}:] by XBOOLE_0:def 7; [:K+`M,{0}:],[:K,{0}:] \/ [:M,{1}:] are_equipotent & [:N,{2}:],[:N,{2}:] are_equipotent by A1,WELLORD2:22; then A4: [:K+`M,{0}:] \/ [:N,{2}:], [:K,{0}:] \/ [:M,{1}:] \/ [:N,{2}:] are_equipotent by A2,A3,CARD_1:58; A5: [:K,{0}:] misses [:M+`N,{2}:] by Lm5; [:K,{0}:] misses [:M,{1}:] & [:K,{0}:] misses [:N,{2}:] by Lm5; then [:K,{0}:] /\ [:M,{1}:] = {} & [:K,{0}:] /\ [:N,{2}:] = {} by XBOOLE_0:def 7; then [:K,{0}:] /\ ([:M,{1}:] \/ [:N,{2}:]) = {} \/ {} by XBOOLE_1:23 .= {} ; then A6: [:K,{0}:] misses ([:M,{1}:] \/ [:N,{2}:]) by XBOOLE_0:def 7; [:M+`N,{2}:],[:M,{1}:] \/ [:N,{2}:] are_equipotent & [:K,{0}:],[:K,{0}:] are_equipotent by A1,WELLORD2:22; then [:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]),[:K,{0}:] \/ [:M+`N,{2}:] are_equipotent & [:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]) = [:K,{0}:] \/ [:M,{1}:] \/ [:N,{2}:] by A5,A6,CARD_1:58,XBOOLE_1:4; then [:K+`M,{0}:] \/ [:N,{2}:],[:K,{0}:] \/ [:M+`N,{2}:] are_equipotent by A4,WELLORD2:22; then K+`M+`N,[:K,{0}:] \/ [:M+`N,{2}:] are_equipotent & [:K,{0}:] \/ [:M+`N,{2}:],K+`(M+`N) are_equipotent by A1,WELLORD2:22; then K+`M+`N,K+`(M+`N) are_equipotent & Card(K+`M+`N) = K+`M+`N by CARD_1:def 5,WELLORD2:22; hence thesis by CARD_1:def 5; end; theorem K*`0 = 0 proof K*`0 = Card [:K,0:] & [:K,{}:] = {} & [:{},K:] = {} by Def2,ZFMISC_1:113; hence thesis by CARD_1:47; end; theorem K*`1 = K proof K = Card K by CARD_1:def 5; then K*`1 = Card [:K,1:] & K = Card [:K,{{}}:] & Card [:K,{{}}:] = Card [:{{}},K:] by Def2,Lm2,Th13; hence thesis by Th20,ORDINAL3:18; end; canceled; theorem Th35: (K*`M)*`N = K*`(M*`N) proof thus (K*`M)*`N = Card [:K*`M,N:] by Def2 .= Card [:Card [:K,M:],N:] by Def2 .= Card [:[:K,M:],N:] by Th14 .= Card [:K,[:M,N:]:] by Th12 .= Card [:K,Card [:M,N:]:] by Th14 .= Card [:K,M*`N:] by Def2 .= K*`(M*`N) by Def2; end; theorem Th36: 2*`K = K+`K proof thus 2*`K = Card [:2,K:] by Def2 .= Card([:{{}},K:] \/ [:{one},K:]) by Th22,ZFMISC_1:132 .= Card([:K,{{}}:] \/ [:K,{one}:]) by Th27 .= Card K +` Card K by Th28 .= K +` Card K by CARD_1:def 5 .= K +` K by CARD_1:def 5; end; theorem Th37: K*`(M+`N) = K*`M +` K*`N proof A1: K*`(M+`N) = K*`Card plus(M,N) by Th17 .= Card [:K,Card plus(M,N):] by Def2 .= Card [:K,plus(M,N):] by Th14 .= Card ([:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:]) by ZFMISC_1:120; M,[:M,{0}:] are_equipotent & N,[:N,{1}:] are_equipotent & K,K are_equipotent & [:K,M:],[:[:K,M:],{0}:] are_equipotent & [:K,N:],[:[:K,N:],{1}:] are_equipotent by Th13; then [:K,M:],[:K,[:M,{0}:]:] are_equipotent & [:K,N:],[:K,[:N,{1}:]:] are_equipotent & [:[:K,M:],{0}:],[:K,M:] are_equipotent & [:[:K,N:],{1}:],[:K,N:] are_equipotent & 0 <> 1 & [:[:K,M:],{0}:],[:Card [:K,M:],{0}:] are_equipotent & [:[:K,N:],{1}:],[:Card [:K,N:],{1}:] are_equipotent by Th14,Th15; then [:[:K,M:],{0}:],[:K,[:M,{0}:]:] are_equipotent & [:[:K,N:],{1}:],[:K,[:N,{1}:]:] are_equipotent & [:Card [:K,M:],{0}:],[:[:K,M:],{0}:] are_equipotent & [:M,{0}:] misses [:N,{1}:] & [:Card [:K,N:],{1}:],[:[:K,N:],{1}:] are_equipotent by Lm5,WELLORD2:22; then [:Card [:K,M:],{0}:],[:K,[:M,{0}:]:] are_equipotent & [:Card [:K,N:],{1}:],[:K,[:N,{1}:]:] are_equipotent & [:Card [:K,M:],{0}:] misses [:Card [:K,N:],{1}:] & [:K,[:M,{0}:]:] misses [:K,[:N,{1}:]:] by Lm5,WELLORD2:22,ZFMISC_1:127; then [:Card [:K,M:],{0}:] \/ [:Card [:K,N:],{1}:], [:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:] are_equipotent by CARD_1:58; hence K*`(M+`N) = Card([:Card [:K,M:],{0}:] \/ [:Card [:K,N:],{1}:]) by A1,CARD_1:21 .= Card [:K,M:] +` Card [:K,N:] by Th17 .= K*`M +` Card [:K,N:] by Def2 .= K*`M +` K*`N by Def2; end; theorem exp(K,0) = 1 proof thus exp(K,0) = Card Funcs({},K) by Def3 .= Card {{}} by FUNCT_5:64 .= 1 by Th20,CARD_1:50; end; theorem K <> 0 implies exp(0,K) = 0 proof assume K <> 0; then Funcs(K,0) = {} by FUNCT_2:14; hence exp(0,K) = 0 by Def3,CARD_1:47; end; theorem exp(K,1) = K & exp(1,K) = 1 proof thus exp(K,1) = Card Funcs(one,K) by Def3,Th20 .= Card K by FUNCT_5:65,ORDINAL3:18 .= K by CARD_1:def 5; thus exp(1,K) = Card Funcs(K,one) by Def3,Th20 .= Card {K --> {}} by FUNCT_5:66,ORDINAL3:18 .= 1 by Th20,CARD_1:50; end; theorem exp(K,M+`N) = exp(K,M)*`exp(K,N) proof A1: M+`N,[:M,{0}:] \/ [:N,{1}:] are_equipotent & [:M,{0}:] misses [:N,{1}:] & K,K are_equipotent by Th17,ZFMISC_1:131; [:M,{0}:],M are_equipotent & [:N,{1}:],N are_equipotent by Th13; then A2: Funcs([:M,{0}:],K),Funcs(M,K) are_equipotent & Funcs([:N,{1}:],K),Funcs(N,K) are_equipotent by FUNCT_5:67; thus exp(K,M+`N) = Card Funcs(M+`N,K) by Def3 .= Card Funcs([:M,{0}:] \/ [:N,{1}:],K) by A1,FUNCT_5:67 .= Card [:Funcs([:M,{0}:],K),Funcs([:N,{1}:],K):] by A1,FUNCT_5:69 .= Card [:Funcs(M,K),Funcs(N,K):] by A2,Th15 .= Card [:Card Funcs(M,K),Card Funcs(N,K):] by Th14 .= (Card Funcs(M,K))*`Card Funcs(N,K) by Def2 .= exp(K,M)*`Card Funcs(N,K) by Def3 .= exp(K,M)*`exp(K,N) by Def3; end; theorem exp(K*`M,N) = exp(K,N)*`exp(M,N) proof A1: Card(K*`M) = K*`M & K*`M = Card [:K,M:] & Card N = Card N by Def2,CARD_1:def 5; thus exp(K*`M,N) = Card Funcs(N,K*`M) by Def3 .= Card Funcs(N,[:K,M:]) by A1,FUNCT_5:68 .= Card [:Funcs(N,K),Funcs(N,M):] by FUNCT_5:71 .= Card [:Card Funcs(N,K),Card Funcs(N,M):] by Th14 .= (Card Funcs(N,K))*`Card Funcs(N,M) by Def2 .= (Card Funcs(N,K))*`exp(M,N) by Def3 .= exp(K,N)*`exp(M,N) by Def3; end; theorem exp(K,M*`N) = exp(exp(K,M),N) proof M*`N = Card [:M,N:] by Def2; then [:M,N:],M*`N are_equipotent & [:N,M:],[:M,N:] are_equipotent by Lm2,CARD_1:def 5; then A1: [:N,M:],M*`N are_equipotent & K,K are_equipotent by WELLORD2:22; A2: Funcs(M,K),Card Funcs(M,K) are_equipotent & N,N are_equipotent by CARD_1:def 5; thus exp(K,M*`N) = Card Funcs(M*`N,K) by Def3 .= Card Funcs([:N,M:],K) by A1,FUNCT_5:67 .= Card Funcs(N,Funcs(M,K)) by FUNCT_5:70 .= Card Funcs(N,Card Funcs(M,K)) by A2,FUNCT_5:67 .= Card Funcs(N,exp(K,M)) by Def3 .= exp(exp(K,M),N) by Def3; end; theorem exp(2,Card X) = Card bool X proof A1: Card Card X = Card X & Card 2 = Card {{},one} by Th22,CARD_1:def 5; thus exp(2,Card X) = Card Funcs(Card X,2) by Def3 .= Card Funcs(X,{{},one}) by A1,FUNCT_5:68 .= Card bool X by FUNCT_5:72; end; theorem Th45: exp(K,2) = K*`K proof thus exp(K,2) = Card Funcs(2,K) by Def3 .= Card [:K,K:] by Th22,FUNCT_5:73 .= K*`K by Def2; end; theorem exp(K+`M,2) = K*`K +` 2*`K*`M +` M*`M proof thus exp(K+`M,2) = (K+`M)*`(K+`M) by Th45 .= K*`(K+`M) +` M*`(K+`M) by Th37 .= K*`K +` K*`M +` M*`(K+`M) by Th37 .= K*`K +` K*`M +` (M*`K +` M*`M) by Th37 .= K*`K +` K*`M +` K*`M +` M*`M by Th31 .= K*`K +` (K*`M +` K*`M) +` M*`M by Th31 .= K*`K +` 2*`(K*`M) +` M*`M by Th36 .= K*`K +` 2*`K*`M +` M*`M by Th35; end; theorem Th47: Card(X \/ Y) <=` Card X +` Card Y proof consider f such that A1: dom f = plus(X,Y) & for x st x in plus(X,Y) holds f.x = g(x) from Lambda; X \/ Y c= rng f proof let x; assume x in X \/ Y; then A2: x in X or x in Y by XBOOLE_0:def 2; now per cases; suppose x in X; then [x,0] in [:X,{0}:] by ZFMISC_1:129; then A3: [x,0] in plus(X,Y) & [x,0]`1 = x by MCART_1:7,XBOOLE_0:def 2; then x = f.[x,0] by A1; hence thesis by A1,A3,FUNCT_1:def 5; suppose not x in X; then [x,1] in [:Y,{1}:] by A2,ZFMISC_1:129; then A4: [x,1] in plus(X,Y) & [x,1]`1 = x by MCART_1:7,XBOOLE_0:def 2; then x = f.[x,1] by A1; hence thesis by A1,A4,FUNCT_1:def 5; end; hence thesis; end; then Card(X \/ Y) <=` Card plus(X,Y) & 0 <> 1 by A1,CARD_1:28; hence thesis by Th28; end; theorem Th48: X misses Y implies Card (X \/ Y) = Card X +` Card Y proof assume A1: X misses Y; X,[:X,{0}:] are_equipotent & [:X,{0}:],[:Card X,{0}:] are_equipotent & Y,[:Y,{1}:] are_equipotent & [:Y,{1}:],[:Card Y,{1}:] are_equipotent by Th13,Th14; then [:Card X,{0}:] misses [:Card Y,{1}:] & X,[:Card X,{0}:] are_equipotent & Y,[:Card Y,{1}:] are_equipotent by Lm5,WELLORD2:22; then X \/ Y,[:Card X,{0}:] \/ [:Card Y,{1}:] are_equipotent by A1,CARD_1:58 ; hence Card (X \/ Y) = Card ([:Card X,{0}:] \/ [:Card Y,{1}:]) by CARD_1:21 .= Card X +` Card Y by Th17; end; reserve m,n for Nat; theorem Th49: n+m = n +^ m proof defpred P[Nat] means n+$1 = n +^ $1; A1: P[0] by ORDINAL2:44; A2: for m st P[m] holds P[m+1] proof let m such that A3: P[m]; thus n+(m+1) = n+m+1 by XCMPLX_1:1 .= succ( n +^ m) by A3,CARD_1:52 .= n +^ succ m by ORDINAL2:45 .= n +^ (m+1) by CARD_1:52; end; for m holds P[m] from Ind(A1,A2); hence thesis; end; theorem Th50: n*m = n *^ m proof defpred P[Nat] means $1*m = $1 *^ m; A1: P[0] by ORDINAL2:52; A2: for n st P[n] holds P[n+1] proof let n such that A3: P[n]; thus (n+1)*m = n*m+1*m by XCMPLX_1:8 .= n *^ m +^ m by A3,Th49 .= n *^ m +^ one *^ m by ORDINAL2:56 .= ( n +^ one) *^ m by ORDINAL3:54 .= (succ n) *^ m by ORDINAL2:48 .= (n+1) *^ m by CARD_1:52; end; for n holds P[n] from Ind(A1,A2); hence thesis; end; theorem Th51: Card(n+m) = Card n +` Card m proof thus Card(n+m) = Card( n +^ m) by Th49 .= Card n +` Card m by Th24; end; theorem Th52: Card(n*m) = Card n *` Card m proof thus Card(n*m) = Card( n *^ m) by Th50 .= Card n *` Card m by Th25; end; theorem Th53: for X,Y being finite set st X misses Y holds card (X \/ Y) = card X + card Y proof let X,Y be finite set; assume A1: X misses Y; Card card (X \/ Y) = Card (X \/ Y) by CARD_1:def 11 .= Card X +` Card Y by A1,Th48 .= Card card X +` Card Y by CARD_1:def 11 .= Card card X +` Card card Y by CARD_1:def 11 .= Card (card X + card Y) by Th51; hence thesis by CARD_1:71; end; theorem Th54: for X being finite set st not x in X holds card (X \/ {x}) = card X + 1 proof let X be finite set; assume not x in X; then X misses {x} & card {x} = 1 & {x} is finite by CARD_1:79,ZFMISC_1:56; hence card (X \/ {x}) = card X + 1 by Th53; end; canceled 2; theorem for X,Y being finite set holds (Card X <=` Card Y iff card X <= card Y) proof let X,Y be finite set; Card card X = Card X & Card card Y = Card Y by CARD_1:def 11; hence thesis by CARD_1:72; end; theorem Th58: for X,Y being finite set holds Card X <` Card Y iff card X < card Y proof let X,Y be finite set; Card card X = Card X & Card card Y = Card Y by CARD_1:def 11; hence thesis by CARD_1:73; end; theorem Th59: for X being set st Card X = 0 holds X = {} proof let X be set; assume Card X = 0; then X,{} are_equipotent by CARD_1:21,78; hence thesis by CARD_1:46; end; theorem for X being set holds Card X = 1 iff ex x st X = {x} proof let X be set; Card {0} = 1 & {0} is finite by CARD_1:79; hence Card X = 1 implies ex x st X = {x} by CARD_1:49; given x such that A1: X = {x}; thus thesis by A1,CARD_1:79; end; theorem Th61: for X being finite set holds X,card X are_equipotent & X,Card card X are_equipotent & X,Seg card X are_equipotent proof let X be finite set; Card card X = Card X by CARD_1:def 11; then X,Card card X are_equipotent & Card Seg card X = Card X by CARD_1:def 5,FINSEQ_1:76; hence thesis by CARD_1:21,def 5; end; theorem Th62: for X,Y being finite set holds card(X \/ Y) <= card X + card Y proof let X,Y be finite set; A1: Card card(X \/ Y) = Card(X \/ Y) by CARD_1:def 11; Card X = Card card X & Card Y = Card card Y by CARD_1:def 11; then Card X +` Card Y = Card(card X + card Y) by Th51; then Card (X \/ Y) <=` Card(card X + card Y) by Th47; hence card(X \/ Y) <= card X + card Y by A1,CARD_1:72; end; theorem Th63: for X,Y being finite set st Y c= X holds card (X \ Y) = card X - card Y proof let X,Y be finite set; assume A1: Y c= X; A2: Y is finite; defpred P[set] means ex S being finite set st S = $1 & card (X \ S) = card X - card S; card X - 0 = card X & X \ {} = X; then A3: P[{}] by CARD_1:78; A4: for X1,Z being set st X1 in Y & Z c= Y & P[Z] holds P[Z \/ {X1}] proof let X1,Z be set such that A5: X1 in Y & Z c= Y & P[Z] & not P[Z \/ {X1}]; now assume X1 in Z; then {X1} c= Z by ZFMISC_1:37; then Z = Z \/ {X1} by XBOOLE_1:12; hence P[Z \/ {X1}] by A5; end; then A6: X \ Z is finite & not X1 in Z & X1 in X & Z is finite & card {X1} = 1 by A1,A5,CARD_1:79; reconsider Z1 = Z as finite set by A5; A7: X1 in X \ Z & X \ Z,Seg card (X \ Z) are_equipotent & card Z1 + card {X1} = card (Z1 \/ {X1}) by A6,Th54,Th61,XBOOLE_0:def 4 ; then Seg card (X \ Z) <> {} by Th5; then consider m such that A8: card (X \ Z) = m+1 by FINSEQ_1:4,NAT_1:22; m+1 in Seg(m+1) & Seg m = Seg (m+1) \ {m+1} & m+1-1 = m+(1-1) & X \ (Z \/ {X1}) = X \ Z \ {X1} & m+0 = m by FINSEQ_1:6,RLVECT_1:104,XBOOLE_1:41,XCMPLX_1:29; then X \ (Z \/ {X1}),Seg m are_equipotent & X \ (Z \/ {X1}) is finite & (m+1)-1 = m & card {X1} = 1 & card Seg m = m by A7,A8,CARD_1:61,79,FINSEQ_1:78; then card (X \ (Z \/ {X1})) = card(X \ Z)-card{X1} by A8,CARD_1:81 .= card X - card (Z1 \/ {X1}) by A5,A7,XCMPLX_1:36; hence contradiction by A5; end; P[Y] from Finite(A2,A3,A4); hence thesis; end; theorem for X,Y being finite set holds card (X \/ Y) = card X + card Y - card (X /\ Y) proof let X,Y be finite set; Y \ X is finite & X misses (Y \ X) by XBOOLE_1:79; then A1: card (X \/ (Y \ X)) = card X + card (Y \ X) by Th53; Y \ X = Y \ X /\ Y & X /\ Y c= Y by XBOOLE_1:17,47; then card (Y \ X) = card Y - card (X /\ Y) & X \/ (Y \ X) = X \/ Y by Th63,XBOOLE_1:39; hence thesis by A1,XCMPLX_1:29; end; theorem for X,Y being finite set holds card [:X,Y:] = card X * card Y proof let X,Y be finite set; Card card [:X,Y:] = Card [:X,Y:] by CARD_1:def 11 .= Card [:Card X,Card Y:] by Th14 .= Card X *` Card Y by Def2 .= Card card X *` Card Y by CARD_1:def 11 .= Card card X *` Card card Y by CARD_1:def 11 .= Card (card X * card Y) by Th52; hence thesis by CARD_1:71; end; canceled; theorem for X,Y being finite set st X c< Y holds card X < card Y & Card X <` Card Y proof let X,Y be finite set; assume A1: X c< Y; then X c= Y & X <> Y by XBOOLE_0:def 8; then A2: Y = X \/ (Y\X) & X misses (Y\X) & X is finite & Y\X is finite by XBOOLE_1:45,79; then A3: card Y = card X + card (Y\X) by Th53; A4: now assume card (Y\X) = 0; then Y \ X = {} by Th59; hence contradiction by A1,A2; end; A5: card X <= card Y by A3,NAT_1:29; now assume card X = card Y; then card X + 0 = card Y; hence contradiction by A3,A4,XCMPLX_1:2; end; hence card X < card Y by A5,REAL_1:def 5; hence thesis by Th58; end; theorem (Card X <=` Card Y or Card X <` Card Y) & Y is finite implies X is finite proof assume A1: (Card X <=` Card Y or Card X <` Card Y) & Y is finite; then (Card X c= Card Y or Card X in Card Y) & Card X = Card X & Card Y = Card Y & Y,Card Y are_equipotent by CARD_1:def 5; then Card X c= Card Y & Card Y is finite by A1,CARD_1:68,ORDINAL1:def 2; then Card X is finite & X,Card X are_equipotent by CARD_1:def 5,FINSET_1:13 ; hence X is finite by CARD_1:68; end; reserve x1,x2,x3,x4,x5,x6,x7,x8 for set; theorem Th69: card {x1,x2} <= 2 proof card {x1} = 1 & card {x2} = 1 & {x1,x2} = {x1} \/ {x2} & {x1} is finite & {x2} is finite & 1+1 = 2 by CARD_1:79,ENUMSET1:41; hence thesis by Th62; end; theorem Th70: card {x1,x2,x3} <= 3 proof card {x1} = 1 & {x1,x2,x3} = {x1} \/ {x2,x3} & {x1} is finite & {x2,x3} is finite & card {x2,x3} <= 2 by Th69,CARD_1:79,ENUMSET1:42; then 1 + card {x2,x3} <= 1+2 & card {x1,x2,x3} <= 1 + card {x2,x3} by Th62,REAL_1:55; hence thesis by AXIOMS:22; end; theorem Th71: card {x1,x2,x3,x4} <= 4 proof card {x1} = 1 & {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} & {x1} is finite & {x2,x3,x4} is finite & card {x2,x3,x4} <= 3 by Th70,CARD_1:79,ENUMSET1:44; then 1 + card {x2,x3,x4} <= 1+3 & card {x1,x2,x3,x4} <= 1 + card {x2,x3,x4 } by Th62,REAL_1:55; hence thesis by AXIOMS:22; end; theorem Th72: card {x1,x2,x3,x4,x5} <= 5 proof card {x1} = 1 & {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} & {x1} is finite & {x2,x3,x4,x5} is finite & card {x2,x3,x4,x5} <= 4 by Th71,CARD_1:79,ENUMSET1:47; then 1 + card {x2,x3,x4,x5} <= 1+4 & card {x1,x2,x3,x4,x5} <= 1 + card {x2,x3,x4,x5} by Th62,REAL_1:55; hence thesis by AXIOMS:22; end; theorem Th73: card {x1,x2,x3,x4,x5,x6} <= 6 proof card {x1} = 1 & {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} & {x1} is finite & {x2,x3,x4,x5,x6} is finite & card {x2,x3,x4,x5,x6} <= 5 by Th72,CARD_1:79,ENUMSET1:51; then 1 + card {x2,x3,x4,x5,x6} <= 1+5 & card {x1,x2,x3,x4,x5,x6} <= 1 + card {x2,x3,x4,x5,x6} by Th62,REAL_1:55; hence thesis by AXIOMS:22; end; theorem Th74: card {x1,x2,x3,x4,x5,x6,x7} <= 7 proof card {x1} = 1 & {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} & {x1} is finite & {x2,x3,x4,x5,x6,x7} is finite & card {x2,x3,x4,x5,x6,x7} <= 6 by Th73,CARD_1:79,ENUMSET1:56; then 1 + card {x2,x3,x4,x5,x6,x7} <= 1+6 & card {x1,x2,x3,x4,x5,x6,x7} <= 1 + card {x2,x3,x4,x5,x6,x7} by Th62,REAL_1:55; hence thesis by AXIOMS:22; end; theorem card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8 proof {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} & card {x1} = 1 & {x1} is finite & {x2,x3,x4,x5,x6,x7,x8} is finite & card {x2,x3,x4,x5,x6,x7,x8} <= 7 by Th74,CARD_1:79,ENUMSET1:62; then 1 + card {x2,x3,x4,x5,x6,x7,x8} <= 1+7 & card {x1,x2,x3,x4,x5,x6,x7,x8} <= 1 + card {x2,x3,x4,x5,x6,x7,x8} by Th62,REAL_1:55; hence thesis by AXIOMS:22; end; theorem Th76: x1 <> x2 implies card {x1,x2} = 2 proof assume x1 <> x2; then {x1} misses {x2} & {x1} is finite & {x2} is finite & card {x1} = 1 & card {x2} = 1 & {x1,x2} = {x1} \/ {x2} & 1+1 = 2 by CARD_1:79,ENUMSET1:41,ZFMISC_1:17; hence thesis by Th53; end; theorem Th77: x1 <> x2 & x1 <> x3 & x2 <> x3 implies card {x1,x2,x3} = 3 proof assume x1 <> x2 & x1 <> x3 & x2 <> x3; then card {x1,x2} = 2 & not x3 in {x1,x2} & {x1,x2} is finite & {x1,x2,x3} = {x1,x2} \/ {x3} by Th76,ENUMSET1:43,TARSKI:def 2; hence card {x1,x2,x3} = 2+1 by Th54 .= 3; end; theorem x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies card {x1,x2,x3,x4} = 4 proof assume x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4; then card {x1,x2,x3} = 3 & not x4 in {x1,x2,x3} & {x1,x2,x3} is finite & {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by Th77,ENUMSET1:13,46; hence card {x1,x2,x3,x4} = 3+1 by Th54 .= 4; end;