:: Ramsey's Theorem :: by Marco Riccardi :: :: Received April 18, 2008 :: Copyright (c) 2008 Association of Mizar Users environ vocabularies RELAT_1, ARYTM_1, BOOLE, FINSEQ_1, FUNCT_1, TARSKI, EQREL_1, T_1TOPSP, ARYTM, FUNCT_2, SEQM_3, CARD_4, ORDINAL2, HENMODEL, NEWTON, FINSET_1, CARD_1, GR_CY_1, BORSUK_1, GROUP_10, RAMSEY_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, NAT_1, NAT_3, NUMBERS, PARTFUN1, SEQM_3, EQREL_1, ORDINAL1, FINSET_1, CARD_1, FUNCT_2, CARD_4, XREAL_0, REAL_1, MEMBERED, WELLORD2, BORSUK_1, GROUP_10, POLYNOM1, NEWTON, BINARITH, SEQ_1, RVSUM_1; constructors SETFAM_1, PARTFUN1, XXREAL_0, XREAL_0, NAT_1, NAT_3, FINSEQ_1, EQREL_1, NUMBERS, XCMPLX_0, CARD_1, MEMBERED, WELLORD2, FUNCT_2, RELAT_1, FUNCT_1, BORSUK_1, CARD_4, GROUP_10, SEQM_3, POLYNOM1, NEWTON, BINARITH, REAL_1, NAT_D, BINOP_2, INT_2, FINSOP_1, SEQ_1, RVSUM_1; registrations XBOOLE_0, SUBSET_1, PARTFUN1, XXREAL_0, XREAL_0, FINSEQ_1, RELAT_1, ORDINAL1, EQREL_1, NUMBERS, REAL_1, CARD_4, CARD_5, NAT_1, NAT_2, NAT_3, CARD_1, MEMBERED, FINSET_1, FUNCT_1, FUNCT_2, BORSUK_1, GROUP_10, SEQM_3, POLYNOM1, NEWTON, BINARITH; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, XBOOLE_0, EQREL_1, BORSUK_1, CARD_1, WELLORD2, ZFMISC_1, FUNCT_1, FUNCT_2, RELAT_1, FINSET_1, INT_1, NAT_1, ORDINAL1, MEMBERED, GROUP_10; theorems TARSKI, XBOOLE_0, XBOOLE_1, EQREL_1, BORSUK_1, CARD_1, WELLORD2, FUNCT_1, FUNCT_2, RELAT_1, GROUP_10, FINSET_1, ZFMISC_1, INT_1, CARD_4, CARD_2, NAT_1, XREAL_1, ORDINAL1, XXREAL_0, STIRL2_1, WAYBEL12, COMPL_SP, CARD_FIL, FINSEQ_1, BINARITH, NEWTON, ENUMSET1; schemes NAT_1, FUNCT_1, FUNCT_2, RECDEF_2; begin :: Preliminaries reserve n,m,k for natural number, X,Y,Z for set, f for Function of X,Y, H for Subset of X; definition let X,Y,H; let P be a_partition of the_subsets_of_card(Y,X); pred H is_homogeneous_for P means :Def1: ex p being Element of P st the_subsets_of_card(Y,H) c= p; end; registration let n; let X be infinite set; cluster the_subsets_of_card(n,X) -> non empty; correctness proof Card X is infinite by CARD_4:1; then Card n c= Card X by CARD_4:13; hence thesis by GROUP_10:2; end; end; definition let n,X,Y,f; assume A1: f is one-to-one & Card n c= Card X & X is non empty & Y is non empty; func f ||^ n -> Function of the_subsets_of_card(n,X), the_subsets_of_card(n,Y) means :Def2: for x being Element of the_subsets_of_card(n,X) holds it.x = f .: x; existence proof deffunc F(set) = f .: $1; set D = the_subsets_of_card(n,X); reconsider D as non empty set by A1,GROUP_10:2; consider IT be Function such that A2: dom IT = D & for x being Element of D holds IT.x = F(x) from FUNCT_1:sch 4; for y being set st y in rng IT holds y in the_subsets_of_card(n,Y) proof let y be set; assume y in rng IT; then consider x be set such that A3: x in dom IT & y = IT.x by FUNCT_1:def 5; consider x' be Subset of X such that A4: x=x' & Card x' = n by A3,A2; reconsider x as Element of D by A3,A2; A5: y = f .: x by A3,A2; f in Funcs(X, Y) by A1,FUNCT_2:11; then consider f' be Function such that A6: f=f' & dom f'=X & rng f' c= Y by FUNCT_2:def 2; f .: x c= rng f by RELAT_1:144; then reconsider y'=y as Subset of Y by A6,A5,XBOOLE_1:1; x, f.: x are_equipotent by A6,A4,A1,CARD_1:60; then Card y' = n by A5,A4,CARD_1:21; hence y in the_subsets_of_card(n,Y); end; then rng IT c= the_subsets_of_card(n,Y) by TARSKI:def 3; then reconsider IT as Function of the_subsets_of_card(n,X), the_subsets_of_card(n,Y) by A2,FUNCT_2:4; take IT; thus thesis by A2; end; uniqueness proof let F1,F2 be Function of the_subsets_of_card(n,X),the_subsets_of_card(n,Y) such that A7: for x being Element of the_subsets_of_card(n,X) holds F1.x = f .: x and A8: for x being Element of the_subsets_of_card(n,X) holds F2.x = f .: x; now let x be set; assume x in the_subsets_of_card(n,X); then reconsider x' = x as Element of the_subsets_of_card(n,X); thus F1.x = f .: x' by A7 .= F2.x by A8; end; hence thesis by FUNCT_2:18; end; end; Lm1: X c= Y implies the_subsets_of_card(Z,X) c= the_subsets_of_card(Z,Y) proof assume A1: X c= Y; for x being set holds x in the_subsets_of_card(Z,X) implies x in the_subsets_of_card(Z,Y) proof let x be set; assume x in the_subsets_of_card(Z,X); then consider x' be Subset of X such that A2: x'=x & Card x' = Z; reconsider x''=x' as Subset of Y by A1,XBOOLE_1:1; x''=x & Card x'' = Z by A2; hence x in the_subsets_of_card(Z,Y); end; hence thesis by TARSKI:def 3; end; theorem Th1: f is one-to-one & Card n c= Card X & X is non empty & Y is non empty implies the_subsets_of_card(n,f .: H) = (f||^n) .: the_subsets_of_card(n,H) proof assume A1: f is one-to-one & Card n c= Card X & X is non empty & Y is non empty; then f in Funcs(X, Y) by FUNCT_2:11; then consider f' be Function such that A2: f=f' & dom f'=X & rng f' c= Y by FUNCT_2:def 2; A3: Card X c= Card Y by A2,A1,CARD_1:26; consider f1 be Function such that A4: n c= f1 .: X by A1,CARD_2:2; consider f2 be Function such that A5: X c= f2 .: Y by A3,CARD_2:2; f1 .: X c= f1 .:(f2 .: Y) by A5,RELAT_1:156; then n c= f1 .:(f2 .: Y) by A4,XBOOLE_1:1; then n c= (f1*f2) .: Y by RELAT_1:159; then Card n c= Card Y by CARD_2:2; then the_subsets_of_card(n,Y) is non empty by A1,GROUP_10:2; then f||^n in Funcs(the_subsets_of_card(n,X), the_subsets_of_card(n,Y)) by FUNCT_2:11; then consider fn be Function such that A6: f||^n=fn & dom fn=the_subsets_of_card(n,X) & rng fn c= the_subsets_of_card(n,Y) by FUNCT_2:def 2; for y being set holds y in the_subsets_of_card(n,f.:H) iff y in (f||^n).:the_subsets_of_card(n,H) proof let y be set; hereby assume y in the_subsets_of_card(n,f.:H); then consider X' be Subset of f.:H such that A7: y=X' & Card X' = n; A8: f.:H c= rng f by RELAT_1:144; ex x being set st x in dom(f||^n) & x in the_subsets_of_card(n,H) & y = (f||^n).x proof set x = f"y; A9: f.:x = y by A8,FUNCT_1:147,A7,XBOOLE_1:1; take x; A10: x c= dom f by RELAT_1:167; reconsider x'=x as Subset of H by A9,A7,A10,A1,FUNCT_1:157; x, f.: x are_equipotent by A10,A1,CARD_1:60; then A11: Card x' = n by A7,A9,CARD_1:21; then A12: x in the_subsets_of_card(n,H); A13: the_subsets_of_card(n,H) c= the_subsets_of_card(n,X) by Lm1; thus x in dom(f||^n) by A6,A13,A12; thus x in the_subsets_of_card(n,H) by A11; thus y = f.:x by A8,FUNCT_1:147,A7,XBOOLE_1:1 .= (f||^n).x by A1,A13,A12,Def2; end; hence y in (f||^n).:the_subsets_of_card(n,H) by FUNCT_1:def 12; end; assume y in (f||^n).:the_subsets_of_card(n,H); then consider x be set such that A14: x in dom(f||^n) & x in the_subsets_of_card(n,H) & y = (f||^n).x by FUNCT_1:def 12; reconsider x as Element of the_subsets_of_card(n,X) by A14; A15: y = f .: x by A14,A1,Def2; consider x' be Subset of H such that A16: x'=x & Card x' = n by A14; reconsider X'=y as Subset of f.:H by A15,A16,RELAT_1:156; x, f.: x are_equipotent by A1,CARD_1:60,A2,A16,XBOOLE_1:1; then Card X' = n by A16,A15,CARD_1:21; hence y in the_subsets_of_card(n,f.:H); end; hence thesis by TARSKI:2; end; Lm2: the_subsets_of_card(0,X) = {0} proof for x being set holds x in the_subsets_of_card(0,X) iff x=0 proof let x be set; hereby assume x in the_subsets_of_card(0,X); then consider x' be Subset of X such that A1: x'=x & Card x' = 0; thus x=0 by A1,CARD_2:59; end; assume A2: x=0; then reconsider x'=x as Subset of X by XBOOLE_1:2; Card x' = 0 by A2,CARD_1:47; hence x in the_subsets_of_card(0,X); end; hence thesis by TARSKI:def 1; end; Lm3: for X,Y being finite set st Card Y = X holds the_subsets_of_card(X,Y) = {Y} proof let X,Y be finite set; assume A1: Card Y = X; for x being set holds x in the_subsets_of_card(X,Y) iff x = Y proof let x be set; hereby assume x in the_subsets_of_card(X,Y); then consider X' be Subset of Y such that A2: X'=x & Card X' = X; reconsider X' as finite Subset of Y; card(Y \ X') = card Y - card X' by CARD_2:63 .= 0 by A2,A1; then Y \ X' = {} by CARD_2:59; then Y c= X' by XBOOLE_1:37; hence x = Y by A2,XBOOLE_0:def 10; end; assume A3: x = Y; then x c= Y; then reconsider x'=x as Subset of Y; x' in the_subsets_of_card(X,Y) by A1,A3; hence thesis; end; hence the_subsets_of_card(X,Y) = {Y} by TARSKI:def 1; end; theorem Th2: X is infinite & X c= omega implies Card X = omega proof assume A1: X is infinite & X c= omega; X is countable by A1,CARD_4:46,44; then NAT,X are_equipotent by A1,WAYBEL12:3; hence thesis by CARD_1:84,21; end; theorem Th3: X is infinite implies X \/ Y is infinite proof assume A1: X is infinite; assume A2: X \/ Y is finite; Card X c= Card(X \/ Y) by XBOOLE_1:7,CARD_1:27; hence contradiction by A2,A1,CARD_2:68; end; theorem Th4: X is infinite & Y is finite implies X \ Y is infinite proof assume A1: X is infinite & Y is finite; assume A2: X \ Y is finite; A3: X \/ Y = (X \ Y) \/ Y by XBOOLE_1:39; X \/ Y is infinite by A1,Th3; hence contradiction by A2,A1,A3,FINSET_1:14; end; registration let X be infinite set; let Y be set; cluster X \/ Y -> infinite; correctness by Th3; end; registration let X be infinite set; let Y be finite set; cluster X \ Y -> infinite; correctness by Th4; end; Lm4: for X,Y being non empty set, f being Function of X,Y holds f is constant iff ex y being Element of Y st rng f = {y} proof let X,Y be non empty set; let f be Function of X,Y; hereby assume A1: f is constant; consider x be set such that A2: x in dom f by XBOOLE_0:def 1; set y = f.x; reconsider y as Element of Y by A2,FUNCT_2:7; take y; for y' being set holds y' in rng f iff y' = y proof let y' be set; hereby assume y' in rng f; then consider x' be set such that A3: x' in dom f & y' = f.x' by FUNCT_1:def 5; thus y' = y by A3,A2,A1,FUNCT_1:def 16; end; assume y' = y; hence y' in rng f by A2,FUNCT_2:6; end; hence rng f = {y} by TARSKI:def 1; end; given y be Element of Y such that A4: rng f = {y}; for x,x' being set holds x in dom f & x' in dom f implies f.x=f.x' proof let x,x' be set; assume A5: x in dom f; assume A6: x' in dom f; A7: f.x in rng f & f.x' in rng f by A5,A6,FUNCT_2:6; hence f.x = y by A4,TARSKI:def 1 .= f.x' by A4,A7,TARSKI:def 1; end; hence f is constant by FUNCT_1:def 16; end; Lm5: for F being Function of (the_subsets_of_card(n,X)),k st Card X = omega & X c= omega & k<>0 holds ex H st H is infinite & F|the_subsets_of_card(n,H) is constant proof defpred P[natural number] means for k being natural number, X being set, F being Function of (the_subsets_of_card($1,X)),k st Card X = omega & X c= omega & k<>0 holds ex H being Subset of X st H is infinite & F|the_subsets_of_card($1,H) is constant; A1: P[0] proof let k be natural number; let X be set; let F be Function of (the_subsets_of_card(0,X)),k; assume A2: Card X = omega; assume X c= omega; assume k<>0; set H = X; A3: H c= X; reconsider H as Subset of X by A3; take H; thus H is infinite by A2,CARD_4:1; for x,y being set holds x in dom(F|the_subsets_of_card(0,H)) & y in dom(F|the_subsets_of_card(0,H)) implies F|the_subsets_of_card(0,H).x=F|the_subsets_of_card(0,H).y proof let x,y be set; A4: dom(F|the_subsets_of_card(0,H)) = dom(F|{0}) by Lm2 .= dom F /\ {0} by RELAT_1:90; assume x in dom(F|the_subsets_of_card(0,H)); then A5: x in {0} by A4,XBOOLE_0:def 3; assume y in dom(F|the_subsets_of_card(0,H)); then y in {0} by A4,XBOOLE_0:def 3; then y=0 by TARSKI:def 1; hence thesis by A5,TARSKI:def 1; end; hence F|the_subsets_of_card(0,H) is constant by FUNCT_1:def 16; end; A6: for n be natural number st P[n] holds P[n + 1] proof let n be natural number; assume A7: P[n]; now let k be natural number; let X be set; let F be Function of (the_subsets_of_card(n+1,X)),k; assume A8: Card X = omega; assume A9: X c= omega; assume A10: k<>0; A11: for Y being set,a being Element of Y st Card Y = omega & Y c= X ex Fa being Function of the_subsets_of_card(n,Y\{a}),k, Ha being Subset of Y\{a} st Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant & for Y' being Element of the_subsets_of_card(n,Y\{a}) holds Fa.Y' = F.(Y' \/ {a}) proof let Y be set; let a be Element of Y; assume A12: Card Y = omega; assume A13: Y c= X; set Y1 = the_subsets_of_card(n,Y\{a}); A14: Y is infinite by CARD_4:1,A12; Y is non empty by CARD_4:1,A12; then A15: {a} c= Y by ZFMISC_1:37; A16: Y\{a} is infinite proof assume A17: Y\{a} is finite; (Y\{a}) \/ {a} is finite by A17,FINSET_1:14; then Y \/ {a} is finite by XBOOLE_1:39; hence contradiction by A14,A15,XBOOLE_1:12; end; Card(Y\{a}) is infinite by A16,CARD_4:1; then Card n c= Card(Y\{a}) by CARD_4:13; then reconsider Y1 as non empty set by A16,GROUP_10:2; deffunc F1(Element of Y1)=F.($1 \/ {a}); A18: for x being Element of Y1 holds F1(x) in k proof let x be Element of Y1; x in Y1; then consider x' be Subset of Y\{a} such that A19: x=x' & Card x'=n; x \/ {a} c= (Y\{a}) \/ {a} by A19,XBOOLE_1:9; then x \/ {a} c= Y \/ {a} by XBOOLE_1:39; then reconsider y=x \/ {a} as Subset of Y by A15,XBOOLE_1:12; reconsider x''=x' as finite set by A19,CARD_4:1; A20: not a in x'' proof assume a in x''; then not a in {a} by XBOOLE_0:def 4; hence contradiction by TARSKI:def 1; end; A21: the_subsets_of_card(n+1,Y) c= the_subsets_of_card(n+1,X) by A13,Lm1; Card y = n+1 by A19,A20,CARD_2:54; then x \/ {a} in the_subsets_of_card(n+1,Y); hence F1(x) in k by A10,A21,FUNCT_2:7; end; consider Fa be Function of Y1,k such that A22: for x being Element of Y1 holds Fa.x = F1(x) from FUNCT_2:sch 8(A18); reconsider Fa as Function of the_subsets_of_card(n,Y\{a}),k; set Y'=Y\{a}; A23: Y c= omega by A9,A13,XBOOLE_1:1; then A24: Y\{a} c= omega by XBOOLE_1:1; Card(Y\{a}) = omega by A16,A23,Th2,XBOOLE_1:1; then consider Ha be Subset of Y\{a} such that A25: Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant by A7,A10,A24; take Fa,Ha; thus Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant by A25; let Y' be Element of the_subsets_of_card(n,Y\{a}); thus Fa.Y' = F.(Y' \/ {a}) by A22; end; X c= X; then A26: X in the_subsets_of_card(omega,X) by A8; then reconsider A = the_subsets_of_card(omega,X) as non empty set; defpred P1[set,set,set,set,set] means for x1,x2 being Element of A, y1,y2 being Element of omega st $2=x1 & $3=y1 & $4=x2 & $5=y2 holds (y1 in x1 implies (ex F1 being Function of the_subsets_of_card(n,x1\{y1}),k, H1 being Subset of x1\{y1} st H1 is infinite & F1|the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x1' being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x1' = F.(x1' \/ {y1})) & for y2' being Element of omega st y2'>y1 & y2' in H1 holds y2<=y2')) & (not y1 in x1 implies x2=X & y2=0); A27: for a being Element of NAT, x'' being Element of A, y'' being Element of omega ex x1'' being Element of A, y1'' being Element of omega st P1[a,x'',y'',x1'',y1''] proof let a be Element of NAT; let x'' be Element of A; let y'' be Element of omega; per cases; suppose A28: y'' in x''; then reconsider a'=y'' as Element of x''; x'' in A; then consider x''' be Subset of X such that A29: x'''=x'' & Card x''' = omega; consider Fa be Function of the_subsets_of_card(n,x''\{a'}),k, Ha be Subset of x''\{a'} such that A30: Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant & for Y' being Element of the_subsets_of_card(n,x''\{a'}) holds Fa.Y' = F.(Y' \/ {a'}) by A11,A29; Ha c= x'' by XBOOLE_1:1; then A31: Ha c= X by A29,XBOOLE_1:1; then A32: Ha c= omega by A9,XBOOLE_1:1; then Card Ha = omega by A30,Th2; then Ha in A by A31; then reconsider x1''=Ha as Element of A; set y1''=min* {y2' where y2' is Element of omega: y2'>y'' & y2' in Ha}; take x1'', y1''; now let x1,x2 be Element of A; let y1,y2 be Element of omega; assume A33: x''=x1 & y''=y1; assume A34: x1''=x2 & y1''=y2; thus (y1 in x1 implies (ex F1 being Function of the_subsets_of_card(n,x1\{y1}),k, H1 being Subset of x1\{y1} st H1 is infinite & F1|the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x1' being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x1' = F.(x1' \/ {y1})) & for y2' being Element of omega st y2'>y1 & y2' in H1 holds y2<=y2')) proof assume y1 in x1; reconsider F1=Fa as Function of the_subsets_of_card(n,x1\{y1}),k by A33; reconsider H1=Ha as Subset of x1\{y1} by A33; take F1, H1; thus H1 is infinite by A30; thus F1|the_subsets_of_card(n,H1) is constant by A30; thus x2=H1 by A34; set A'= {y2' where y2' is Element of omega: y2'>y'' & y2' in Ha}; for x being set st x in A' holds x in NAT proof let x be set; assume x in A'; then consider x' be Element of omega such that A35: x'=x & x'>y'' & x' in Ha; thus x in NAT by A35; end; then reconsider A' as Subset of NAT by TARSKI:def 3; A36: A' <> {} proof assume A37: A' = {}; set A'' = {y2''' where y2''' is Element of omega: y2'''<=y'' & y2''' in Ha}; now let x be set; assume x in A''; then consider x' be Element of omega such that A38: x=x' & x'<=y'' & x' in Ha; x' < y''+1 by A38,NAT_1:13; hence x in Segm(y''+1) by NAT_1:45,A38; end; then A'' c= Segm(y''+1) by TARSKI:def 3; then A39: A'' is finite by FINSET_1:13; A40: now let x be set; assume A41: x in A' \/ A''; per cases by A41,XBOOLE_0:def 2; suppose x in A'; then consider x' be Element of omega such that A42: x=x' & x'>y'' & x' in Ha; thus x in Ha by A42; end; suppose x in A''; then consider x' be Element of omega such that A43: x=x' & x'<=y'' & x' in Ha; thus x in Ha by A43; end; end; now let x be set; assume A44: x in Ha; then reconsider x'=x as Element of omega by A32; per cases; suppose x'<=y''; then x in A'' by A44; hence x in A' \/ A'' by XBOOLE_0:def 2; end; suppose x'>y''; then x in A' by A44; hence x in A' \/ A'' by XBOOLE_0:def 2; end; end; hence contradiction by A30,A37,A39,A40,TARSKI:2; end; y1'' in A' by A36,NAT_1:def 1; then consider y2'' be Element of omega such that A45: y1''=y2'' & y2''>y'' & y2'' in Ha; thus y2 in H1 by A45,A34; thus y1 < y2 by A45,A33,A34; thus (for x1' being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x1' = F.(x1' \/ {y1})) by A33,A30; let y2' be Element of omega; assume A46: y2'>y1; assume A47: y2' in H1; y2' in A' by A46,A47,A33; hence y2<=y2' by A34,NAT_1:def 1; end; assume not y1 in x1; hence thesis by A33,A28; end; hence thesis; end; suppose A48: not y'' in x''; reconsider x1''=X as Element of A by A26; reconsider y1''=0 as Element of omega by INT_1:16; take x1'', y1''; thus thesis by A48; end; end; reconsider X0=X as Element of A by A26; set Y0 = min* X; consider S be Function of NAT, A, a be Function of NAT, omega such that A49: S.0 = X0 & a.0 = Y0 & for i being Element of NAT holds P1[i,S.i,a.i,S.(i+1),a.(i+1)] from RECDEF_2:sch 3(A27); defpred P2[natural number] means a.$1 in a.($1+1) & S.($1+1) c= S.$1 & a.$1 in S.$1 & a.($1+1) in S.($1+1) & not a.$1 in S.($1+1); A50: P2[0] proof set i=0; reconsider i as Element of NAT by ORDINAL1:def 13; reconsider x1=S.i as Element of A; reconsider x2=S.(i+1) as Element of A; reconsider y1=a.i as Element of omega; reconsider y2=a.(i+1) as Element of omega; P1[i,S.i,a.i,S.(i+1),a.(i+1)] by A49; then A51: (y1 in x1 implies (ex F1 being Function of the_subsets_of_card(n,x1\{y1}),k, H1 being Subset of x1\{y1} st H1 is infinite & F1|the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x1' being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x1' = F.(x1' \/ {y1})) & for y2' being Element of omega st y2'>y1 & y2' in H1 holds y2<=y2')) & (not y1 in x1 implies x2=X & y2=0); consider F1 be Function of the_subsets_of_card(n,x1\{y1}),k, H1 be Subset of x1\{y1} such that A52: H1 is infinite & F1|the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 by A51,A49,NAT_1:def 1,A8,A9,CARD_1:47; thus a.0 in a.(0+1) by A52,NAT_1:45; thus S.(0+1) c= S.0 by A52,XBOOLE_1:1; thus a.0 in S.0 by A49,NAT_1:def 1,A8,A9,CARD_1:47; thus a.(0+1) in S.(0+1) by A52; not y1 in x2 proof assume y1 in x2; then not y1 in {y1} by A52,XBOOLE_0:def 4; hence contradiction by TARSKI:def 1; end; hence not a.0 in S.(0+1); end; A53: for i being natural number st P2[i] holds P2[i + 1] proof let i be natural number; assume A54: P2[i]; reconsider i'=i+1 as Element of NAT by ORDINAL1:def 13; reconsider x1=S.i' as Element of A; reconsider x2=S.(i'+1) as Element of A; reconsider y1=a.i' as Element of omega; reconsider y2=a.(i'+1) as Element of omega; consider F1 be Function of the_subsets_of_card(n,x1\{y1}),k, H1 be Subset of x1\{y1} such that A55: H1 is infinite & F1|the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x1' being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x1' = F.(x1' \/ {y1})) & for y2' being Element of omega st y2'>y1 & y2' in H1 holds y2<=y2' by A49,A54; thus P2[i + 1] proof thus a.(i+1) in a.(i+1+1) by A55,NAT_1:45; thus S.(i+1+1) c= S.(i+1) by A55,XBOOLE_1:1; thus a.(i+1) in S.(i+1) by A54; thus a.(i+1+1) in S.(i+1+1) by A55; not y1 in x2 proof assume y1 in x2; then not y1 in {y1} by A55,XBOOLE_0:def 4; hence contradiction by TARSKI:def 1; end; hence not a.(i+1) in S.(i+1+1); end; end; A56: for i being natural number holds P2[i] from NAT_1:sch 2(A50,A53); defpred P3[natural number] means for i,j being natural number st i>=j & i=$1+j holds S.i c= S.j & (for ai,aj being natural number st i<>j & ai=a.i & aj=a.j holds ai > aj); A57: P3[0]; A58: for l being natural number st P3[l] holds P3[l+1] proof let l be natural number; assume A59: P3[l]; thus P3[l+1] proof let i,j be natural number; assume A60: i>=j; assume A61: i=l+1+j; i<>j proof assume i=j; then 0=l+1 by A61; hence contradiction; end; then A62: i>j by A60,XXREAL_0:1; set j'=j+1; i>=j' & i=l+j' by A62,A61,NAT_1:13; then A63: S.i c= S.(j+1) & (for ai,aj' being natural number st i<>j' & ai=a.i & aj'=a.j' holds ai > aj') by A59; S.(j+1) c= S.j by A56; hence S.i c= S.j by A63,XBOOLE_1:1; thus for ai,aj being natural number st i<>j & ai=a.i & aj=a.j holds ai > aj proof let ai,aj be natural number; assume i<>j; assume A64: ai=a.i & aj=a.j; per cases; suppose A65: i=j'; a.j in a.(j+1) by A56; hence ai > aj by A64,A65,NAT_1:45; end; suppose i<>j'; reconsider aj'=a.j' as natural number; aj in aj' by A64,A56; then aj' > aj by NAT_1:45; hence ai > aj by A63,A64,XXREAL_0:2; end; end; end; end; A66: for l being natural number holds P3[l] from NAT_1:sch 2(A57,A58); A67: for i,j being natural number st i>=j holds S.i c= S.j & (for ai,aj being natural number st i<>j & ai=a.i & aj=a.j holds ai > aj) proof let i,j be natural number; assume A68: i>=j; then consider l be natural number such that A69: i = j + l by NAT_1:10; thus S.i c= S.j by A66,A68,A69; thus for ai,aj being natural number st i<>j & ai=a.i & aj=a.j holds ai > aj by A66,A68,A69; end; A70: for i being Element of NAT, Y being set, Fi being Function of the_subsets_of_card(n,S.i\{a.i}),k st Y = {x where x is Element of omega: ex j being Element of NAT st a.j=x & j>i} & (for Y' being Element of the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y' = F.(Y' \/ {a.i})) holds Y c= S.(i+1) & Fi|the_subsets_of_card(n,Y) is constant proof let i be Element of NAT; let Y be set; let Fi be Function of the_subsets_of_card(n,S.i\{a.i}),k; assume A71: Y = {x where x is Element of omega: ex j being Element of NAT st a.j=x & j>i}; assume A72: for Y' being Element of the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y' = F.(Y' \/ {a.i}); consider x1 be Element of A, y1 be Element of omega such that A73: S.i=x1 & a.i=y1; consider x2 be Element of A, y2 be Element of omega such that A74: S.(i+1)=x2 & a.(i+1)=y2; y1 in x1 implies (ex F1 being Function of the_subsets_of_card(n,x1\{y1}),k, H1 being Subset of x1\{y1} st H1 is infinite & F1|the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x1' being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x1' = F.(x1' \/ {y1})) & for y2' being Element of omega st y2'>y1 & y2' in H1 holds y2<=y2') & (not y1 in x1 implies x2=X & y2=0) by A49,A73,A74; then consider F1 be Function of the_subsets_of_card(n,x1\{y1}),k, H1 be Subset of x1\{y1} such that A75: H1 is infinite & F1|the_subsets_of_card(n,H1) is constant & x2=H1 & (for x1' being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x1' = F.(x1' \/ {y1})) & for y2' being Element of omega st y2'>y1 & y2' in H1 holds y2<=y2' by A73,A56; reconsider F1 as Function of the_subsets_of_card(n,S.i\{a.i}),k by A73; for x1' being Element of the_subsets_of_card(n,S.i\{a.i}) holds F1.x1' = Fi.x1' proof let x1' be Element of the_subsets_of_card(n,S.i\{a.i}); thus F1.x1' = F.(x1' \/ {a.i}) by A73,A75 .= Fi.x1' by A72; end; then A76: Fi|the_subsets_of_card(n,S.(i+1)) is constant by A75,A74,FUNCT_2:113; now let x be set; assume x in Y; then consider x' be Element of omega such that A77: x=x' & ex j being Element of NAT st a.j=x' & j>i by A71; consider j be Element of NAT such that A78: a.j=x & j>i by A77; j>=i+1 by NAT_1:13,A78; then A79: S.j c= S.(i+1) by A67; a.j in S.j by A56; hence x in S.(i+1) by A78,A79; end; hence A80: Y c= S.(i+1) by TARSKI:def 3; A81: the_subsets_of_card(n,Y) c= the_subsets_of_card(n,S.(i+1)) by Lm1,A80; for x,y being set st x in dom(Fi|the_subsets_of_card(n,Y)) & y in dom(Fi|the_subsets_of_card(n,Y)) holds Fi|the_subsets_of_card(n,Y).x = Fi|the_subsets_of_card(n,Y).y proof let x,y be set; assume x in dom(Fi|the_subsets_of_card(n,Y)); then A82: x in dom Fi & x in the_subsets_of_card(n,Y) by RELAT_1:86; then A83: x in dom(Fi|the_subsets_of_card(n,S.(i+1))) by A81,RELAT_1:86; assume y in dom(Fi|the_subsets_of_card(n,Y)); then A84: y in dom Fi & y in the_subsets_of_card(n,Y) by RELAT_1:86; then A85: y in dom(Fi|the_subsets_of_card(n,S.(i+1))) by A81,RELAT_1:86; thus Fi|the_subsets_of_card(n,Y).x = (Fi|the_subsets_of_card(n,S.(i+1)))|the_subsets_of_card(n,Y).x by A81,FUNCT_1:82 .= Fi|the_subsets_of_card(n,S.(i+1)).x by A82,FUNCT_1:72 .= Fi|the_subsets_of_card(n,S.(i+1)).y by A85,A76,A83,FUNCT_1:def 16 .= (Fi|the_subsets_of_card(n,S.(i+1)))|the_subsets_of_card(n,Y).y by A84,FUNCT_1:72 .= Fi|the_subsets_of_card(n,Y).y by A81,FUNCT_1:82; end; hence Fi|the_subsets_of_card(n,Y) is constant by FUNCT_1:def 16; end; for x1,x2 being set st x1 in dom a & x2 in dom a & a.x1 = a.x2 holds x1 = x2 proof let x1,x2 be set; assume A86: x1 in dom a; assume A87: x2 in dom a; assume A88: a.x1 = a.x2; assume A89: x1 <> x2; reconsider i1=x1 as Element of NAT by A86; reconsider i2=x2 as Element of NAT by A87; reconsider ai1=a.i1 as Element of NAT; reconsider ai2=a.i2 as Element of NAT; per cases by A89,XXREAL_0:1; suppose i1 < i2; then ai1 < ai2 by A67; hence contradiction by A88; end; suppose i1 > i2; then ai1 > ai2 by A67; hence contradiction by A88; end; end; then A90: a is one-to-one by FUNCT_1:def 8; A91: NAT = dom a by FUNCT_2:def 1; A92: for i being Element of NAT holds Card {x' where x' is Element of omega: ex j being Element of NAT st a.j=x' & j>i} = omega proof let i be Element of NAT; set Z = {x' where x' is Element of omega: ex j being Element of NAT st a.j=x' & j>i}; A93: dom(a|(NAT \ Segm(i+1))) = dom a /\ (NAT \ Segm(i+1)) by RELAT_1:90 .= NAT /\ (NAT \ Segm(i+1)) by FUNCT_2:def 1 .= (NAT /\ NAT) \ Segm(i+1) by XBOOLE_1:49 .= NAT \ Segm(i+1); for z being set holds z in Z iff z in rng(a|(NAT \ Segm(i+1))) proof let z be set; hereby assume z in Z; then consider z' be Element of omega such that A94: z=z' & ex j being Element of NAT st a.j=z' & j>i; consider j be Element of NAT such that A95: a.j=z & j>i by A94; j>=i+1 by NAT_1:13,A95; then not j in i+1 by NAT_1:45; then j in dom a & j in (NAT \ Segm(i+1)) by A91,XBOOLE_0:def 4; hence z in rng(a|(NAT \ Segm(i+1))) by A95,FUNCT_1:73; end; assume z in rng(a|(NAT \ Segm(i+1))); then consider j be set such that A96: j in dom(a|(NAT \ Segm(i+1))) & z =(a|(NAT \ Segm(i+1))).j by FUNCT_1:def 5; reconsider j as Element of NAT by A96; not j in Segm(i+1) by A96,A93,XBOOLE_0:def 4; then j>=i+1 by NAT_1:45; then a.j=z & j>i by A96,FUNCT_1:70,NAT_1:13; hence z in Z; end; then A97: Z = rng(a|(NAT \ Segm(i+1))) by TARSKI:2; A98: a|(NAT \ Segm(i+1)) is one-to-one by A90,FUNCT_1:84; now let z be set; assume z in Z; then consider z' be Element of omega such that A99: z=z' & ex j being Element of NAT st a.j=z' & j>i; thus z in NAT by A99; end; then A100: Z c= NAT by TARSKI:def 3; dom(a|(NAT \ Segm(i+1))) is infinite by A93,Th4; hence Card Z = omega by A97,A100,Th2,A98,CARD_1:97; end; defpred P4[set,set] means for Y being set, i being Element of NAT, Fi being Function of the_subsets_of_card(n,S.i\{a.i}),k st i=$1 & Y = {x where x is Element of omega: ex j being Element of NAT st a.j=x & j>i} & (for Y' being Element of the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y' = F.(Y' \/ {a.i})) holds ex l being natural number st l=$2 & l in k & rng(Fi|the_subsets_of_card(n,Y)) = {l}; A101: for x being set st x in NAT ex y being set st y in k & P4[x,y] proof let x be set; assume x in NAT; then reconsider i' = x as Element of NAT; set Y' = S.i'; reconsider a' = a.i' as Element of Y' by A56; Y' in A; then consider Y'' be Subset of X such that A102: Y''=Y' & Card Y'' = omega; consider Fa be Function of the_subsets_of_card(n,Y'\{a'}),k, Ha be Subset of Y'\{a'} such that A103: Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant & for Y'' being Element of the_subsets_of_card(n,Y'\{a'}) holds Fa.Y'' = F.(Y'' \/ {a'}) by A102,A11; set Z = {x' where x' is Element of omega: ex j being Element of NAT st a.j=x' & j>i'}; A104: Z c= S.(i'+1) & Fa|the_subsets_of_card(n,Z) is constant by A70,A103; A105: a.i' in a.(i'+1) & S.(i'+1) c= S.i' & a.i' in S.i' & a.(i'+1) in S.(i'+1) & not a.i' in S.(i'+1) by A56; now let x be set; assume x in Z; then A106: x in S.(i'+1) by A104; not x in {a.i'} by A106,A105,TARSKI:def 1; hence x in S.i'\{a.i'} by A106,A105,XBOOLE_0:def 4; end; then Z c= S.i'\{a.i'} by TARSKI:def 3; then A107: the_subsets_of_card(n,Z) c= the_subsets_of_card(n,Y'\{a'}) by Lm1; A108: Fa|the_subsets_of_card(n,Z) is Function of the_subsets_of_card(n,Z),k by A10,A107,FUNCT_2:38; Card Z = omega by A92; then Card n c= Card Z & Z is non empty by CARD_4:13,CARD_1:47; then the_subsets_of_card(n,Z) is non empty by GROUP_10:2; then consider y be Element of k such that A109: rng(Fa|the_subsets_of_card(n,Z)) = {y} by A10,A108,A104,Lm4; reconsider y as set; take y; thus A110: y in k by A10; thus P4[x,y] proof thus for Y being set, i being Element of NAT, Fi being Function of the_subsets_of_card(n,S.i\{a.i}),k st i=x & Y = {x' where x' is Element of omega: ex j being Element of NAT st a.j=x' & j>i} & (for Y' being Element of the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y' = F.(Y' \/ {a.i})) holds ex l being natural number st l=y & l in k & rng(Fi|the_subsets_of_card(n,Y)) = {l} proof let Y be set; let i be Element of NAT; let Fi be Function of the_subsets_of_card(n,S.i\{a.i}),k; assume A111: i=x; assume A112: Y = {x' where x' is Element of omega: ex j being Element of NAT st a.j=x' & j>i}; assume A113: for Y' being Element of the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y' = F.(Y' \/ {a.i}); reconsider k'=k as Element of NAT by ORDINAL1:def 13; k' is Subset of NAT by STIRL2_1:8; then reconsider l=y as natural number by A110,ORDINAL1:def 13; take l; thus l=y; thus l in k by A10; for x1' being Element of the_subsets_of_card(n,S.i\{a.i}) holds Fa.x1' = Fi.x1' proof let x1' be Element of the_subsets_of_card(n,S.i\{a.i}); thus Fa.x1' = F.(x1' \/ {a.i}) by A111,A103 .= Fi.x1' by A113; end; hence rng(Fi|the_subsets_of_card(n,Y)) = {l} by A109,A112,A111,FUNCT_2:113; end; end; end; consider g be Function of NAT,k such that A114: for x being set st x in NAT holds P4[x,g.x] from FUNCT_2:sch 1(A101); A115: dom g is infinite by A10,FUNCT_2:def 1; g in Funcs(NAT,k) by A10,FUNCT_2:11; then consider g' be Function such that A116: g=g' & dom g' = NAT & rng g' c= k by FUNCT_2:def 2; rng g is finite by A116,FINSET_1:13; then consider k' be set such that A117: k' in rng g & g"{k'} is infinite by A115,COMPL_SP:24; set H = a.:(g"{k'}); A118: g"{k'} c= dom g by RELAT_1:167; g"{k'}, H are_equipotent by A90,A91,CARD_1:60,A118,XBOOLE_1:1; then A119: Card(g"{k'}) = Card H by CARD_1:21; A120: Card(g"{k'}) is infinite by A117,CARD_4:1; now let y be set; assume y in H; then consider x be set such that A121: [x,y] in a & x in g"{k'} by RELAT_1:def 13; A122: x in dom a & y = a.x by A121,FUNCT_1:8; then reconsider i=x as Element of NAT; A123: y in S.i by A122,A56; S.i in the_subsets_of_card(omega,X); then consider Xi be Subset of X such that A124: S.i=Xi & Card Xi = omega; thus y in X by A124,A123; end; then reconsider H as Subset of X by TARSKI:def 3; take H; thus H is infinite by A120,A119,CARD_4:1; A125: for y being set st y in dom(F|the_subsets_of_card(n+1,H)) holds F|the_subsets_of_card(n+1,H).y = k' proof let y be set; assume y in dom(F|the_subsets_of_card(n+1,H)); then A126: y in dom F & y in the_subsets_of_card(n+1,H) by RELAT_1:86; then consider Y be Subset of H such that A127: y=Y & Card Y = n+1; set y0 = min* Y; Y c= X by XBOOLE_1:1; then A128: Y c= NAT by A9,XBOOLE_1:1; then A129: y0 in Y & for k being Element of NAT st k in Y holds y0 <= k by A127,NAT_1:def 1,CARD_1:47; then consider x0 be set such that A130: x0 in dom a & x0 in g"{k'} & y0 = a.x0 by FUNCT_1:def 12; consider y0' be set such that A131: y0' in rng g & [x0,y0'] in g & y0' in {k'} by A130,RELAT_1:166; A132: x0 in dom g & g.x0 = y0' by A131,FUNCT_1:8; reconsider x0 as Element of NAT by A132; reconsider a' = a.x0 as Element of S.x0 by A56; S.x0 in the_subsets_of_card(omega,X); then consider S0 be Subset of X such that A133: S0=S.x0 & Card S0 = omega; consider F0 be Function of the_subsets_of_card(n,S.x0\{a'}),k, H0 be Subset of S.x0\{a'} such that A134: H0 is infinite & F0|the_subsets_of_card(n,H0) is constant & for Y' being Element of the_subsets_of_card(n,S.x0\{a'}) holds F0.Y' = F.(Y' \/ {a'}) by A11,A133; set Y0 = {x where x is Element of omega: ex j being Element of NAT st a.j=x & j>x0}; consider l be natural number such that A135: l=g.x0 & l in k & rng(F0|the_subsets_of_card(n,Y0)) = {l} by A114,A134; A136: rng(F0|the_subsets_of_card(n,Y0)) = {k'} by A135,A132,A131,TARSKI:def 1; set Y' = y \ {y0}; A137: Y0 c= S.(x0+1) & F0|the_subsets_of_card(n,Y0) is constant by A70,A134; A138: a.x0 in a.(x0+1) & S.(x0+1) c= S.x0 & a.x0 in S.x0 & a.(x0+1) in S.(x0+1) & not a.x0 in S.(x0+1) by A56; A139: not a.x0 in Y0 by A137,A56; Y0 c= S.x0 by A137,A138,XBOOLE_1:1; then Y0\{a.x0} c= S.x0\{a.x0} by XBOOLE_1:33; then Y0 c= S.x0\{a.x0} by A139,ZFMISC_1:65; then A140: the_subsets_of_card(n,Y0) c= the_subsets_of_card(n,S.x0\{a.x0}) by Lm1; now let x be set; assume A141: x in Y'; then A142: x in y & not x in {y0} by XBOOLE_0:def 4; consider j be set such that A143: j in dom a & j in g"{k'} & x = a.j by A142,A127,FUNCT_1:def 12; reconsider x'=x as Element of omega by A142,A127,A128; ex j being Element of NAT st a.j=x' & j>x0 proof reconsider j as Element of NAT by A143; take j; thus a.j=x' by A143; A144: y0 <= x' by A128,A141,A127,NAT_1:def 1; thus j>x0 proof assume A145: x0>=j; x0<>j by A143,A142,A130,TARSKI:def 1; hence contradiction by A144,A130,A145,A143,A67; end; end; hence x in Y0; end; then A146: Y' is Subset of Y0 by TARSKI:def 3; A147: {y0} c= y by A127,A129,ZFMISC_1:37; A148: Y' \/ {a.x0} = y by A130,A147,XBOOLE_1:45; reconsider y'=y as finite set by A127,CARD_4:1; Card Y' c= Card y' by CARD_1:27; then reconsider Y''=Y' as finite set by CARD_2:68; y0 in {y0} by TARSKI:def 1; then A149: not a.x0 in Y' by A130,XBOOLE_0:def 4; card y' = card Y'' + 1 by A148,A149,CARD_2:54; then A150: Y' in the_subsets_of_card(n,Y0) by A127,A146; then A151: Y' in the_subsets_of_card(n,S.x0\{a.x0}) by A140; reconsider Y' as Element of the_subsets_of_card(n,S.x0\{a.x0}) by A140,A150; Y' in dom F0 by A10,FUNCT_2:def 1,A151; then Y' in dom(F0|the_subsets_of_card(n,Y0)) by A150,RELAT_1:86; then F0|the_subsets_of_card(n,Y0).Y' in rng(F0|the_subsets_of_card(n,Y0)) by FUNCT_1:12; then F0|the_subsets_of_card(n,Y0).Y' = k' by A136,TARSKI:def 1; then A152: F0.Y' = k' by A150,FUNCT_1:72; F0.Y' = F.(Y' \/ {a.x0}) by A134; hence F|the_subsets_of_card(n+1,H).y = k' by A152,A148,A126,FUNCT_1:72; end; for x,y being set st x in dom(F|the_subsets_of_card(n+1,H)) & y in dom(F|the_subsets_of_card(n+1,H)) holds F|the_subsets_of_card(n+1,H).x = F|the_subsets_of_card(n+1,H).y proof let x,y be set; assume x in dom(F|the_subsets_of_card(n+1,H)); then A153: F|the_subsets_of_card(n+1,H).x = k' by A125; assume y in dom(F|the_subsets_of_card(n+1,H)); hence thesis by A153,A125; end; hence F|the_subsets_of_card(n+1,H) is constant by FUNCT_1:def 16; end; hence thesis; end; for n being natural number holds P[n] from NAT_1:sch 2(A1,A6); hence thesis; end; theorem the_subsets_of_card(0,X) = {0} by Lm2; theorem Th6: for X being finite set st card X < n holds the_subsets_of_card(n, X) is empty proof let X be finite set; assume A1: card X < n; assume the_subsets_of_card(n, X) is not empty; then consider x be set such that A2: x in the_subsets_of_card(n, X) by XBOOLE_0:def 1; consider X' be Subset of X such that A3: x=X' & Card X' = n by A2; A4: Card Seg n = n by FINSEQ_1:78; Card Seg n c= Card X by A3,A4,CARD_1:27; then card Seg n <= card X by CARD_2:57; hence contradiction by A1,FINSEQ_1:78; end; theorem X c= Y implies the_subsets_of_card(Z,X) c= the_subsets_of_card(Z,Y) by Lm1; theorem X is finite & Y is finite & Card Y = X implies the_subsets_of_card(X,Y) = {Y} by Lm3; theorem X is non empty & Y is non empty implies (f is constant iff ex y being Element of Y st rng f = {y}) by Lm4; theorem Th10: for X being finite set st k <= card X holds ex Y being Subset of X st card Y = k proof let X be finite set; assume k <= card X; then card k <= card X by CARD_1:66; then Card k c= Card X by CARD_2:57; then consider Y be set such that A1: Y c= X & Card Y = Card k by CARD_FIL:36; reconsider Y as Subset of X by A1; take Y; thus card Y = k by A1,CARD_1:66; end; theorem Th11: m>=1 implies n+1 <= (n+m) choose m proof defpred Q[Nat] means for n being Element of NAT st $1>=1 holds n+1 <= (n+$1) choose $1; A1: Q[0]; A2: for k being Element of NAT st Q[k] holds Q[k+1] proof let k be Element of NAT; assume A3: Q[k]; set k'=k+1; reconsider k' as Element of NAT by ORDINAL1:def 13; for n being Element of NAT st k'>=1 holds n+1 <= (n+k') choose k' proof let n be Element of NAT; assume A4: k'>=1; per cases by A4,NAT_1:8; suppose A5: k+1=1; n+1 >= 0+1 by XREAL_1:8; hence n+1 <= (n+k') choose k' by A5,NEWTON:33; end; suppose k>=1; then A6: n+1 <= (n+k) choose k by A3; A7: (n+k') choose k' = (n+k+1) choose (k+1) .= (n+k) choose (k+1) + (n+k) choose k by NEWTON:32; A8: (n+1) + (n+k) choose (k+1) <= (n+k') choose k' by A7,A6,XREAL_1:8; 0+(n+1) <= (n+k) choose (k+1) + (n+1) by XREAL_1:8; hence n+1 <= (n+k') choose k' by A8,XXREAL_0:2; end; end; hence thesis; end; A9: for k being Element of NAT holds Q[k] from NAT_1:sch 1(A1,A2); assume A10: m >= 1; reconsider m'=m as Element of NAT by ORDINAL1:def 13; reconsider n'=n as Element of NAT by ORDINAL1:def 13; n'+1 <= (n'+m') choose m' by A9,A10; hence thesis; end; theorem Th12: m>=1 & n>=1 implies m+1 <= (n+m) choose m proof defpred Q[Nat] means for n being Element of NAT st $1>=1 & n>=1 holds $1+1 <= (n+$1) choose $1; A1: Q[0]; A2: for k being Element of NAT st Q[k] holds Q[k+1] proof let k be Element of NAT; assume A3: Q[k]; set k'=k+1; reconsider k' as Element of NAT by ORDINAL1:def 13; for n being Element of NAT st k'>=1 & n>=1 holds k'+1 <= (n+k') choose k' proof let n be Element of NAT; assume A4: k'>=1; assume A5: n>=1; per cases by A4,NAT_1:8; suppose A6: k+1=1; A7: n+1 >= 0+1 by XREAL_1:8; n+1 >= 1+1 by A5,XREAL_1:8; hence k'+1 <= (n+k') choose k' by A6,A7,NEWTON:33; end; suppose k>=1; then A8: k+1 <= (n+k) choose k by A5,A3; A9: (n+k') choose k' = (n+k+1) choose (k+1) .= (n+k) choose (k+1) + (n+k) choose k by NEWTON:32; A10: (k+1) + (n+k) choose (k+1) <= (n+k') choose k' by A9,A8,XREAL_1:8; n-1 >= 1-1 by A5,XREAL_1:11; then A11: n -' 1 = n - 1 by BINARITH:def 3; set k''=k+1; k+1>=0+1 by XREAL_1:8; then (n-'1) +1 <= (n-'1+k'') choose k'' by Th11; then 1 <= (n+k) choose (k+1) by A11,A5,XXREAL_0:2; then 1+(k+1) <= (n+k) choose (k+1) + (k+1) by XREAL_1:8; hence k'+1 <= (n+k') choose k' by A10,XXREAL_0:2; end; end; hence thesis; end; A12: for k being Element of NAT holds Q[k] from NAT_1:sch 1(A1,A2); assume A13: m >= 1 & n >= 1; reconsider m'=m as Element of NAT by ORDINAL1:def 13; reconsider n'=n as Element of NAT by ORDINAL1:def 13; m'+1 <= (n'+m') choose m' by A12,A13; hence thesis; end; theorem Th13: for X being non empty set, p1,p2 being Element of X, P being a_partition of X, A being Element of P st p1 in A & (proj P).p1=(proj P).p2 holds p2 in A proof let X be non empty set; let p1,p2 be Element of X; let P be a_partition of X; let A be Element of P; assume A1: p1 in A; assume (proj P).p1=(proj P).p2; then A2: (proj P).p2 = A by A1,BORSUK_1:29; assume A3: not p2 in A; union P = X by EQREL_1:def 6; then consider B be set such that A4: p2 in B & B in P by TARSKI:def 4; reconsider B as Element of P by A4; A5: (proj P).p2 = B by A4,BORSUK_1:29; per cases by EQREL_1:def 6; suppose A=B; hence contradiction by A3,A4; end; suppose A misses B; then A /\ A = {} by A2,A5,XBOOLE_0:def 7; hence contradiction by EQREL_1:def 6; end; end; begin :: Infinite Ramsey Theorem theorem Th14: for F being Function of the_subsets_of_card(n,X),k st k<>0 & X is infinite holds ex H st H is infinite & F|the_subsets_of_card(n,H) is constant proof let F be Function of the_subsets_of_card(n,X),k; assume A1: k<>0 & X is infinite; consider Y be set such that A2: Y c= X & Card Y = alef 0 by A1,CARD_4:14; reconsider Y as non empty set by A2,CARD_1:47; Y,omega are_equipotent by CARD_1:21,A2,CARD_1:38; then consider f be Function such that A3: f is one-to-one & dom f = omega & rng f = Y by WELLORD2:def 4; reconsider f as Function of omega,Y by A3,FUNCT_2:3; set F' = F * (f||^n); F in Funcs(the_subsets_of_card(n,X),k) by A1,FUNCT_2:11; then consider g1 be Function such that A4: F=g1 & dom g1=the_subsets_of_card(n,X) & rng g1 c= k by FUNCT_2:def 2; Card omega is infinite by CARD_4:1; then A5: Card n c= Card omega by CARD_4:13; Card n c= Card Y by A2,CARD_4:13; then the_subsets_of_card(n,Y) is non empty by GROUP_10:2; then f||^n in Funcs(the_subsets_of_card(n,omega), the_subsets_of_card(n,Y)) by FUNCT_2:11; then consider g2 be Function such that A6: f||^n=g2 & dom g2=the_subsets_of_card(n,omega) & rng g2 c= the_subsets_of_card(n,Y) by FUNCT_2:def 2; the_subsets_of_card(n,Y) c= the_subsets_of_card(n,X) by A2,Lm1; then A7: dom F' = the_subsets_of_card(n,omega) by RELAT_1:46,A6,A4,XBOOLE_1:1; A8: rng F' c= rng F by RELAT_1:45; then A9: rng F' c= k by A4,XBOOLE_1:1; reconsider F' as Function of the_subsets_of_card(n,omega),k by A8,A7,FUNCT_2:4,A4,XBOOLE_1:1; consider H' be Subset of omega such that A10: H' is infinite & F'|the_subsets_of_card(n,H') is constant by A1,Lm5,CARD_1:84; Card H' is infinite by A10,CARD_4:1; then Card n c= Card H' by CARD_4:13; then A11: the_subsets_of_card(n,H') is non empty by A10,GROUP_10:2; A12: dom(F'|the_subsets_of_card(n,H')) = the_subsets_of_card(n,H') by A7,RELAT_1:91,Lm1; rng(F'|the_subsets_of_card(n,H')) c= rng F' by RELAT_1:99; then F'|the_subsets_of_card(n,H') is Function of the_subsets_of_card(n,H'),k by A12,FUNCT_2:4,A9,XBOOLE_1:1; then consider y be Element of k such that A13: rng(F'|the_subsets_of_card(n,H')) = {y} by A10,A11,A1,Lm4; set H = f .: H'; A14: f .: H' c= rng f by RELAT_1:144; reconsider H as Subset of X by A2,A3,A14,XBOOLE_1:1; take H; H',f.:H' are_equipotent by A3,CARD_1:60; hence A15: H is infinite by A10,CARD_1:68; Card H is infinite by A15,CARD_4:1; then Card n c= Card H by CARD_4:13; then A16: the_subsets_of_card(n,H) is non empty by A15,GROUP_10:2; A17: dom(F|the_subsets_of_card(n,H)) = the_subsets_of_card(n,H) by Lm1,A4,RELAT_1:91; rng(F|the_subsets_of_card(n,H)) c= rng F by RELAT_1:99; then A18: F|the_subsets_of_card(n,H) is Function of the_subsets_of_card(n,H),k by A17,FUNCT_2:4,A4,XBOOLE_1:1; ex y being Element of k st rng(F|the_subsets_of_card(n,H)) = {y} proof take y; thus rng(F|the_subsets_of_card(n,H)) = F.:the_subsets_of_card(n,H) by RELAT_1:148 .= F.:((f||^n) .: the_subsets_of_card(n,H')) by A3,A5,Th1 .= F' .: the_subsets_of_card(n,H') by RELAT_1:159 .= {y} by A13,RELAT_1:148; end; hence F|the_subsets_of_card(n,H) is constant by A16,A1,A18,Lm4; end; :: theorem 9.1 Set Theory T.Jech theorem for X being infinite set, P being a_partition of the_subsets_of_card(n,X) st Card P = k holds ex H being Subset of X st H is infinite & H is_homogeneous_for P proof let X be infinite set; let P be a_partition of the_subsets_of_card(n,X); assume Card P = k; then A1: P,k are_equipotent by CARD_1:def 5; then consider F1 be Function such that A2: F1 is one-to-one & dom F1 = P & rng F1 = k by WELLORD2:def 4; reconsider F1 as Function of P,k by A2,FUNCT_2:3; set F=F1*proj P; reconsider F as Function of the_subsets_of_card(n,X),k; A3: k<>0 by A1,CARD_1:46; consider H be Subset of X such that A4: H is infinite & F|the_subsets_of_card(n,H) is constant by A3,Th14; take H; thus H is infinite by A4; consider h be Element of the_subsets_of_card(n,H); A5: the_subsets_of_card(n,H) c= the_subsets_of_card(n,X) by Lm1; Card H is infinite by A4,CARD_4:1; then Card n c= Card H by CARD_4:13; then A6: the_subsets_of_card(n,H) is non empty by A4,GROUP_10:2; then h in the_subsets_of_card(n,H); then reconsider h as Element of the_subsets_of_card(n,X) by A5; set E = EqClass(h,P); reconsider E as Element of P by EQREL_1:def 8; for x being set holds x in the_subsets_of_card(n,H) implies x in E proof let x be set; assume A7: x in the_subsets_of_card(n,H); then reconsider x'=x as Element of the_subsets_of_card(n,X) by A5; A8: h in E by EQREL_1:def 8; k <> {} by A1,CARD_1:46; then A9: dom F = the_subsets_of_card(n,X) by FUNCT_2:def 1; x' in dom F /\ the_subsets_of_card(n,H) by A9,A7,XBOOLE_0:def 3; then A10: x' in dom(F|the_subsets_of_card(n,H)) by RELAT_1:90; h in dom F /\ the_subsets_of_card(n,H) by A9,A6,XBOOLE_0:def 3; then A11: h in dom(F|the_subsets_of_card(n,H)) by RELAT_1:90; A12: F.x' = F|the_subsets_of_card(n,H).x' by A7,FUNCT_1:72 .= F|the_subsets_of_card(n,H).h by A4,A10,A11,FUNCT_1:def 16 .= F.h by A6,FUNCT_1:72; F1.((proj P).x') = (F1*proj P).h by A12,A9,FUNCT_1:22 .= F1.((proj P).h) by A9,FUNCT_1:22; then (proj P).h = (proj P).x' by A2,FUNCT_1:def 8; hence x in E by A8,Th13; end; then the_subsets_of_card(n,H) c= E by TARSKI:def 3; hence H is_homogeneous_for P by Def1; end; begin :: Ramsey's Theorem scheme BinInd2 { P[natural number,natural number] } : P[m,n] provided A1: P[0,n] & P[n,0] and A2: P[m+1,n] & P[m,n+1] implies P[m+1,n+1] proof defpred Q[Nat] means for m,n being natural number st m+n=$1 holds P[m,n]; A3: Q[0] proof let m,n be natural number; assume m+n=0; then m=0 & n=0 by NAT_1:7; hence P[m,n] by A1; end; A4: for k being Element of NAT st Q[k] holds Q[k+1] proof let k be Element of NAT; assume A5: Q[k]; for m,n being natural number st m+n=k+1 holds P[m,n] proof let m,n be natural number; assume A6: m+n=k+1; per cases; suppose m=0 or n=0; hence P[m,n] by A1; end; suppose A7: m<>0 & n<>0; then 0 < n; then reconsider n'=n-1 as Element of NAT by NAT_1:20; A8: m+n'=k by A6; 0 < m by A7; then reconsider m'=m-1 as Element of NAT by NAT_1:20; m'+n=k by A6; then P[m',n'+1] & P[m'+1,n'] by A5,A8; hence P[m,n] by A2; end; end; hence thesis; end; A9: for k being Element of NAT holds Q[k] from NAT_1:sch 1(A3,A4); let m,n; set k=m+n; reconsider k as Element of NAT by ORDINAL1:def 13; Q[k] by A9; hence thesis; end; :: Chapter 35 proof from THE BOOK Aigner-Ziegler theorem Th16: m >= 2 & n >= 2 implies ex r being natural number st r <= (m + n -' 2) choose (m -' 1) & r >= 2 & for X being finite set, F being Function of the_subsets_of_card(2,X), Seg 2 st card X >= r holds ex S being Subset of X st (card S >= m & rng(F|the_subsets_of_card(2,S)) = {1}) or (card S >= n & rng(F|the_subsets_of_card(2,S)) = {2}) proof defpred P[natural number,natural number] means $1 >= 2 & $2 >= 2 implies ex r being natural number st r <= ($1 + $2 -' 2) choose ($1 -' 1) & r >= 2 & for X being finite set, F being Function of the_subsets_of_card(2,X), Seg 2 st card X >= r holds ex S being Subset of X st (card S >= $1 & rng(F|the_subsets_of_card(2,S)) = {1}) or (card S >= $2 & rng(F|the_subsets_of_card(2,S)) = {2}); A1: for n being natural number holds P[0,n] & P[n,0]; A2: for m,n being natural number st P[m+1,n] & P[m,n+1] holds P[m+1,n+1] proof let m,n be natural number; assume A3: P[m+1,n]; assume A4: P[m,n+1]; assume A5: m+1 >= 2 & n+1 >= 2; per cases by XXREAL_0:1; suppose m+1<2 or n+1<2; hence thesis by A5; end; suppose A6: m+1=2; set r=n+1; take r; (m+1)+(n+1) >= 2+2 by A5,XREAL_1:9; then A7: (m+1)+(n+1)-2 >= 4-2 by XREAL_1:11; A8: m+n = (m+1) + (n+1) -' 2 by A7,BINARITH:def 3; A9: (m+1) -' 1 = m by BINARITH:39; m+1-1 >= 2-1 by A5,XREAL_1:11; hence r <= ((m+1) + (n+1) -' 2) choose ((m+1) -' 1) by A8,A9,Th11; thus r >= 2 by A5; let X be finite set; let F be Function of the_subsets_of_card(2,X), Seg 2; assume A10: card X >= r; F in Funcs(the_subsets_of_card(2,X), Seg 2) by FINSEQ_1:4,FUNCT_2:11; then consider f be Function such that A11: F = f & dom f = the_subsets_of_card(2,X) & rng f c= Seg 2 by FUNCT_2:def 2; per cases; suppose A12: not 1 in rng F; consider S be Subset of X such that A13: card S = r by A10,Th10; A14: the_subsets_of_card(2,S) c= the_subsets_of_card(2,X) by Lm1; card 2 <= card S by A5,A13,CARD_1:66; then A15: Card 2 c= Card S by CARD_2:57; the_subsets_of_card(2,S) is non empty by A15,GROUP_10:2,A13,CARD_1:78; then consider x be set such that A16: x in the_subsets_of_card(2,S) by XBOOLE_0:def 1; A17: F|the_subsets_of_card(2,S) <> {} by A11,A16,A14,RELAT_1:86,RELAT_1:60; A18: rng(F|the_subsets_of_card(2,S)) c= rng F by RELAT_1:99; then A19: rng(F|the_subsets_of_card(2,S)) c= {1,2} by A11,FINSEQ_1:4,XBOOLE_1:1; A20: now let x be set; hereby assume A21: x in rng(F|the_subsets_of_card(2,S)); then x=1 or x=2 by A19,TARSKI:def 2; hence x=2 by A21,A12,A18; end; assume A22: x=2; assume not x in rng(F|the_subsets_of_card(2,S)); then A23: not 2 in rng(F|the_subsets_of_card(2,S)) & not 1 in rng(F|the_subsets_of_card(2,S)) by A22,A12,A18; rng(F|the_subsets_of_card(2,S)) = {} or rng(F|the_subsets_of_card(2,S)) = {1} or rng(F|the_subsets_of_card(2,S)) = {2} or rng(F|the_subsets_of_card(2,S)) = {1,2} by A19,ZFMISC_1:42; hence contradiction by A17,RELAT_1:64,A23,TARSKI:def 1,def 2; end; take S; thus thesis by A20,A13,TARSKI:def 1; end; suppose 1 in rng F; then consider S be set such that A24: S in dom F & 1 = F.S by FUNCT_1:def 5; S in {X' where X' is Subset of X: Card X' = 2} by A24; then consider X' be Subset of X such that A25: S=X' & Card X' = 2; reconsider S as Subset of X by A25; A26: {S} c= dom F by A24,ZFMISC_1:37; the_subsets_of_card(2,S) = {S} by A25,Lm3; then S in the_subsets_of_card(2,S) by TARSKI:def 1; then A27: F|the_subsets_of_card(2,S).S = 1 by A24,FUNCT_1:72; A28: dom(F|the_subsets_of_card(2,S)) = dom F /\ the_subsets_of_card(2,S) by FUNCT_1:68 .= dom F /\ {S} by A25,Lm3 .= {S} by A26,XBOOLE_1:28; take S; thus thesis by A6,A28,A25,A27,FUNCT_1:14; end; end; suppose A29: n+1=2; set r=m+1; take r; (m+1)+(n+1) >= 2+2 by A5,XREAL_1:9; then A30: (m+1)+(n+1)-2 >= 4-2 by XREAL_1:11; A31: m+n = (m+1) + (n+1) -' 2 by A30,BINARITH:def 3; A32: (m+1) -' 1 = m by BINARITH:39; A33: m+1-1 >= 2-1 by A5,XREAL_1:11; n+1-1 >= 2-1 by A5,XREAL_1:11; hence r <= ((m+1) + (n+1) -' 2) choose ((m+1) -' 1) by A31,A32,A33,Th12; thus r >= 2 by A5; let X be finite set; let F be Function of the_subsets_of_card(2,X), Seg 2; assume A34: card X >= r; F in Funcs(the_subsets_of_card(2,X), Seg 2) by FINSEQ_1:4,FUNCT_2:11; then consider f be Function such that A35: F = f & dom f = the_subsets_of_card(2,X) & rng f c= Seg 2 by FUNCT_2:def 2; per cases; suppose A36: not 2 in rng F; consider S be Subset of X such that A37: card S = r by A34,Th10; A38: the_subsets_of_card(2,S) c= the_subsets_of_card(2,X) by Lm1; card 2 <= card S by A5,A37,CARD_1:66; then A39: Card 2 c= Card S by CARD_2:57; the_subsets_of_card(2,S) is non empty by A39,GROUP_10:2,A37,CARD_1:78; then consider x be set such that A40: x in the_subsets_of_card(2,S) by XBOOLE_0:def 1; A41: F|the_subsets_of_card(2,S) <> {} by A35,A40,A38,RELAT_1:86,RELAT_1:60; A42: rng(F|the_subsets_of_card(2,S)) c= rng F by RELAT_1:99; then A43: rng(F|the_subsets_of_card(2,S)) c= {1,2} by A35,FINSEQ_1:4,XBOOLE_1:1; A44: now let x be set; hereby assume A45: x in rng(F|the_subsets_of_card(2,S)); then x=1 or x=2 by A43,TARSKI:def 2; hence x=1 by A45,A36,A42; end; assume A46: x=1; assume not x in rng(F|the_subsets_of_card(2,S)); then A47: not 2 in rng(F|the_subsets_of_card(2,S)) & not 1 in rng(F|the_subsets_of_card(2,S)) by A46,A36,A42; rng(F|the_subsets_of_card(2,S)) = {} or rng(F|the_subsets_of_card(2,S)) = {1} or rng(F|the_subsets_of_card(2,S)) = {2} or rng(F|the_subsets_of_card(2,S)) = {1,2} by A43,ZFMISC_1:42; hence contradiction by A41,RELAT_1:64,A47,TARSKI:def 1,def 2; end; take S; thus thesis by A44,A37,TARSKI:def 1; end; suppose 2 in rng F; then consider S be set such that A48: S in dom F & 2 = F.S by FUNCT_1:def 5; S in {X' where X' is Subset of X: Card X' = 2} by A48; then consider X' be Subset of X such that A49: S=X' & Card X' = 2; reconsider S as Subset of X by A49; A50: {S} c= dom F by A48,ZFMISC_1:37; the_subsets_of_card(2,S) = {S} by A49,Lm3; then S in the_subsets_of_card(2,S) by TARSKI:def 1; then A51: F|the_subsets_of_card(2,S).S = 2 by A48,FUNCT_1:72; A52: dom(F|the_subsets_of_card(2,S)) = dom F /\ the_subsets_of_card(2,S) by FUNCT_1:68 .= dom F /\ {S} by A49,Lm3 .= {S} by A50,XBOOLE_1:28; take S; thus thesis by A29,A52,A49,A51,FUNCT_1:14; end; end; suppose A53: m+1>2 & n+1>2; consider r1 be natural number such that A54: r1 <= ((m+1) + n -' 2) choose ((m+1) -' 1) and A55: r1 >= 2 and A56: for X being finite set, F being Function of the_subsets_of_card(2,X), Seg 2 st card X >= r1 holds ex S being Subset of X st (card S >= m+1 & rng(F|the_subsets_of_card(2,S)) = {1}) or (card S >= n & rng(F|the_subsets_of_card(2,S)) = {2}) by A3,A53,NAT_1:13; consider r2 be natural number such that A57: r2 <= (m + (n+1) -' 2) choose (m -' 1) and r2 >= 2 and A58: for X being finite set, F being Function of the_subsets_of_card(2,X), Seg 2 st card X >= r2 holds ex S being Subset of X st (card S >= m & rng(F|the_subsets_of_card(2,S)) = {1}) or (card S >= n+1 & rng(F|the_subsets_of_card(2,S)) = {2}) by A4,A53,NAT_1:13; set r = r1+r2; take r; set s = m -' 1; set t = m + n -' 1; m + 1 - 2 >= 2 - 2 by A5,XREAL_1:11; then A59: m -' 1 = m - 1 by BINARITH:def 3; (m+1) + (n+1) >= 2+2 by A5,XREAL_1:9; then A60: m+n+2-3 >= 4-3 by XREAL_1:11; A61: m + n -' 1 = m + n - 1 by A60,BINARITH:def 3; A62: m + n + 1 -' 2 = m + n + 1 - 2 by A60,BINARITH:def 3; m + n >= 0; then A63: (m+1) + (n+1) -' 2 = (m+1) + (n+1) - 2 by BINARITH:def 3 .= t + 1 by A61; A64: (m+1) -' 1 = s + 1 by A59,BINARITH:39; r1+r2 <= ((m+1) + n -' 2) choose ((m+1) -' 1) + (m + (n+1) -' 2) choose (m -' 1) by A54,A57,XREAL_1:9; hence r <= ((m+1) + (n+1) -' 2) choose ((m+1) -' 1) by A63,A62,A61,A64,NEWTON:32; A65: r1 + r2 >= 0 + 2 by A55,XREAL_1:9; hence r >= 2; let X be finite set; let F be Function of (the_subsets_of_card(2,X)), Seg 2; assume card X >= r; then consider S be Subset of X such that A66: card S = r by Th10; F in Funcs(the_subsets_of_card(2,X), Seg 2) by FINSEQ_1:4,FUNCT_2:11; then consider f be Function such that A67: F = f & dom f = the_subsets_of_card(2,X) & rng f c= Seg 2 by FUNCT_2:def 2; consider s be set such that A68: s in S by XBOOLE_0:def 1,A66,A65,CARD_1:78; set A = {s' where s' is Element of S: F.{s,s'} = 1 & {s,s'} in dom F}; set B = {s' where s' is Element of S: F.{s,s'} = 2 & {s,s'} in dom F}; A69: S \ {s} c= S by XBOOLE_1:36; A70: now assume A /\ B <> {}; then consider x be set such that A71: x in A /\ B by XBOOLE_0:def 1; A72: x in A & x in B by A71,XBOOLE_0:def 3; then consider s1 be Element of S such that A73: x = s1 & F.{s,s1} = 1 & {s,s1} in dom F; consider s2 be Element of S such that A74: x = s2 & F.{s,s2} = 2 & {s,s2} in dom F by A72; thus contradiction by A73,A74; end; A75: for x being set holds x in A \/ B iff x in S \ {s} proof let x be set; hereby assume A76: x in A \/ B; per cases by A76,XBOOLE_0:def 2; suppose x in A; then consider s' be Element of S such that A77: x = s' & F.{s,s'} = 1 & {s,s'} in dom F; now assume x in {s}; then A78: x = s by TARSKI:def 1; {s,s'} = {s} \/ {s'} by ENUMSET1:41 .= {s} by A77,A78; then {s} in the_subsets_of_card(2,X) by A77; then consider X' be Subset of X such that A79: X'={s} & Card X' = 2; thus contradiction by A79,CARD_1:50; end; hence x in S \ {s} by A66,A65,CARD_1:78,A77,XBOOLE_0:def 4; end; suppose x in B; then consider s' be Element of S such that A80: x = s' & F.{s,s'} = 2 & {s,s'} in dom F; now assume x in {s}; then A81: x = s by TARSKI:def 1; {s,s'} = {s} \/ {s'} by ENUMSET1:41 .= {s} by A80,A81; then {s} in the_subsets_of_card(2,X) by A80; then consider X' be Subset of X such that A82: X'={s} & Card X' = 2; thus contradiction by A82,CARD_1:50; end; hence x in S \ {s} by A66,A65,CARD_1:78,A80,XBOOLE_0:def 4; end; end; assume A83: x in S \ {s}; then reconsider s'=x as Element of S by XBOOLE_0:def 4; {s,s'} c= S by A68,ZFMISC_1:38; then A84: {s,s'} is Subset of X by XBOOLE_1:1; not s' in {s} by A83,XBOOLE_0:def 4; then s<>s' by TARSKI:def 1; then Card {s,s'} = 2 by CARD_2:76; then A85: {s,s'} in dom F by A84,A67; then A86: F.{s,s'} in rng F by FUNCT_1:12; per cases by A86,A67,FINSEQ_1:4,TARSKI:def 2; suppose F.{s,s'} = 1; then x in A by A85; hence x in A \/ B by XBOOLE_0:def 2; end; suppose F.{s,s'} = 2; then x in B by A85; hence x in A \/ B by XBOOLE_0:def 2; end; end; A87: A \/ B c= S by A75,A69,TARSKI:2; reconsider A as finite Subset of S by A87,XBOOLE_1:11,FINSET_1:13; reconsider B as finite Subset of S by A87,XBOOLE_1:11,FINSET_1:13; A88: card (A \/ B) = card A + card B - card {} by A70,CARD_2:64 .= card A + card B; {s} c= S by A68,ZFMISC_1:37; then card(S \ {s}) = card S - card {s} by CARD_2:63 .= r1 + r2 - 1 by A66,CARD_1:50; then A89: card A + card B = r1 + r2 - 1 by A88,A75,TARSKI:2; A90: card A >= r2 or card B >= r1 proof assume card A < r2; then A91: card A + 1 <= r2 by NAT_1:13; assume card B < r1; then card A + 1 + card B < r2 + r1 by A91,XREAL_1:10; hence contradiction by A89; end; per cases by A90; suppose A92: card A >= r2; set F' = F|the_subsets_of_card(2,A); A c= X by XBOOLE_1:1; then A93: the_subsets_of_card(2,X) /\ the_subsets_of_card(2,A) = the_subsets_of_card(2,A) by XBOOLE_1:28,Lm1; A94: dom(F|the_subsets_of_card(2,A)) = the_subsets_of_card(2,A) by A67,A93,RELAT_1:90; rng(F|the_subsets_of_card(2,A)) c= rng F by RELAT_1:99; then reconsider F' as Function of the_subsets_of_card(2,A), Seg 2 by A94,FUNCT_2:4,A67,XBOOLE_1:1; consider S' be Subset of A such that A95: (card S' >= m & rng(F'|the_subsets_of_card(2,S')) = {1}) or (card S' >= n+1 & rng(F'|the_subsets_of_card(2,S')) = {2}) by A92,A58; A96: F'|the_subsets_of_card(2,S') = F|the_subsets_of_card(2,S') by Lm1,RELAT_1:103; A c= X by XBOOLE_1:1; then reconsider S' as Subset of X by XBOOLE_1:1; per cases by A95; suppose A97: card S' >= n+1 & rng(F'|the_subsets_of_card(2,S')) = {2}; take S'; thus thesis by Lm1,RELAT_1:103,A97; end; suppose A98: card S' >= m & rng(F'|the_subsets_of_card(2,S')) = {1}; set S'' = S' \/ {s}; {s} c= X by A68,ZFMISC_1:37; then reconsider S'' as Subset of X by XBOOLE_1:8; A99: the_subsets_of_card(2,S') c= the_subsets_of_card(2,S'') by Lm1,XBOOLE_1:7; A100: rng(F|the_subsets_of_card(2,S')) = {1} by A98,Lm1,RELAT_1:103; A101: for y being set holds y in rng(F|the_subsets_of_card(2,S'')) iff y = 1 proof let y be set; hereby assume y in rng(F|the_subsets_of_card(2,S'')); then consider x be set such that A102: x in dom(F|the_subsets_of_card(2,S'')) and A103: y = (F|the_subsets_of_card(2,S'')).x by FUNCT_1:def 5; A104: x in the_subsets_of_card(2,S'') & x in dom F by A102,RELAT_1:86; x in {S''' where S''' is Subset of S'': Card S''' = 2} by A102,RELAT_1:86; then consider S''' be Subset of S'' such that A105: x=S''' & Card S''' = 2; consider s1,s2 be set such that A106: s1 <> s2 & S''' = {s1,s2} by A105,CARD_2:79; A107: s1 in S''' & s2 in S''' by A106,TARSKI:def 2; per cases by A107,XBOOLE_0:def 2; suppose A108: s1 in S'; per cases by A107,XBOOLE_0:def 2; suppose s2 in S'; then reconsider x as Subset of S' by A105,A106,A108,ZFMISC_1:38; x in the_subsets_of_card(2,S') by A105; then A109: x in dom(F|the_subsets_of_card(2,S')) by A104,RELAT_1:86; A110: x in dom(F|the_subsets_of_card(2,S'')| the_subsets_of_card(2,S')) by A109,A99,RELAT_1:103; (F|the_subsets_of_card(2,S')).x = (F|the_subsets_of_card(2,S'')|the_subsets_of_card(2,S')).x by A99,RELAT_1:103 .= (F|the_subsets_of_card(2,S'')).x by A110,FUNCT_1:70; then y in rng(F|the_subsets_of_card(2,S')) by A103,A109,FUNCT_1:12; hence y = 1 by TARSKI:def 1,A98,A96; end; suppose s2 in {s}; then A111: s1 <> s & x = {s1,s} by A106,A105,TARSKI:def 1; s1 in A by A108; then consider s'' be Element of S such that A112: s1=s'' & F.{s,s''} = 1 & {s,s''} in dom F; thus y = 1 by A103,A104,A111,A112,FUNCT_1:72; end; end; suppose A113: s1 in {s}; then A114: s <> s2 & x = {s,s2} by A106,A105,TARSKI:def 1; per cases by A107,XBOOLE_0:def 2; suppose s2 in S'; then s2 in A; then consider s'' be Element of S such that A115: s2=s'' & F.{s,s''} = 1 & {s,s''} in dom F; F.x = 1 & x in dom F by A113,A115,A106,A105,TARSKI:def 1; hence y = 1 by A103,A104,FUNCT_1:72; end; suppose s2 in {s}; hence y=1 by A114,TARSKI:def 1; end; end; end; assume y = 1; then A116: y in rng(F|the_subsets_of_card(2,S')) by A100,TARSKI:def 1; F|the_subsets_of_card(2,S') c= F|the_subsets_of_card(2,S'') by A99,RELAT_1:104; then rng(F|the_subsets_of_card(2,S')) c= rng(F|the_subsets_of_card(2,S'')) by RELAT_1:25; hence y in rng(F|the_subsets_of_card(2,S'')) by A116; end; A117: card S' + 1 >= m + 1 by A98,XREAL_1:8; A118: not s in S' proof assume s in S'; then s in A; then consider s' be Element of S such that A119: s=s' & F.{s,s'} = 1 & {s,s'} in dom F; A120: {s,s} = {s} \/ {s} by ENUMSET1:41 .= {s}; {s} in the_subsets_of_card(2,X) by A119,A120; then consider X' be Subset of X such that A121: X'={s} & Card X' = 2; thus contradiction by A121,CARD_1:50; end; take S''; thus thesis by A101,A118,A117,CARD_2:54,TARSKI:def 1; end; end; suppose A122: card B >= r1; set F' = F|the_subsets_of_card(2,B); B c= X by XBOOLE_1:1; then A123: the_subsets_of_card(2,X) /\ the_subsets_of_card(2,B) = the_subsets_of_card(2,B) by XBOOLE_1:28,Lm1; A124: dom(F|the_subsets_of_card(2,B)) = the_subsets_of_card(2,B) by A67,A123,RELAT_1:90; rng(F|the_subsets_of_card(2,B)) c= rng F by RELAT_1:99; then reconsider F' as Function of the_subsets_of_card(2,B), Seg 2 by A124,FUNCT_2:4,A67,XBOOLE_1:1; consider S' be Subset of B such that A125: (card S' >= m+1 & rng(F'|the_subsets_of_card(2,S')) = {1}) or (card S' >= n & rng(F'|the_subsets_of_card(2,S')) = {2}) by A122,A56; A126: F'|the_subsets_of_card(2,S') = F|the_subsets_of_card(2,S') by Lm1,RELAT_1:103; B c= X by XBOOLE_1:1; then reconsider S' as Subset of X by XBOOLE_1:1; per cases by A125; suppose A127: card S' >= m+1 & rng(F'|the_subsets_of_card(2,S')) = {1}; take S'; thus thesis by Lm1,RELAT_1:103,A127; end; suppose A128: card S' >= n & rng(F'|the_subsets_of_card(2,S')) = {2}; set S'' = S' \/ {s}; {s} c= X by A68,ZFMISC_1:37; then reconsider S'' as Subset of X by XBOOLE_1:8; A129: the_subsets_of_card(2,S') c= the_subsets_of_card(2,S'') by Lm1,XBOOLE_1:7; A130: rng(F|the_subsets_of_card(2,S')) = {2} by A128,Lm1,RELAT_1:103; A131: for y being set holds y in rng(F|the_subsets_of_card(2,S'')) iff y = 2 proof let y be set; hereby assume y in rng(F|the_subsets_of_card(2,S'')); then consider x be set such that A132: x in dom(F|the_subsets_of_card(2,S'')) and A133: y = (F|the_subsets_of_card(2,S'')).x by FUNCT_1:def 5; A134: x in the_subsets_of_card(2,S'') & x in dom F by A132,RELAT_1:86; x in {S''' where S''' is Subset of S'': Card S''' = 2} by A132,RELAT_1:86; then consider S''' be Subset of S'' such that A135: x=S''' & Card S''' = 2; consider s1,s2 be set such that A136: s1 <> s2 & S''' = {s1,s2} by A135,CARD_2:79; A137: s1 in S''' & s2 in S''' by A136,TARSKI:def 2; per cases by A137,XBOOLE_0:def 2; suppose A138: s1 in S'; per cases by A137,XBOOLE_0:def 2; suppose s2 in S'; then reconsider x as Subset of S' by A135,A136,A138,ZFMISC_1:38; x in the_subsets_of_card(2,S') by A135; then A139: x in dom(F|the_subsets_of_card(2,S')) by A134,RELAT_1:86; A140: x in dom(F|the_subsets_of_card(2,S'')| the_subsets_of_card(2,S')) by A139,A129,RELAT_1:103; (F|the_subsets_of_card(2,S')).x = (F|the_subsets_of_card(2,S'')|the_subsets_of_card(2,S')).x by A129,RELAT_1:103 .= (F|the_subsets_of_card(2,S'')).x by A140,FUNCT_1:70; then y in rng(F|the_subsets_of_card(2,S')) by A133,A139,FUNCT_1:12; hence y = 2 by TARSKI:def 1,A128,A126; end; suppose s2 in {s}; then A141: s1 <> s & x = {s1,s} by A136,A135,TARSKI:def 1; s1 in B by A138; then consider s'' be Element of S such that A142: s1=s'' & F.{s,s''} = 2 & {s,s''} in dom F; thus y = 2 by A133,A134,A141,A142,FUNCT_1:72; end; end; suppose A143: s1 in {s}; then A144: s <> s2 & x = {s,s2} by A136,A135,TARSKI:def 1; per cases by A137,XBOOLE_0:def 2; suppose s2 in S'; then s2 in B; then consider s'' be Element of S such that A145: s2=s'' & F.{s,s''} = 2 & {s,s''} in dom F; F.x = 2 & x in dom F by A143,A145,A136,A135,TARSKI:def 1; hence y = 2 by A133,A134,FUNCT_1:72; end; suppose s2 in {s}; hence y = 2 by A144,TARSKI:def 1; end; end; end; assume y = 2; then A146: y in rng(F|the_subsets_of_card(2,S')) by A130,TARSKI:def 1; F|the_subsets_of_card(2,S') c= F|the_subsets_of_card(2,S'') by A129,RELAT_1:104; then rng(F|the_subsets_of_card(2,S')) c= rng(F|the_subsets_of_card(2,S'')) by RELAT_1:25; hence y in rng(F|the_subsets_of_card(2,S'')) by A146; end; A147: card S' + 1 >= n + 1 by A128,XREAL_1:8; A148: not s in S' proof assume s in S'; then s in B; then consider s' be Element of S such that A149: s=s' & F.{s,s'} = 2 & {s,s'} in dom F; A150: {s,s} = {s} \/ {s} by ENUMSET1:41 .= {s}; {s} in the_subsets_of_card(2,X) by A149,A150; then consider X' be Subset of X such that A151: X'={s} & Card X' = 2; thus contradiction by A151,CARD_1:50; end; take S''; thus thesis by A131,A148,A147,CARD_2:54,TARSKI:def 1; end; end; end; end; for m,n being natural number holds P[m,n] from BinInd2(A1,A2); hence thesis; end; theorem for m being natural number holds ex r being natural number st for X being finite set, P being a_partition of the_subsets_of_card(2,X) st card X >= r & Card P = 2 holds ex S being Subset of X st card S >= m & S is_homogeneous_for P proof let m be natural number; per cases; suppose m<2; then m<1+1; then A1: m<=1 by NAT_1:13; set r=1; take r; let X be finite set; let P be a_partition of the_subsets_of_card(2,X); assume A2: card X >= r; assume Card P = 2; consider x be set such that A3: x in X by A2,CARD_1:78,XBOOLE_0:def 1; reconsider S = {x} as Subset of X by A3,ZFMISC_1:37; take S; A4: card S = 1 by CARD_1:79; thus card S >= m by A1,CARD_1:79; ex p being Element of P st the_subsets_of_card(2,S) c= p proof consider p be Element of P; take p; the_subsets_of_card(2,S) = {} by A4,Th6; hence the_subsets_of_card(2,S) c= p by XBOOLE_1:2; end; hence S is_homogeneous_for P by Def1; end; suppose A5: m>=2; then consider r be natural number such that A6: r <= (m + m -' 2) choose (m -' 1) & r >= 2 and A7: for X being finite set, F being Function of the_subsets_of_card(2,X), Seg 2 st card X >= r holds ex S being Subset of X st (card S >= m & rng(F|the_subsets_of_card(2,S)) = {1}) or (card S >= m & rng(F|the_subsets_of_card(2,S)) = {2}) by Th16; take r; let X be finite set; let P be a_partition of the_subsets_of_card(2,X); assume A8: card X >= r & Card P = 2; then 2 <= card X by A6,XXREAL_0:2; then card Seg 2 <= card X by FINSEQ_1:78; then Card Seg 2 c= Card X by CARD_2:57; then A9: Card 2 c= Card X by FINSEQ_1:76; reconsider X' = the_subsets_of_card(2,X) as non empty set by A8,A6,CARD_1:78,A9,GROUP_10:2; reconsider P'=P as a_partition of X'; Card P' = Card Seg 2 by A8,FINSEQ_1:78; then A10: P', Seg 2 are_equipotent by CARD_1:21; then consider F1 be Function such that A11: F1 is one-to-one & dom F1 = P' & rng F1 = Seg 2 by WELLORD2:def 4; reconsider F1 as Function of P',Seg 2 by A11,FUNCT_2:3; set F=F1*(proj P'); reconsider F as Function of the_subsets_of_card(2,X),Seg 2; consider S be Subset of X such that A12: (card S >= m & rng(F|the_subsets_of_card(2,S)) = {1}) or (card S >= m & rng(F|the_subsets_of_card(2,S)) = {2}) by A7,A8; take S; thus card S >= m by A12; consider h be Element of the_subsets_of_card(2,S); A13: the_subsets_of_card(2,S) c= the_subsets_of_card(2,X) by Lm1; 2 <= card S by A5,A12,XXREAL_0:2; then card Seg 2 <= card S by FINSEQ_1:78; then Card Seg 2 c= Card S by CARD_2:57; then Card 2 c= Card S by FINSEQ_1:76; then A14: the_subsets_of_card(2,S) is non empty by A5,A12,CARD_1:78,GROUP_10:2; then h in the_subsets_of_card(2,S); then reconsider h as Element of X' by A13; A15: F|the_subsets_of_card(2,S) is constant proof A16: 1 is Element of Seg 2 & 2 is Element of Seg 2 by TARSKI:def 2,FINSEQ_1:4; F|the_subsets_of_card(2,S) is Function of the_subsets_of_card(2,S),Seg 2 by A13,FUNCT_2:38,FINSEQ_1:4; hence thesis by A16,FINSEQ_1:4,A14,A12,Lm4; end; set E = EqClass(h,P'); reconsider E as Element of P by EQREL_1:def 8; for x being set holds x in the_subsets_of_card(2,S) implies x in E proof let x be set; assume A17: x in the_subsets_of_card(2,S); then reconsider x'=x as Element of the_subsets_of_card(2,X) by A13; reconsider x''=x as Element of X' by A17,A13; A18: h in E by EQREL_1:def 8; Seg 2 <> {} by A10,CARD_1:46; then A19: dom F = the_subsets_of_card(2,X) by FUNCT_2:def 1; x' in dom F /\ the_subsets_of_card(2,S) by A19,A17,XBOOLE_0:def 3; then A20: x' in dom(F|the_subsets_of_card(2,S)) by RELAT_1:90; h in dom F /\ the_subsets_of_card(2,S) by A19,A14,XBOOLE_0:def 3; then A21: h in dom(F|the_subsets_of_card(2,S)) by RELAT_1:90; A22: F.x' = F|the_subsets_of_card(2,S).x' by A17,FUNCT_1:72 .= F|the_subsets_of_card(2,S).h by A15,A20,A21,FUNCT_1:def 16 .= F.h by A14,FUNCT_1:72; A23: F1.((proj P').x') = (F1*proj P').h by A22,A19,FUNCT_1:22 .= F1.((proj P').h) by A19,FUNCT_1:22; A24: (proj P').x'' in P'; (proj P').h = (proj P').x' by A24,A23,A11,FUNCT_1:def 8; hence x in E by A18,Th13; end; then the_subsets_of_card(2,S) c= E by TARSKI:def 3; hence S is_homogeneous_for P by Def1; end; end;