:: RAMSEY_1 semantic presentation begin definition let X, Y be set ; let H be Subset of X; let P be a_partition of the_subsets_of_card (Y,X); predH is_homogeneous_for P means :Def1: :: RAMSEY_1:def 1 ex p being Element of P st the_subsets_of_card (Y,H) c= p; end; :: deftheorem Def1 defines is_homogeneous_for RAMSEY_1:def_1_:_ for X, Y being set for H being Subset of X for P being a_partition of the_subsets_of_card (Y,X) holds ( H is_homogeneous_for P iff ex p being Element of P st the_subsets_of_card (Y,H) c= p ); registration let n be Nat; let X be infinite set ; cluster the_subsets_of_card (n,X) -> non empty ; correctness coherence not the_subsets_of_card (n,X) is empty ; proof not card X c= card n ; hence not the_subsets_of_card (n,X) is empty by GROUP_10:1; ::_thesis: verum end; end; definition let n be Nat; let X, Y be set ; let f be Function of X,Y; assume that A1: f is one-to-one and A2: ( card n c= card X & not X is empty ) and A3: not Y is empty ; funcf ||^ n -> Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) means :Def2: :: RAMSEY_1:def 2 for x being Element of the_subsets_of_card (n,X) holds it . x = f .: x; existence ex b1 being Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) st for x being Element of the_subsets_of_card (n,X) holds b1 . x = f .: x proof set D = the_subsets_of_card (n,X); reconsider D = the_subsets_of_card (n,X) as non empty set by A2, GROUP_10:1; deffunc H1( set ) -> set = f .: $1; consider IT being Function such that A4: ( dom IT = D & ( for x being Element of D holds IT . x = H1(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 ; ::_thesis: ( y in rng IT implies y in the_subsets_of_card (n,Y) ) assume y in rng IT ; ::_thesis: y in the_subsets_of_card (n,Y) then consider x being set such that A5: x in dom IT and A6: y = IT . x by FUNCT_1:def_3; A7: ex x9 being Subset of X st ( x = x9 & card x9 = n ) by A4, A5; reconsider x = x as Element of D by A4, A5; A8: y = f .: x by A4, A6; f in Funcs (X,Y) by A3, FUNCT_2:8; then A9: ex f9 being Function st ( f = f9 & dom f9 = X & rng f9 c= Y ) by FUNCT_2:def_2; f .: x c= rng f by RELAT_1:111; then reconsider y9 = y as Subset of Y by A8, A9, XBOOLE_1:1; x,f .: x are_equipotent by A1, A4, A5, A9, CARD_1:33; then card y9 = n by A7, A8, CARD_1:5; hence y in the_subsets_of_card (n,Y) ; ::_thesis: verum end; then rng IT c= the_subsets_of_card (n,Y) by TARSKI:def_3; then reconsider IT = IT as Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) by A4, FUNCT_2:2; take IT ; ::_thesis: for x being Element of the_subsets_of_card (n,X) holds IT . x = f .: x thus for x being Element of the_subsets_of_card (n,X) holds IT . x = f .: x by A4; ::_thesis: verum end; uniqueness for b1, b2 being Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) st ( for x being Element of the_subsets_of_card (n,X) holds b1 . x = f .: x ) & ( for x being Element of the_subsets_of_card (n,X) holds b2 . x = f .: x ) holds b1 = b2 proof let F1, F2 be Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)); ::_thesis: ( ( for x being Element of the_subsets_of_card (n,X) holds F1 . x = f .: x ) & ( for x being Element of the_subsets_of_card (n,X) holds F2 . x = f .: x ) implies F1 = F2 ) assume that A10: for x being Element of the_subsets_of_card (n,X) holds F1 . x = f .: x and A11: for x being Element of the_subsets_of_card (n,X) holds F2 . x = f .: x ; ::_thesis: F1 = F2 now__::_thesis:_for_x_being_set_st_x_in_the_subsets_of_card_(n,X)_holds_ F1_._x_=_F2_._x let x be set ; ::_thesis: ( x in the_subsets_of_card (n,X) implies F1 . x = F2 . x ) assume x in the_subsets_of_card (n,X) ; ::_thesis: F1 . x = F2 . x then reconsider x9 = x as Element of the_subsets_of_card (n,X) ; thus F1 . x = f .: x9 by A10 .= F2 . x by A11 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def2 defines ||^ RAMSEY_1:def_2_:_ for n being Nat for X, Y being set for f being Function of X,Y st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds for b5 being Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) holds ( b5 = f ||^ n iff for x being Element of the_subsets_of_card (n,X) holds b5 . x = f .: x ); Lm1: for X, Y, Z being set st X c= Y holds the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) proof let X, Y, Z be set ; ::_thesis: ( X c= Y implies the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) ) assume A1: X c= Y ; ::_thesis: the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) for x being set st x in the_subsets_of_card (Z,X) holds x in the_subsets_of_card (Z,Y) proof let x be set ; ::_thesis: ( x in the_subsets_of_card (Z,X) implies x in the_subsets_of_card (Z,Y) ) assume x in the_subsets_of_card (Z,X) ; ::_thesis: x in the_subsets_of_card (Z,Y) then consider x9 being Subset of X such that A2: x9 = x and A3: card x9 = Z ; reconsider x99 = x9 as Subset of Y by A1, XBOOLE_1:1; x99 = x by A2; hence x in the_subsets_of_card (Z,Y) by A3; ::_thesis: verum end; hence the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) by TARSKI:def_3; ::_thesis: verum end; theorem Th1: :: RAMSEY_1:1 for n being Nat for X, Y being set for f being Function of X,Y for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) proof let n be Nat; ::_thesis: for X, Y being set for f being Function of X,Y for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) let X, Y be set ; ::_thesis: for f being Function of X,Y for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) let f be Function of X,Y; ::_thesis: for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) let H be Subset of X; ::_thesis: ( f is one-to-one & card n c= card X & not X is empty & not Y is empty implies the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) ) assume that A1: f is one-to-one and A2: card n c= card X and A3: not X is empty and A4: not Y is empty ; ::_thesis: the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) consider f1 being Function such that A5: n c= f1 .: X by A2, CARD_1:66; f in Funcs (X,Y) by A4, FUNCT_2:8; then A6: ex f9 being Function st ( f = f9 & dom f9 = X & rng f9 c= Y ) by FUNCT_2:def_2; then card X c= card Y by A1, CARD_1:10; then consider f2 being Function such that A7: X c= f2 .: Y by CARD_1:66; f1 .: X c= f1 .: (f2 .: Y) by A7, RELAT_1:123; then n c= f1 .: (f2 .: Y) by A5, XBOOLE_1:1; then n c= (f1 * f2) .: Y by RELAT_1:126; then card n c= card Y by CARD_1:66; then not the_subsets_of_card (n,Y) is empty by A4, GROUP_10:1; then f ||^ n in Funcs ((the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y))) by FUNCT_2:8; then A8: ex fn being Function st ( 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 ; ::_thesis: ( y in the_subsets_of_card (n,(f .: H)) iff y in (f ||^ n) .: (the_subsets_of_card (n,H)) ) hereby ::_thesis: ( y in (f ||^ n) .: (the_subsets_of_card (n,H)) implies y in the_subsets_of_card (n,(f .: H)) ) A9: f .: H c= rng f by RELAT_1:111; assume A10: y in the_subsets_of_card (n,(f .: H)) ; ::_thesis: y in (f ||^ n) .: (the_subsets_of_card (n,H)) then A11: ex X9 being Subset of (f .: H) st ( y = X9 & card X9 = n ) ; 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; take f " y ; ::_thesis: ( f " y in dom (f ||^ n) & f " y in the_subsets_of_card (n,H) & y = (f ||^ n) . (f " y) ) A12: f " y c= dom f by RELAT_1:132; A13: f .: (f " y) = y by A10, A9, FUNCT_1:77, XBOOLE_1:1; then reconsider x9 = f " y as Subset of H by A1, A10, A12, FUNCT_1:87; f " y,f .: (f " y) are_equipotent by A1, A12, CARD_1:33; then A14: card x9 = n by A11, A13, CARD_1:5; then A15: f " y in the_subsets_of_card (n,H) ; A16: the_subsets_of_card (n,H) c= the_subsets_of_card (n,X) by Lm1; hence f " y in dom (f ||^ n) by A8, A15; ::_thesis: ( f " y in the_subsets_of_card (n,H) & y = (f ||^ n) . (f " y) ) thus f " y in the_subsets_of_card (n,H) by A14; ::_thesis: y = (f ||^ n) . (f " y) thus y = f .: (f " y) by A10, A9, FUNCT_1:77, XBOOLE_1:1 .= (f ||^ n) . (f " y) by A1, A2, A3, A4, A15, A16, Def2 ; ::_thesis: verum end; hence y in (f ||^ n) .: (the_subsets_of_card (n,H)) by FUNCT_1:def_6; ::_thesis: verum end; assume y in (f ||^ n) .: (the_subsets_of_card (n,H)) ; ::_thesis: y in the_subsets_of_card (n,(f .: H)) then consider x being set such that A17: x in dom (f ||^ n) and A18: x in the_subsets_of_card (n,H) and A19: y = (f ||^ n) . x by FUNCT_1:def_6; reconsider x = x as Element of the_subsets_of_card (n,X) by A17; A20: y = f .: x by A1, A2, A3, A4, A19, Def2; then reconsider X9 = y as Subset of (f .: H) by A18, RELAT_1:123; ( ex x9 being Subset of H st ( x9 = x & card x9 = n ) & x,f .: x are_equipotent ) by A1, A6, A18, CARD_1:33, XBOOLE_1:1; then card X9 = n by A20, CARD_1:5; hence y in the_subsets_of_card (n,(f .: H)) ; ::_thesis: verum end; hence the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) by TARSKI:1; ::_thesis: verum end; Lm2: for X being set holds the_subsets_of_card (0,X) = {0} proof let X be set ; ::_thesis: the_subsets_of_card (0,X) = {0} for x being set holds ( x in the_subsets_of_card (0,X) iff x = 0 ) proof let x be set ; ::_thesis: ( x in the_subsets_of_card (0,X) iff x = 0 ) hereby ::_thesis: ( x = 0 implies x in the_subsets_of_card (0,X) ) assume x in the_subsets_of_card (0,X) ; ::_thesis: x = 0 then ex x9 being Subset of X st ( x9 = x & card x9 = 0 ) ; hence x = 0 ; ::_thesis: verum end; assume A1: x = 0 ; ::_thesis: x in the_subsets_of_card (0,X) then reconsider x9 = x as Subset of X by XBOOLE_1:2; card x9 = 0 by A1; hence x in the_subsets_of_card (0,X) ; ::_thesis: verum end; hence the_subsets_of_card (0,X) = {0} by TARSKI:def_1; ::_thesis: verum 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 ; ::_thesis: ( card Y = X implies the_subsets_of_card (X,Y) = {Y} ) assume A1: card Y = X ; ::_thesis: the_subsets_of_card (X,Y) = {Y} for x being set holds ( x in the_subsets_of_card (X,Y) iff x = Y ) proof let x be set ; ::_thesis: ( x in the_subsets_of_card (X,Y) iff x = Y ) hereby ::_thesis: ( x = Y implies x in the_subsets_of_card (X,Y) ) assume x in the_subsets_of_card (X,Y) ; ::_thesis: x = Y then consider X9 being Subset of Y such that A2: X9 = x and A3: card X9 = X ; reconsider X9 = X9 as finite Subset of Y ; card (Y \ X9) = (card Y) - (card X9) by CARD_2:44 .= 0 by A1, A3 ; then Y \ X9 = {} ; then Y c= X9 by XBOOLE_1:37; hence x = Y by A2, XBOOLE_0:def_10; ::_thesis: verum end; assume A4: x = Y ; ::_thesis: x in the_subsets_of_card (X,Y) then x c= Y ; then reconsider x9 = x as Subset of Y ; x9 in the_subsets_of_card (X,Y) by A1, A4; hence x in the_subsets_of_card (X,Y) ; ::_thesis: verum end; hence the_subsets_of_card (X,Y) = {Y} by TARSKI:def_1; ::_thesis: verum end; theorem Th2: :: RAMSEY_1:2 for X being set st X is infinite & X c= omega holds card X = omega proof let X be set ; ::_thesis: ( X is infinite & X c= omega implies card X = omega ) assume ( X is infinite & X c= omega ) ; ::_thesis: card X = omega then NAT ,X are_equipotent by WAYBEL12:2; hence card X = omega by CARD_1:5, CARD_1:47; ::_thesis: verum end; theorem Th3: :: RAMSEY_1:3 for X, Y being set st X is infinite holds X \/ Y is infinite proof let X, Y be set ; ::_thesis: ( X is infinite implies X \/ Y is infinite ) assume A1: X is infinite ; ::_thesis: X \/ Y is infinite A2: card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7; assume X \/ Y is finite ; ::_thesis: contradiction hence contradiction by A1, A2; ::_thesis: verum end; theorem Th4: :: RAMSEY_1:4 for X, Y being set st X is infinite & Y is finite holds X \ Y is infinite proof let X, Y be set ; ::_thesis: ( X is infinite & Y is finite implies X \ Y is infinite ) assume A1: ( X is infinite & Y is finite ) ; ::_thesis: X \ Y is infinite A2: X \/ Y = (X \ Y) \/ Y by XBOOLE_1:39; assume X \ Y is finite ; ::_thesis: contradiction hence contradiction by A1, A2, Th3; ::_thesis: verum end; registration let X be infinite set ; let Y be set ; clusterX \/ Y -> infinite ; correctness coherence not X \/ Y is finite ; by Th3; end; registration let X be infinite set ; let Y be finite set ; clusterX \ Y -> infinite ; correctness coherence not X \ Y is finite ; by Th4; end; Lm4: for n, k being Nat for X being set for F being Function of (the_subsets_of_card (n,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 (n,H)) is constant ) proof let n, k be Nat; ::_thesis: for X being set for F being Function of (the_subsets_of_card (n,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 (n,H)) is constant ) let X be set ; ::_thesis: for F being Function of (the_subsets_of_card (n,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 (n,H)) is constant ) defpred S1[ Nat] means for k being Nat for X being set for 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: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_k_being_Nat for_X_being_set_ for_F_being_Function_of_(the_subsets_of_card_((n_+_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_((n_+_1),H))_is_constant_) let k be Nat; ::_thesis: for X being set for F being Function of (the_subsets_of_card ((n + 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 ((n + 1),H)) is constant ) let X be set ; ::_thesis: for F being Function of (the_subsets_of_card ((n + 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 ((n + 1),H)) is constant ) let F be Function of (the_subsets_of_card ((n + 1),X)),k; ::_thesis: ( card X = omega & X c= omega & k <> 0 implies ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) ) assume A3: card X = omega ; ::_thesis: ( X c= omega & k <> 0 implies ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) ) X c= X ; then A4: X in the_subsets_of_card (omega,X) by A3; then reconsider A = the_subsets_of_card (omega,X) as non empty set ; reconsider X0 = X as Element of A by A4; defpred S2[ set , set , set , set , set ] means for x1, x2 being Element of A for 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 ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) ); set Y0 = min* X; assume A5: X c= omega ; ::_thesis: ( k <> 0 implies ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) ) assume A6: k <> 0 ; ::_thesis: ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) A7: for Y being set for a being Element of Y st card Y = omega & Y c= X holds ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) proof let Y be set ; ::_thesis: for a being Element of Y st card Y = omega & Y c= X holds ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) let a be Element of Y; ::_thesis: ( card Y = omega & Y c= X implies ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) ) set Y1 = the_subsets_of_card (n,(Y \ {a})); assume A8: card Y = omega ; ::_thesis: ( not Y c= X or ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) ) then A9: Y is infinite ; then reconsider Y1 = the_subsets_of_card (n,(Y \ {a})) as non empty set ; deffunc H1( Element of Y1) -> set = F . ($1 \/ {a}); assume A10: Y c= X ; ::_thesis: ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) not Y is empty by A8; then A11: {a} c= Y by ZFMISC_1:31; A12: for x being Element of Y1 holds H1(x) in k proof let x be Element of Y1; ::_thesis: H1(x) in k x in Y1 ; then consider x9 being Subset of (Y \ {a}) such that A13: x = x9 and A14: card x9 = n ; x \/ {a} c= (Y \ {a}) \/ {a} by A13, XBOOLE_1:9; then x \/ {a} c= Y \/ {a} by XBOOLE_1:39; then reconsider y = x \/ {a} as Subset of Y by A11, XBOOLE_1:12; reconsider x99 = x9 as finite set by A14; not a in x99 proof assume a in x99 ; ::_thesis: contradiction then not a in {a} by XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then card y = n + 1 by A13, A14, CARD_2:41; then A15: x \/ {a} in the_subsets_of_card ((n + 1),Y) ; the_subsets_of_card ((n + 1),Y) c= the_subsets_of_card ((n + 1),X) by A10, Lm1; hence H1(x) in k by A6, A15, FUNCT_2:5; ::_thesis: verum end; consider Fa being Function of Y1,k such that A16: for x being Element of Y1 holds Fa . x = H1(x) from FUNCT_2:sch_8(A12); reconsider Fa = Fa as Function of (the_subsets_of_card (n,(Y \ {a}))),k ; A17: Y c= omega by A5, A10, XBOOLE_1:1; then card (Y \ {a}) = omega by A9, Th2, XBOOLE_1:1; then consider Ha being Subset of (Y \ {a}) such that A18: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A2, A6, A17, XBOOLE_1:1; take Fa ; ::_thesis: ex Ha being Subset of (Y \ {a}) st ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) take Ha ; ::_thesis: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) thus ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A18; ::_thesis: for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) let Y9 be Element of the_subsets_of_card (n,(Y \ {a})); ::_thesis: Fa . Y9 = F . (Y9 \/ {a}) thus Fa . Y9 = F . (Y9 \/ {a}) by A16; ::_thesis: verum end; A19: for a being Element of NAT for x99 being Element of A for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199] proof let a be Element of NAT ; ::_thesis: for x99 being Element of A for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199] let x99 be Element of A; ::_thesis: for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199] let y99 be Element of omega ; ::_thesis: ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199] percases ( y99 in x99 or not y99 in x99 ) ; supposeA20: y99 in x99 ; ::_thesis: ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199] then reconsider a9 = y99 as Element of x99 ; A21: x99 in A ; then ex x999 being Subset of X st ( x999 = x99 & card x999 = omega ) ; then consider Fa being Function of (the_subsets_of_card (n,(x99 \ {a9}))),k, Ha being Subset of (x99 \ {a9}) such that A22: Ha is infinite and A23: Fa | (the_subsets_of_card (n,Ha)) is constant and A24: for Y9 being Element of the_subsets_of_card (n,(x99 \ {a9})) holds Fa . Y9 = F . (Y9 \/ {a9}) by A7; Ha c= x99 by XBOOLE_1:1; then A25: Ha c= X by A21, XBOOLE_1:1; then card Ha = omega by A5, A22, Th2, XBOOLE_1:1; then Ha in A by A25; then reconsider x199 = Ha as Element of A ; set y199 = min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; take x199 ; ::_thesis: ex y199 being Element of omega st S2[a,x99,y99,x199,y199] take min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; ::_thesis: S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] A26: Ha c= omega by A5, A25, XBOOLE_1:1; now__::_thesis:_for_x1,_x2_being_Element_of_A for_y1,_y2_being_Element_of_omega_st_x99_=_x1_&_y99_=_y1_&_x199_=_x2_&_min*__{__y29_where_y29_is_Element_of_omega_:_(_y29_>_y99_&_y29_in_Ha_)__}__=_y2_holds_ (_(_y1_in_x1_implies_ex_F1_being_Function_of_(the_subsets_of_card_(n,(x1_\_{y1}))),k_ex_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_x19_being_Element_of_the_subsets_of_card_(n,(x1_\_{y1}))_holds_F1_._x19_=_F_._(x19_\/_{y1})_)_&_(_for_y29_being_Element_of_omega_st_y29_>_y1_&_y29_in_H1_holds_ y2_<=_y29_)_)_)_&_(_not_y1_in_x1_implies_S2[a,x99,y99,x199,_min*__{__y29_where_y29_is_Element_of_omega_:_(_y29_>_y99_&_y29_in_Ha_)__}__]_)_) let x1, x2 be Element of A; ::_thesis: for y1, y2 being Element of omega st x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 holds ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) let y1, y2 be Element of omega ; ::_thesis: ( x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) ) assume that A27: x99 = x1 and A28: y99 = y1 ; ::_thesis: ( x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) ) assume that A29: x199 = x2 and A30: min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 ; ::_thesis: ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) thus ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) ) ::_thesis: ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) proof reconsider H1 = Ha as Subset of (x1 \ {y1}) by A27, A28; set A9 = { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; reconsider F1 = Fa as Function of (the_subsets_of_card (n,(x1 \ {y1}))),k by A27, A28; assume y1 in x1 ; ::_thesis: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) take F1 ; ::_thesis: ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) take H1 ; ::_thesis: ( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) for x being set st x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } holds x in NAT proof let x be set ; ::_thesis: ( x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } implies x in NAT ) assume x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; ::_thesis: x in NAT then ex x9 being Element of omega st ( x9 = x & x9 > y99 & x9 in Ha ) ; hence x in NAT ; ::_thesis: verum end; then reconsider A9 = { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } as Subset of NAT by TARSKI:def_3; thus H1 is infinite by A22; ::_thesis: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) thus F1 | (the_subsets_of_card (n,H1)) is constant by A23; ::_thesis: ( x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) thus x2 = H1 by A29; ::_thesis: ( y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) A9 <> {} proof set A99 = { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; A31: now__::_thesis:_for_x_being_set_st_x_in_A9_\/__{__y2999_where_y2999_is_Element_of_omega_:_(_y2999_<=_y99_&_y2999_in_Ha_)__}__holds_ x_in_Ha let x be set ; ::_thesis: ( x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } implies b1 in Ha ) assume A32: x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; ::_thesis: b1 in Ha percases ( x in A9 or x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ) by A32, XBOOLE_0:def_3; suppose x in A9 ; ::_thesis: b1 in Ha then ex x9 being Element of omega st ( x = x9 & x9 > y99 & x9 in Ha ) ; hence x in Ha ; ::_thesis: verum end; suppose x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; ::_thesis: b1 in Ha then ex x9 being Element of omega st ( x = x9 & x9 <= y99 & x9 in Ha ) ; hence x in Ha ; ::_thesis: verum end; end; end; now__::_thesis:_for_x_being_set_st_x_in__{__y2999_where_y2999_is_Element_of_omega_:_(_y2999_<=_y99_&_y2999_in_Ha_)__}__holds_ x_in_Segm_(y99_+_1) let x be set ; ::_thesis: ( x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } implies x in Segm (y99 + 1) ) assume x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; ::_thesis: x in Segm (y99 + 1) then consider x9 being Element of omega such that A33: x = x9 and A34: x9 <= y99 and x9 in Ha ; x9 < y99 + 1 by A34, NAT_1:13; hence x in Segm (y99 + 1) by A33, NAT_1:44; ::_thesis: verum end; then A35: { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } c= Segm (y99 + 1) by TARSKI:def_3; A36: now__::_thesis:_for_x_being_set_st_x_in_Ha_holds_ x_in_A9_\/__{__y2999_where_y2999_is_Element_of_omega_:_(_y2999_<=_y99_&_y2999_in_Ha_)__}_ let x be set ; ::_thesis: ( x in Ha implies b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) } ) assume A37: x in Ha ; ::_thesis: b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) } then reconsider x9 = x as Element of omega by A26; percases ( x9 <= y99 or x9 > y99 ) ; suppose x9 <= y99 ; ::_thesis: b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) } then x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } by A37; hence x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } by XBOOLE_0:def_3; ::_thesis: verum end; suppose x9 > y99 ; ::_thesis: b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) } then x in A9 by A37; hence x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } by XBOOLE_0:def_3; ::_thesis: verum end; end; end; assume A9 = {} ; ::_thesis: contradiction hence contradiction by A22, A35, A31, A36, TARSKI:1; ::_thesis: verum end; then min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } in A9 by NAT_1:def_1; then A38: ex y299 being Element of omega st ( min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y299 & y299 > y99 & y299 in Ha ) ; hence y2 in H1 by A30; ::_thesis: ( y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) thus y1 < y2 by A28, A30, A38; ::_thesis: ( ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) thus for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) by A24, A27, A28; ::_thesis: for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 let y29 be Element of omega ; ::_thesis: ( y29 > y1 & y29 in H1 implies y2 <= y29 ) assume A39: y29 > y1 ; ::_thesis: ( not y29 in H1 or y2 <= y29 ) assume y29 in H1 ; ::_thesis: y2 <= y29 then y29 in A9 by A28, A39; hence y2 <= y29 by A30, NAT_1:def_1; ::_thesis: verum end; assume not y1 in x1 ; ::_thesis: S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] hence S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] by A20, A27, A28; ::_thesis: verum end; hence S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ; ::_thesis: verum end; supposeA40: not y99 in x99 ; ::_thesis: ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199] reconsider y199 = 0 as Element of omega ; reconsider x199 = X as Element of A by A4; take x199 ; ::_thesis: ex y199 being Element of omega st S2[a,x99,y99,x199,y199] take y199 ; ::_thesis: S2[a,x99,y99,x199,y199] thus S2[a,x99,y99,x199,y199] by A40; ::_thesis: verum end; end; end; consider S being Function of NAT,A, a being Function of NAT,omega such that A41: ( S . 0 = X0 & a . 0 = min* X & ( for i being Element of NAT holds S2[i,S . i,a . i,S . (i + 1),a . (i + 1)] ) ) from RECDEF_2:sch_3(A19); defpred S3[ Nat] 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) ); A42: S3[ 0 ] proof set i = 0 ; reconsider i = 0 as Element of NAT ; 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 ; A43: ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) ) by A41; hence a . 0 in a . (0 + 1) by A3, A5, A41, CARD_1:27, NAT_1:44, NAT_1:def_1; ::_thesis: ( S . (0 + 1) c= S . 0 & a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) ) thus S . (0 + 1) c= S . 0 by A3, A5, A41, A43, CARD_1:27, NAT_1:def_1, XBOOLE_1:1; ::_thesis: ( a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) ) thus a . 0 in S . 0 by A3, A5, A41, CARD_1:27, NAT_1:def_1; ::_thesis: ( a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) ) thus a . (0 + 1) in S . (0 + 1) by A3, A5, A41, A43, CARD_1:27, NAT_1:def_1; ::_thesis: not a . 0 in S . (0 + 1) not y1 in x2 proof assume y1 in x2 ; ::_thesis: contradiction then not y1 in {y1} by A3, A5, A41, A43, CARD_1:27, NAT_1:def_1, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; hence not a . 0 in S . (0 + 1) ; ::_thesis: verum end; defpred S4[ set , set ] means for Y being set for i being Element of NAT for 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 Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds ex l being Nat st ( l = $2 & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ); defpred S5[ Nat] means for i, j being Nat st i >= j & i = $1 + j holds ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ) ); A44: for i being Nat st S3[i] holds S3[i + 1] proof let i be Nat; ::_thesis: ( S3[i] implies S3[i + 1] ) reconsider i9 = i + 1 as Element of NAT ; reconsider x1 = S . i9 as Element of A ; reconsider x2 = S . (i9 + 1) as Element of A ; reconsider y1 = a . i9 as Element of omega ; reconsider y2 = a . (i9 + 1) as Element of omega ; assume A45: S3[i] ; ::_thesis: S3[i + 1] then A46: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) by A41; not y1 in x2 proof assume y1 in x2 ; ::_thesis: contradiction then not y1 in {y1} by A46, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; hence S3[i + 1] by A45, A46, NAT_1:44, XBOOLE_1:1; ::_thesis: verum end; A47: for i being Nat holds S3[i] from NAT_1:sch_2(A42, A44); A48: for l being Nat st S5[l] holds S5[l + 1] proof let l be Nat; ::_thesis: ( S5[l] implies S5[l + 1] ) assume A49: S5[l] ; ::_thesis: S5[l + 1] thus S5[l + 1] ::_thesis: verum proof let i, j be Nat; ::_thesis: ( i >= j & i = (l + 1) + j implies ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ) ) ) assume A50: i >= j ; ::_thesis: ( not i = (l + 1) + j or ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ) ) ) set j9 = j + 1; assume A51: i = (l + 1) + j ; ::_thesis: ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ) ) then A52: i = l + (j + 1) ; A53: S . (j + 1) c= S . j by A47; i <> j proof assume i = j ; ::_thesis: contradiction then 0 = l + 1 by A51; hence contradiction ; ::_thesis: verum end; then i > j by A50, XXREAL_0:1; then A54: i >= j + 1 by NAT_1:13; then S . i c= S . (j + 1) by A49, A52; hence S . i c= S . j by A53, XBOOLE_1:1; ::_thesis: for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj A55: for ai, aj9 being Nat st i <> j + 1 & ai = a . i & aj9 = a . (j + 1) holds ai > aj9 by A49, A54, A52; thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ::_thesis: verum proof let ai, aj be Nat; ::_thesis: ( i <> j & ai = a . i & aj = a . j implies ai > aj ) assume i <> j ; ::_thesis: ( not ai = a . i or not aj = a . j or ai > aj ) assume that A56: ai = a . i and A57: aj = a . j ; ::_thesis: ai > aj reconsider aj9 = a . (j + 1) as Nat ; aj in aj9 by A47, A57; then aj9 > aj by NAT_1:44; hence ai > aj by A55, A56, XXREAL_0:2; ::_thesis: verum end; end; end; A58: S5[ 0 ] ; A59: for l being Nat holds S5[l] from NAT_1:sch_2(A58, A48); A60: for i, j being Nat st i >= j holds ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ) ) proof let i, j be Nat; ::_thesis: ( i >= j implies ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ) ) ) assume A61: i >= j ; ::_thesis: ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj ) ) then A62: ex l being Nat st i = j + l by NAT_1:10; hence S . i c= S . j by A59, A61; ::_thesis: for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds ai > aj by A59, A61, A62; ::_thesis: verum end; A63: for i being Element of NAT for Y being set for 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 Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) proof let i be Element of NAT ; ::_thesis: for Y being set for 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 Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) let Y be set ; ::_thesis: for 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 Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; ::_thesis: ( Y = { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) ) assume A64: Y = { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > i ) } ; ::_thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) ) consider x2 being Element of A, y2 being Element of omega such that A65: S . (i + 1) = x2 and A66: a . (i + 1) = y2 ; consider x1 being Element of A, y1 being Element of omega such that A67: ( S . i = x1 & a . i = y1 ) ; ( y1 in x1 implies ( ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex 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 x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) ) ) by A41, A67, A65, A66; then consider F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k, H1 being Subset of (x1 \ {y1}) such that H1 is infinite and A68: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 ) and A69: for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) and for y29 being Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 by A47, A67; reconsider F1 = F1 as Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k by A67; assume A70: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; ::_thesis: ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds F1 . x19 = Fi . x19 proof let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); ::_thesis: F1 . x19 = Fi . x19 thus F1 . x19 = F . (x19 \/ {(a . i)}) by A67, A69 .= Fi . x19 by A70 ; ::_thesis: verum end; then A71: Fi | (the_subsets_of_card (n,(S . (i + 1)))) is constant by A65, A68, FUNCT_2:63; now__::_thesis:_for_x_being_set_st_x_in_Y_holds_ x_in_S_._(i_+_1) let x be set ; ::_thesis: ( x in Y implies x in S . (i + 1) ) assume x in Y ; ::_thesis: x in S . (i + 1) then ex x9 being Element of omega st ( x = x9 & ex j being Element of NAT st ( a . j = x9 & j > i ) ) by A64; then consider j being Element of NAT such that A72: a . j = x and A73: j > i ; j >= i + 1 by A73, NAT_1:13; then A74: S . j c= S . (i + 1) by A60; a . j in S . j by A47; hence x in S . (i + 1) by A72, A74; ::_thesis: verum end; hence Y c= S . (i + 1) by TARSKI:def_3; ::_thesis: Fi | (the_subsets_of_card (n,Y)) is constant then A75: the_subsets_of_card (n,Y) c= the_subsets_of_card (n,(S . (i + 1))) by Lm1; 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 ; ::_thesis: ( x in dom (Fi | (the_subsets_of_card (n,Y))) & y in dom (Fi | (the_subsets_of_card (n,Y))) implies (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y ) assume A76: x in dom (Fi | (the_subsets_of_card (n,Y))) ; ::_thesis: ( not y in dom (Fi | (the_subsets_of_card (n,Y))) or (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y ) then A77: x in the_subsets_of_card (n,Y) ; x in dom Fi by A76, RELAT_1:57; then A78: x in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by A75, A77, RELAT_1:57; assume A79: y in dom (Fi | (the_subsets_of_card (n,Y))) ; ::_thesis: (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y then A80: y in the_subsets_of_card (n,Y) ; y in dom Fi by A79, RELAT_1:57; then A81: y in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by A75, A80, RELAT_1:57; 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 A75, FUNCT_1:51 .= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . x by A77, FUNCT_1:49 .= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . y by A71, A78, A81, FUNCT_1:def_10 .= ((Fi | (the_subsets_of_card (n,(S . (i + 1))))) | (the_subsets_of_card (n,Y))) . y by A80, FUNCT_1:49 .= (Fi | (the_subsets_of_card (n,Y))) . y by A75, FUNCT_1:51 ; ::_thesis: verum end; hence Fi | (the_subsets_of_card (n,Y)) is constant by FUNCT_1:def_10; ::_thesis: verum 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 ; ::_thesis: ( x1 in dom a & x2 in dom a & a . x1 = a . x2 implies x1 = x2 ) assume x1 in dom a ; ::_thesis: ( not x2 in dom a or not a . x1 = a . x2 or x1 = x2 ) then reconsider i1 = x1 as Element of NAT ; assume x2 in dom a ; ::_thesis: ( not a . x1 = a . x2 or x1 = x2 ) then reconsider i2 = x2 as Element of NAT ; reconsider ai2 = a . i2 as Element of NAT ; reconsider ai1 = a . i1 as Element of NAT ; assume A82: a . x1 = a . x2 ; ::_thesis: x1 = x2 assume A83: x1 <> x2 ; ::_thesis: contradiction percases ( i1 < i2 or i1 > i2 ) by A83, XXREAL_0:1; suppose i1 < i2 ; ::_thesis: contradiction then ai1 < ai2 by A60; hence contradiction by A82; ::_thesis: verum end; suppose i1 > i2 ; ::_thesis: contradiction then ai1 > ai2 by A60; hence contradiction by A82; ::_thesis: verum end; end; end; then A84: a is one-to-one by FUNCT_1:def_4; A85: NAT = dom a by FUNCT_2:def_1; A86: for i being Element of NAT holds card { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } = omega proof let i be Element of NAT ; ::_thesis: card { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } = omega set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } ; now__::_thesis:_for_z_being_set_st_z_in__{__x9_where_x9_is_Element_of_omega_:_ex_j_being_Element_of_NAT_st_ (_a_._j_=_x9_&_j_>_i_)__}__holds_ z_in_NAT let z be set ; ::_thesis: ( z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } implies z in NAT ) assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } ; ::_thesis: z in NAT then ex z9 being Element of omega st ( z = z9 & ex j being Element of NAT st ( a . j = z9 & j > i ) ) ; hence z in NAT ; ::_thesis: verum end; then A87: { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } c= NAT by TARSKI:def_3; A88: dom (a | (NAT \ (Segm (i + 1)))) = (dom a) /\ (NAT \ (Segm (i + 1))) by RELAT_1:61 .= 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 { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } iff z in rng (a | (NAT \ (Segm (i + 1)))) ) proof let z be set ; ::_thesis: ( z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } iff z in rng (a | (NAT \ (Segm (i + 1)))) ) hereby ::_thesis: ( z in rng (a | (NAT \ (Segm (i + 1)))) implies z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } ) assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } ; ::_thesis: z in rng (a | (NAT \ (Segm (i + 1)))) then ex z9 being Element of omega st ( z = z9 & ex j being Element of NAT st ( a . j = z9 & j > i ) ) ; then consider j being Element of NAT such that A89: a . j = z and A90: j > i ; j >= i + 1 by A90, NAT_1:13; then not j in i + 1 by NAT_1:44; then j in NAT \ (Segm (i + 1)) by XBOOLE_0:def_5; hence z in rng (a | (NAT \ (Segm (i + 1)))) by A85, A89, FUNCT_1:50; ::_thesis: verum end; assume z in rng (a | (NAT \ (Segm (i + 1)))) ; ::_thesis: z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } then consider j being set such that A91: j in dom (a | (NAT \ (Segm (i + 1)))) and A92: z = (a | (NAT \ (Segm (i + 1)))) . j by FUNCT_1:def_3; j in dom a by A91, RELAT_1:57; then reconsider j = j as Element of NAT ; not j in Segm (i + 1) by A91, XBOOLE_0:def_5; then j >= i + 1 by NAT_1:44; then A93: j > i by NAT_1:13; a . j = z by A91, A92, FUNCT_1:47; hence z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } by A93; ::_thesis: verum end; then A94: { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } = rng (a | (NAT \ (Segm (i + 1)))) by TARSKI:1; a | (NAT \ (Segm (i + 1))) is one-to-one by A84, FUNCT_1:52; hence card { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } = omega by A88, A94, A87, Th2, CARD_1:59; ::_thesis: verum end; A95: for x being set st x in NAT holds ex y being set st ( y in k & S4[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in k & S4[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in k & S4[x,y] ) then reconsider i9 = x as Element of NAT ; set Y9 = S . i9; A96: not a . i9 in S . (i9 + 1) by A47; reconsider a9 = a . i9 as Element of S . i9 by A47; set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } ; A97: S . (i9 + 1) c= S . i9 by A47; S . i9 in A ; then ex Y99 being Subset of X st ( Y99 = S . i9 & card Y99 = omega ) ; then consider Fa being Function of (the_subsets_of_card (n,((S . i9) \ {a9}))),k, Ha being Subset of ((S . i9) \ {a9}) such that Ha is infinite and Fa | (the_subsets_of_card (n,Ha)) is constant and A98: for Y99 being Element of the_subsets_of_card (n,((S . i9) \ {a9})) holds Fa . Y99 = F . (Y99 \/ {a9}) by A7; A99: { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } c= S . (i9 + 1) by A63, A98; now__::_thesis:_for_x_being_set_st_x_in__{__x9_where_x9_is_Element_of_omega_:_ex_j_being_Element_of_NAT_st_ (_a_._j_=_x9_&_j_>_i9_)__}__holds_ x_in_(S_._i9)_\_{(a_._i9)} let x be set ; ::_thesis: ( x in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } implies x in (S . i9) \ {(a . i9)} ) assume x in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } ; ::_thesis: x in (S . i9) \ {(a . i9)} then A100: x in S . (i9 + 1) by A99; then not x in {(a . i9)} by A96, TARSKI:def_1; hence x in (S . i9) \ {(a . i9)} by A97, A100, XBOOLE_0:def_5; ::_thesis: verum end; then { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } c= (S . i9) \ {(a . i9)} by TARSKI:def_3; then the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } ) c= the_subsets_of_card (n,((S . i9) \ {a9})) by Lm1; then A101: Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } )) is Function of (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } )),k by A6, FUNCT_2:32; A102: not card { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } c= card n by A86; then not { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } is empty ; then A103: not the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } ) is empty by A102, GROUP_10:1; Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } )) is constant by A63, A98; then consider y being Element of k such that A104: rng (Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } ))) = {y} by A6, A101, A103, FUNCT_2:111; reconsider y = y as set ; take y ; ::_thesis: ( y in k & S4[x,y] ) thus y in k by A6; ::_thesis: S4[x,y] for Y being set for i being Element of NAT for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds ex l being Nat st ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) proof reconsider k9 = k as Element of NAT by ORDINAL1:def_12; let Y be set ; ::_thesis: for i being Element of NAT for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds ex l being Nat st ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) let i be Element of NAT ; ::_thesis: for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds ex l being Nat st ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; ::_thesis: ( i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ex l being Nat st ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) ) assume A105: i = x ; ::_thesis: ( not Y = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } or ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) ) k9 is Subset of NAT by STIRL2_1:8; then reconsider l = y as Nat ; assume A106: Y = { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } ; ::_thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) ) assume A107: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; ::_thesis: ex l being Nat st ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) take l ; ::_thesis: ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) thus l = y ; ::_thesis: ( l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) thus l in k by A6; ::_thesis: rng (Fi | (the_subsets_of_card (n,Y))) = {l} for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fa . x19 = Fi . x19 proof let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); ::_thesis: Fa . x19 = Fi . x19 thus Fa . x19 = F . (x19 \/ {(a . i)}) by A98, A105 .= Fi . x19 by A107 ; ::_thesis: verum end; hence rng (Fi | (the_subsets_of_card (n,Y))) = {l} by A104, A105, A106, FUNCT_2:63; ::_thesis: verum end; hence S4[x,y] ; ::_thesis: verum end; consider g being Function of NAT,k such that A108: for x being set st x in NAT holds S4[x,g . x] from FUNCT_2:sch_1(A95); g in Funcs (NAT,k) by A6, FUNCT_2:8; then ex g9 being Function st ( g = g9 & dom g9 = NAT & rng g9 c= k ) by FUNCT_2:def_2; then consider k9 being set such that k9 in rng g and A109: g " {k9} is infinite by CARD_2:101; set H = a .: (g " {k9}); g " {k9} c= dom g by RELAT_1:132; then g " {k9},a .: (g " {k9}) are_equipotent by A84, A85, CARD_1:33, XBOOLE_1:1; then A110: card (g " {k9}) = card (a .: (g " {k9})) by CARD_1:5; now__::_thesis:_for_y_being_set_st_y_in_a_.:_(g_"_{k9})_holds_ y_in_X let y be set ; ::_thesis: ( y in a .: (g " {k9}) implies y in X ) assume y in a .: (g " {k9}) ; ::_thesis: y in X then consider x being set such that A111: [x,y] in a and x in g " {k9} by RELAT_1:def_13; x in dom a by A111, FUNCT_1:1; then reconsider i = x as Element of NAT ; y = a . x by A111, FUNCT_1:1; then A112: y in S . i by A47; S . i in the_subsets_of_card (omega,X) ; hence y in X by A112; ::_thesis: verum end; then reconsider H = a .: (g " {k9}) as Subset of X by TARSKI:def_3; take H = H; ::_thesis: ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) thus H is infinite by A109, A110; ::_thesis: F | (the_subsets_of_card ((n + 1),H)) is constant A113: 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 = k9 proof let y be set ; ::_thesis: ( y in dom (F | (the_subsets_of_card ((n + 1),H))) implies (F | (the_subsets_of_card ((n + 1),H))) . y = k9 ) assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; ::_thesis: (F | (the_subsets_of_card ((n + 1),H))) . y = k9 then A114: y in the_subsets_of_card ((n + 1),H) by RELAT_1:57; then consider Y being Subset of H such that A115: y = Y and A116: card Y = n + 1 ; set y0 = min* Y; set Y9 = y \ {(min* Y)}; Y c= X by XBOOLE_1:1; then A117: Y c= NAT by A5, XBOOLE_1:1; then A118: min* Y in Y by A116, CARD_1:27, NAT_1:def_1; then consider x0 being set such that x0 in dom a and A119: x0 in g " {k9} and A120: min* Y = a . x0 by FUNCT_1:def_6; consider y09 being set such that y09 in rng g and A121: [x0,y09] in g and A122: y09 in {k9} by A119, RELAT_1:131; A123: x0 in dom g by A121, FUNCT_1:1; A124: g . x0 = y09 by A121, FUNCT_1:1; reconsider x0 = x0 as Element of NAT by A123; set Y0 = { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ; {(min* Y)} c= y by A115, A118, ZFMISC_1:31; then A125: (y \ {(min* Y)}) \/ {(a . x0)} = y by A120, XBOOLE_1:45; reconsider a9 = a . x0 as Element of S . x0 by A47; S . x0 in the_subsets_of_card (omega,X) ; then ex S0 being Subset of X st ( S0 = S . x0 & card S0 = omega ) ; then consider F0 being Function of (the_subsets_of_card (n,((S . x0) \ {a9}))),k, H0 being Subset of ((S . x0) \ {a9}) such that H0 is infinite and F0 | (the_subsets_of_card (n,H0)) is constant and A126: for Y9 being Element of the_subsets_of_card (n,((S . x0) \ {a9})) holds F0 . Y9 = F . (Y9 \/ {a9}) by A7; reconsider y9 = y as finite set by A115, A116; card (y \ {(min* Y)}) c= card y9 by CARD_1:11; then reconsider Y99 = y \ {(min* Y)} as finite set ; A127: { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } c= S . (x0 + 1) by A63, A126; now__::_thesis:_for_x_being_set_st_x_in_y_\_{(min*_Y)}_holds_ x_in__{__x_where_x_is_Element_of_omega_:_ex_j_being_Element_of_NAT_st_ (_a_._j_=_x_&_j_>_x0_)__}_ let x be set ; ::_thesis: ( x in y \ {(min* Y)} implies x in { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ) assume A128: x in y \ {(min* Y)} ; ::_thesis: x in { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } then A129: x in y ; then consider j being set such that A130: j in dom a and j in g " {k9} and A131: x = a . j by A115, FUNCT_1:def_6; reconsider x9 = x as Element of omega by A115, A117, A129; A132: not x in {(min* Y)} by A128, XBOOLE_0:def_5; ex j being Element of NAT st ( a . j = x9 & j > x0 ) proof reconsider j = j as Element of NAT by A130; take j ; ::_thesis: ( a . j = x9 & j > x0 ) thus a . j = x9 by A131; ::_thesis: j > x0 A133: min* Y <= x9 by A115, A117, A128, NAT_1:def_1; thus j > x0 ::_thesis: verum proof assume A134: x0 >= j ; ::_thesis: contradiction x0 <> j by A120, A132, A131, TARSKI:def_1; hence contradiction by A60, A120, A131, A133, A134; ::_thesis: verum end; end; hence x in { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ; ::_thesis: verum end; then A135: y \ {(min* Y)} is Subset of { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } by TARSKI:def_3; min* Y in {(min* Y)} by TARSKI:def_1; then not a . x0 in y \ {(min* Y)} by A120, XBOOLE_0:def_5; then card y9 = (card Y99) + 1 by A125, CARD_2:41; then A136: y \ {(min* Y)} in the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ) by A115, A116, A135; ex l being Nat st ( l = g . x0 & l in k & rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ))) = {l} ) by A108, A126; then A137: rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ))) = {k9} by A122, A124, TARSKI:def_1; S . (x0 + 1) c= S . x0 by A47; then { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } c= S . x0 by A127, XBOOLE_1:1; then A138: { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } \ {(a . x0)} c= (S . x0) \ {(a . x0)} by XBOOLE_1:33; not a . x0 in { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } by A47, A127; then { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } c= (S . x0) \ {(a . x0)} by A138, ZFMISC_1:57; then A139: the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ) c= the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by Lm1; then A140: y \ {(min* Y)} in the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by A136; reconsider Y9 = y \ {(min* Y)} as Element of the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by A139, A136; Y9 in dom F0 by A6, A140, FUNCT_2:def_1; then Y9 in dom (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ))) by A136, RELAT_1:57; then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ))) . Y9 in rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ))) by FUNCT_1:3; then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st ( a . j = x & j > x0 ) } ))) . Y9 = k9 by A137, TARSKI:def_1; then A141: F0 . Y9 = k9 by A136, FUNCT_1:49; F0 . Y9 = F . (Y9 \/ {(a . x0)}) by A126; hence (F | (the_subsets_of_card ((n + 1),H))) . y = k9 by A114, A125, A141, FUNCT_1:49; ::_thesis: verum 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 ; ::_thesis: ( x in dom (F | (the_subsets_of_card ((n + 1),H))) & y in dom (F | (the_subsets_of_card ((n + 1),H))) implies (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y ) assume x in dom (F | (the_subsets_of_card ((n + 1),H))) ; ::_thesis: ( not y in dom (F | (the_subsets_of_card ((n + 1),H))) or (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y ) then A142: (F | (the_subsets_of_card ((n + 1),H))) . x = k9 by A113; assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; ::_thesis: (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y hence (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y by A113, A142; ::_thesis: verum end; hence F | (the_subsets_of_card ((n + 1),H)) is constant by FUNCT_1:def_10; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A143: S1[ 0 ] proof let k be Nat; ::_thesis: for X being set for F being Function of (the_subsets_of_card (0,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 (0,H)) is constant ) let X be set ; ::_thesis: for F being Function of (the_subsets_of_card (0,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 (0,H)) is constant ) set H = X; X c= X ; then reconsider H = X as Subset of X ; let F be Function of (the_subsets_of_card (0,X)),k; ::_thesis: ( card X = omega & X c= omega & k <> 0 implies ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) ) assume A144: card X = omega ; ::_thesis: ( not X c= omega or not k <> 0 or ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) ) assume X c= omega ; ::_thesis: ( not k <> 0 or ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) ) assume k <> 0 ; ::_thesis: ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) take H ; ::_thesis: ( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) thus H is infinite by A144; ::_thesis: F | (the_subsets_of_card (0,H)) is constant for x, y being set st x in dom (F | (the_subsets_of_card (0,H))) & y in dom (F | (the_subsets_of_card (0,H))) holds (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y proof let x, y be set ; ::_thesis: ( 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 ) assume A145: x in dom (F | (the_subsets_of_card (0,H))) ; ::_thesis: ( not y in dom (F | (the_subsets_of_card (0,H))) or (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y ) A146: dom (F | (the_subsets_of_card (0,H))) = dom (F | {0}) by Lm2 .= (dom F) /\ {0} by RELAT_1:61 ; assume y in dom (F | (the_subsets_of_card (0,H))) ; ::_thesis: (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y then y in {0} by A146, XBOOLE_0:def_4; then A147: y = 0 by TARSKI:def_1; x in {0} by A146, A145, XBOOLE_0:def_4; hence (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y by A147, TARSKI:def_1; ::_thesis: verum end; hence F | (the_subsets_of_card (0,H)) is constant by FUNCT_1:def_10; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A143, A1); hence for F being Function of (the_subsets_of_card (n,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 (n,H)) is constant ) ; ::_thesis: verum end; theorem :: RAMSEY_1:5 for X being set holds the_subsets_of_card (0,X) = {0} by Lm2; theorem Th6: :: RAMSEY_1:6 for n being Nat for X being finite set st card X < n holds the_subsets_of_card (n,X) is empty proof let n be Nat; ::_thesis: for X being finite set st card X < n holds the_subsets_of_card (n,X) is empty let X be finite set ; ::_thesis: ( card X < n implies the_subsets_of_card (n,X) is empty ) assume A1: card X < n ; ::_thesis: the_subsets_of_card (n,X) is empty A2: card (Seg n) = n by FINSEQ_1:57; assume not the_subsets_of_card (n,X) is empty ; ::_thesis: contradiction then consider x being set such that A3: x in the_subsets_of_card (n,X) by XBOOLE_0:def_1; ex X9 being Subset of X st ( x = X9 & card X9 = n ) by A3; then card (Seg n) c= card X by A2, CARD_1:11; then card (Seg n) <= card X by NAT_1:39; hence contradiction by A1, FINSEQ_1:57; ::_thesis: verum end; theorem :: RAMSEY_1:7 for X, Y, Z being set st X c= Y holds the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) by Lm1; theorem :: RAMSEY_1:8 for X, Y being set st X is finite & Y is finite & card Y = X holds the_subsets_of_card (X,Y) = {Y} by Lm3; theorem :: RAMSEY_1:9 for X, Y being set for f being Function of X,Y st not X is empty & not Y is empty holds ( f is constant iff ex y being Element of Y st rng f = {y} ) by FUNCT_2:111; theorem Th10: :: RAMSEY_1:10 for k being Nat for X being finite set st k <= card X holds ex Y being Subset of X st card Y = k proof let k be Nat; ::_thesis: for X being finite set st k <= card X holds ex Y being Subset of X st card Y = k let X be finite set ; ::_thesis: ( k <= card X implies ex Y being Subset of X st card Y = k ) assume k <= card X ; ::_thesis: ex Y being Subset of X st card Y = k then card k <= card X by CARD_1:def_2; then card k c= card X by NAT_1:39; then consider Y being set such that A1: Y c= X and A2: card Y = card k by CARD_FIL:36; reconsider Y = Y as Subset of X by A1; take Y ; ::_thesis: card Y = k thus card Y = k by A2, CARD_1:def_2; ::_thesis: verum end; theorem Th11: :: RAMSEY_1:11 for m, n being Nat st m >= 1 holds n + 1 <= (n + m) choose m proof let m, n be Nat; ::_thesis: ( m >= 1 implies n + 1 <= (n + m) choose m ) defpred S1[ Nat] means for n being Element of NAT st $1 >= 1 holds n + 1 <= (n + $1) choose $1; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) set k9 = k + 1; reconsider k9 = k + 1 as Element of NAT ; assume A2: S1[k] ; ::_thesis: S1[k + 1] for n being Element of NAT st k9 >= 1 holds n + 1 <= (n + k9) choose k9 proof let n be Element of NAT ; ::_thesis: ( k9 >= 1 implies n + 1 <= (n + k9) choose k9 ) assume A3: k9 >= 1 ; ::_thesis: n + 1 <= (n + k9) choose k9 percases ( k + 1 = 1 or k >= 1 ) by A3, NAT_1:8; supposeA4: k + 1 = 1 ; ::_thesis: n + 1 <= (n + k9) choose k9 n + 1 >= 0 + 1 by XREAL_1:6; hence n + 1 <= (n + k9) choose k9 by A4, NEWTON:23; ::_thesis: verum end; supposeA5: k >= 1 ; ::_thesis: n + 1 <= (n + k9) choose k9 A6: (n + k9) choose k9 = ((n + k) + 1) choose (k + 1) .= ((n + k) choose (k + 1)) + ((n + k) choose k) by NEWTON:22 ; n + 1 <= (n + k) choose k by A2, A5; then A7: (n + 1) + ((n + k) choose (k + 1)) <= (n + k9) choose k9 by A6, XREAL_1:6; 0 + (n + 1) <= ((n + k) choose (k + 1)) + (n + 1) by XREAL_1:6; hence n + 1 <= (n + k9) choose k9 by A7, XXREAL_0:2; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; reconsider n9 = n as Element of NAT by ORDINAL1:def_12; reconsider m9 = m as Element of NAT by ORDINAL1:def_12; assume A8: m >= 1 ; ::_thesis: n + 1 <= (n + m) choose m A9: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A1); then n9 + 1 <= (n9 + m9) choose m9 by A8; hence n + 1 <= (n + m) choose m ; ::_thesis: verum end; theorem Th12: :: RAMSEY_1:12 for m, n being Nat st m >= 1 & n >= 1 holds m + 1 <= (n + m) choose m proof let m, n be Nat; ::_thesis: ( m >= 1 & n >= 1 implies m + 1 <= (n + m) choose m ) defpred S1[ Nat] means for n being Element of NAT st $1 >= 1 & n >= 1 holds $1 + 1 <= (n + $1) choose $1; assume A1: ( m >= 1 & n >= 1 ) ; ::_thesis: m + 1 <= (n + m) choose m reconsider n9 = n as Element of NAT by ORDINAL1:def_12; reconsider m9 = m as Element of NAT by ORDINAL1:def_12; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) set k9 = k + 1; reconsider k9 = k + 1 as Element of NAT ; assume A3: S1[k] ; ::_thesis: S1[k + 1] for n being Element of NAT st k9 >= 1 & n >= 1 holds k9 + 1 <= (n + k9) choose k9 proof let n be Element of NAT ; ::_thesis: ( k9 >= 1 & n >= 1 implies k9 + 1 <= (n + k9) choose k9 ) assume A4: k9 >= 1 ; ::_thesis: ( not n >= 1 or k9 + 1 <= (n + k9) choose k9 ) assume A5: n >= 1 ; ::_thesis: k9 + 1 <= (n + k9) choose k9 percases ( k + 1 = 1 or k >= 1 ) by A4, NAT_1:8; supposeA6: k + 1 = 1 ; ::_thesis: k9 + 1 <= (n + k9) choose k9 ( n + 1 >= 0 + 1 & n + 1 >= 1 + 1 ) by A5, XREAL_1:6; hence k9 + 1 <= (n + k9) choose k9 by A6, NEWTON:23; ::_thesis: verum end; supposeA7: k >= 1 ; ::_thesis: k9 + 1 <= (n + k9) choose k9 set k99 = k + 1; A8: (n + k9) choose k9 = ((n + k) + 1) choose (k + 1) .= ((n + k) choose (k + 1)) + ((n + k) choose k) by NEWTON:22 ; k + 1 >= 0 + 1 by XREAL_1:6; then A9: (n -' 1) + 1 <= ((n -' 1) + (k + 1)) choose (k + 1) by Th11; n - 1 >= 1 - 1 by A5, XREAL_1:9; then n -' 1 = n - 1 by XREAL_0:def_2; then 1 <= (n + k) choose (k + 1) by A5, A9, XXREAL_0:2; then A10: 1 + (k + 1) <= ((n + k) choose (k + 1)) + (k + 1) by XREAL_1:6; k + 1 <= (n + k) choose k by A3, A5, A7; then (k + 1) + ((n + k) choose (k + 1)) <= (n + k9) choose k9 by A8, XREAL_1:6; hence k9 + 1 <= (n + k9) choose k9 by A10, XXREAL_0:2; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A11: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A2); then m9 + 1 <= (n9 + m9) choose m9 by A1; hence m + 1 <= (n + m) choose m ; ::_thesis: verum end; theorem Th13: :: RAMSEY_1:13 for X being non empty set for p1, p2 being Element of X for P being a_partition of X for 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 ; ::_thesis: for p1, p2 being Element of X for P being a_partition of X for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds p2 in A let p1, p2 be Element of X; ::_thesis: for P being a_partition of X for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds p2 in A let P be a_partition of X; ::_thesis: for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds p2 in A let A be Element of P; ::_thesis: ( p1 in A & (proj P) . p1 = (proj P) . p2 implies p2 in A ) assume A1: p1 in A ; ::_thesis: ( not (proj P) . p1 = (proj P) . p2 or p2 in A ) assume (proj P) . p1 = (proj P) . p2 ; ::_thesis: p2 in A then A2: (proj P) . p2 = A by A1, EQREL_1:65; assume A3: not p2 in A ; ::_thesis: contradiction union P = X by EQREL_1:def_4; then consider B being set such that A4: p2 in B and A5: B in P by TARSKI:def_4; reconsider B = B as Element of P by A5; A6: (proj P) . p2 = B by A4, EQREL_1:65; percases ( A = B or A misses B ) by EQREL_1:def_4; suppose A = B ; ::_thesis: contradiction hence contradiction by A3, A4; ::_thesis: verum end; suppose A misses B ; ::_thesis: contradiction then A /\ A = {} by A2, A6, XBOOLE_0:def_7; hence contradiction by EQREL_1:def_4; ::_thesis: verum end; end; end; begin theorem Th14: :: RAMSEY_1:14 for n, k being Nat for X being set for F being Function of (the_subsets_of_card (n,X)),k st k <> 0 & X is infinite holds ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) proof let n, k be Nat; ::_thesis: for X being set for F being Function of (the_subsets_of_card (n,X)),k st k <> 0 & X is infinite holds ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) let X be set ; ::_thesis: for F being Function of (the_subsets_of_card (n,X)),k st k <> 0 & X is infinite holds ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) let F be Function of (the_subsets_of_card (n,X)),k; ::_thesis: ( k <> 0 & X is infinite implies ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) ) assume that A1: k <> 0 and A2: X is infinite ; ::_thesis: ex H being Subset of X st ( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) F in Funcs ((the_subsets_of_card (n,X)),k) by A1, FUNCT_2:8; then A3: ex g1 being Function st ( F = g1 & dom g1 = the_subsets_of_card (n,X) & rng g1 c= k ) by FUNCT_2:def_2; consider Y being set such that A4: Y c= X and A5: card Y = omega by A2, CARD_3:87; reconsider Y = Y as non empty set by A5; Y, omega are_equipotent by A5, CARD_1:5, CARD_1:47; then consider f being Function such that A6: f is one-to-one and A7: dom f = omega and A8: rng f = Y by WELLORD2:def_4; reconsider f = f as Function of omega,Y by A7, A8, FUNCT_2:1; not card Y c= card n by A5; then not the_subsets_of_card (n,Y) is empty by GROUP_10:1; then f ||^ n in Funcs ((the_subsets_of_card (n,omega)),(the_subsets_of_card (n,Y))) by FUNCT_2:8; then A9: ex g2 being Function st ( 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; set F9 = F * (f ||^ n); the_subsets_of_card (n,Y) c= the_subsets_of_card (n,X) by A4, Lm1; then A10: dom (F * (f ||^ n)) = the_subsets_of_card (n,omega) by A3, A9, RELAT_1:27, XBOOLE_1:1; A11: rng (F * (f ||^ n)) c= rng F by RELAT_1:26; then A12: rng (F * (f ||^ n)) c= k by A3, XBOOLE_1:1; reconsider F9 = F * (f ||^ n) as Function of (the_subsets_of_card (n,omega)),k by A3, A10, A11, FUNCT_2:2, XBOOLE_1:1; consider H9 being Subset of omega such that A13: H9 is infinite and A14: F9 | (the_subsets_of_card (n,H9)) is constant by A1, Lm4, CARD_1:47; A15: rng (F9 | (the_subsets_of_card (n,H9))) c= rng F9 by RELAT_1:70; set H = f .: H9; f .: H9 c= rng f by RELAT_1:111; then reconsider H = f .: H9 as Subset of X by A4, A8, XBOOLE_1:1; take H ; ::_thesis: ( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) H9,f .: H9 are_equipotent by A6, A7, CARD_1:33; hence H is infinite by A13, CARD_1:38; ::_thesis: F | (the_subsets_of_card (n,H)) is constant dom (F9 | (the_subsets_of_card (n,H9))) = the_subsets_of_card (n,H9) by A10, Lm1, RELAT_1:62; then F9 | (the_subsets_of_card (n,H9)) is Function of (the_subsets_of_card (n,H9)),k by A12, A15, FUNCT_2:2, XBOOLE_1:1; then consider y being Element of k such that A17: rng (F9 | (the_subsets_of_card (n,H9))) = {y} by A1, A13, A14, FUNCT_2:111; A18: not card omega c= card n ; A19: ex y being Element of k st rng (F | (the_subsets_of_card (n,H))) = {y} proof take y ; ::_thesis: rng (F | (the_subsets_of_card (n,H))) = {y} thus rng (F | (the_subsets_of_card (n,H))) = F .: (the_subsets_of_card (n,H)) by RELAT_1:115 .= F .: ((f ||^ n) .: (the_subsets_of_card (n,H9))) by A6, A18, Th1 .= F9 .: (the_subsets_of_card (n,H9)) by RELAT_1:126 .= {y} by A17, RELAT_1:115 ; ::_thesis: verum end; thus F | (the_subsets_of_card (n,H)) is constant by A19; ::_thesis: verum end; theorem :: RAMSEY_1:15 for n, k being Nat for X being infinite set for 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 n, k be Nat; ::_thesis: for X being infinite set for 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 ) let X be infinite set ; ::_thesis: for 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 ) let P be a_partition of the_subsets_of_card (n,X); ::_thesis: ( card P = k implies ex H being Subset of X st ( H is infinite & H is_homogeneous_for P ) ) assume A1: card P = k ; ::_thesis: ex H being Subset of X st ( H is infinite & H is_homogeneous_for P ) then P,k are_equipotent by CARD_1:def_2; then consider F1 being Function such that A2: F1 is one-to-one and A3: dom F1 = P and A4: rng F1 = k by WELLORD2:def_4; reconsider F1 = F1 as Function of P,k by A3, A4, FUNCT_2:1; set F = F1 * (proj P); reconsider F = F1 * (proj P) as Function of (the_subsets_of_card (n,X)),k ; consider H being Subset of X such that A5: H is infinite and A6: F | (the_subsets_of_card (n,H)) is constant by A1, Th14; take H ; ::_thesis: ( H is infinite & H is_homogeneous_for P ) thus H is infinite by A5; ::_thesis: H is_homogeneous_for P set h = the Element of the_subsets_of_card (n,H); not the_subsets_of_card (n,H) is empty by A5; then A7: the Element of the_subsets_of_card (n,H) in the_subsets_of_card (n,H) ; A8: the_subsets_of_card (n,H) c= the_subsets_of_card (n,X) by Lm1; then reconsider h = the Element of the_subsets_of_card (n,H) as Element of the_subsets_of_card (n,X) by A7; set E = EqClass (h,P); reconsider E = EqClass (h,P) as Element of P by EQREL_1:def_6; for x being set st x in the_subsets_of_card (n,H) holds x in E proof let x be set ; ::_thesis: ( x in the_subsets_of_card (n,H) implies x in E ) assume A9: x in the_subsets_of_card (n,H) ; ::_thesis: x in E then reconsider x9 = x as Element of the_subsets_of_card (n,X) by A8; A10: dom F = the_subsets_of_card (n,X) by A1, FUNCT_2:def_1; then h in (dom F) /\ (the_subsets_of_card (n,H)) by A5, XBOOLE_0:def_4; then A11: h in dom (F | (the_subsets_of_card (n,H))) by RELAT_1:61; x9 in (dom F) /\ (the_subsets_of_card (n,H)) by A9, A10, XBOOLE_0:def_4; then A12: x9 in dom (F | (the_subsets_of_card (n,H))) by RELAT_1:61; F . x9 = (F | (the_subsets_of_card (n,H))) . x9 by A9, FUNCT_1:49 .= (F | (the_subsets_of_card (n,H))) . h by A6, A12, A11, FUNCT_1:def_10 .= F . h by A5, FUNCT_1:49 ; then F1 . ((proj P) . x9) = (F1 * (proj P)) . h by A10, FUNCT_1:12 .= F1 . ((proj P) . h) by A10, FUNCT_1:12 ; then ( h in E & (proj P) . h = (proj P) . x9 ) by A2, A3, EQREL_1:def_6, FUNCT_1:def_4; hence x in E by Th13; ::_thesis: verum end; then the_subsets_of_card (n,H) c= E by TARSKI:def_3; hence H is_homogeneous_for P by Def1; ::_thesis: verum end; begin scheme :: RAMSEY_1:sch 1 BinInd2{ P1[ Nat, Nat] } : for m, n being Nat holds P1[m,n] provided A1: for n being Nat holds ( P1[ 0 ,n] & P1[n, 0 ] ) and A2: for m, n being Nat st P1[m + 1,n] & P1[m,n + 1] holds P1[m + 1,n + 1] proof defpred S1[ Nat] means for m, n being Nat st m + n = $1 holds P1[m,n]; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] for m, n being Nat st m + n = k + 1 holds P1[m,n] proof let m, n be Nat; ::_thesis: ( m + n = k + 1 implies P1[m,n] ) assume A5: m + n = k + 1 ; ::_thesis: P1[m,n] percases ( m = 0 or n = 0 or ( m <> 0 & n <> 0 ) ) ; suppose ( m = 0 or n = 0 ) ; ::_thesis: P1[m,n] hence P1[m,n] by A1; ::_thesis: verum end; supposeA6: ( m <> 0 & n <> 0 ) ; ::_thesis: P1[m,n] then reconsider m9 = m - 1 as Element of NAT by NAT_1:20; reconsider n9 = n - 1 as Element of NAT by A6, NAT_1:20; m9 + n = k by A5; then A7: P1[m9,n9 + 1] by A4; m + n9 = k by A5; then P1[m9 + 1,n9] by A4; hence P1[m,n] by A2, A7; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; let m, n be Nat; ::_thesis: P1[m,n] set k = m + n; reconsider k = m + n as Element of NAT by ORDINAL1:def_12; A8: S1[ 0 ] proof let m, n be Nat; ::_thesis: ( m + n = 0 implies P1[m,n] ) assume m + n = 0 ; ::_thesis: P1[m,n] then m = 0 ; hence P1[m,n] by A1; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A8, A3); then S1[k] ; hence P1[m,n] ; ::_thesis: verum end; theorem Th16: :: RAMSEY_1:16 for m, n being Nat st m >= 2 & n >= 2 holds ex r being Nat st ( r <= ((m + n) -' 2) choose (m -' 1) & r >= 2 & ( for X being finite set for 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 let m, n be Nat; ::_thesis: ( m >= 2 & n >= 2 implies ex r being Nat st ( r <= ((m + n) -' 2) choose (m -' 1) & r >= 2 & ( for X being finite set for 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} ) ) ) ) ) defpred S1[ Nat, Nat] means ( $1 >= 2 & $2 >= 2 implies ex r being Nat st ( r <= (($1 + $2) -' 2) choose ($1 -' 1) & r >= 2 & ( for X being finite set for 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 m, n being Nat st S1[m + 1,n] & S1[m,n + 1] holds S1[m + 1,n + 1] proof let m, n be Nat; ::_thesis: ( S1[m + 1,n] & S1[m,n + 1] implies S1[m + 1,n + 1] ) assume A2: S1[m + 1,n] ; ::_thesis: ( not S1[m,n + 1] or S1[m + 1,n + 1] ) assume A3: S1[m,n + 1] ; ::_thesis: S1[m + 1,n + 1] assume that A4: m + 1 >= 2 and A5: n + 1 >= 2 ; ::_thesis: ex r being Nat st ( r <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r >= 2 & ( for X being finite set for 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) percases ( m + 1 < 2 or n + 1 < 2 or m + 1 = 2 or n + 1 = 2 or ( m + 1 > 2 & n + 1 > 2 ) ) by XXREAL_0:1; suppose ( m + 1 < 2 or n + 1 < 2 ) ; ::_thesis: ex r being Nat st ( r <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r >= 2 & ( for X being finite set for 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) hence ex r being Nat st ( r <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r >= 2 & ( for X being finite set for 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 + 1 & 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, A5; ::_thesis: verum end; supposeA6: m + 1 = 2 ; ::_thesis: ex r being Nat st ( r <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r >= 2 & ( for X being finite set for 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) set r = n + 1; take n + 1 ; ::_thesis: ( n + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & n + 1 >= 2 & ( for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) (m + 1) + (n + 1) >= 2 + 2 by A4, A5, XREAL_1:7; then ((m + 1) + (n + 1)) - 2 >= 4 - 2 by XREAL_1:9; then A7: m + n = ((m + 1) + (n + 1)) -' 2 by XREAL_0:def_2; ( (m + 1) -' 1 = m & (m + 1) - 1 >= 2 - 1 ) by A4, NAT_D:34, XREAL_1:9; hence n + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A7, Th11; ::_thesis: ( n + 1 >= 2 & ( for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) thus n + 1 >= 2 by A5; ::_thesis: for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) let X be finite set ; ::_thesis: for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) let F be Function of (the_subsets_of_card (2,X)),(Seg 2); ::_thesis: ( card X >= n + 1 implies ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) assume A8: card X >= n + 1 ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) F in Funcs ((the_subsets_of_card (2,X)),(Seg 2)) by FUNCT_2:8; then A9: ex f being Function st ( F = f & dom f = the_subsets_of_card (2,X) & rng f c= Seg 2 ) by FUNCT_2:def_2; percases ( not 1 in rng F or 1 in rng F ) ; supposeA10: not 1 in rng F ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) consider S being Subset of X such that A11: card S = n + 1 by A8, Th10; card 2 <= card S by A5, A11, CARD_1:def_2; then card 2 c= card S by NAT_1:39; then not the_subsets_of_card (2,S) is empty by A11, CARD_1:27, GROUP_10:1; then A12: ex x being set st x in the_subsets_of_card (2,S) by XBOOLE_0:def_1; take S ; ::_thesis: ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) A13: rng (F | (the_subsets_of_card (2,S))) c= rng F by RELAT_1:70; then A14: rng (F | (the_subsets_of_card (2,S))) c= {1,2} by A9, FINSEQ_1:2, XBOOLE_1:1; the_subsets_of_card (2,S) c= the_subsets_of_card (2,X) by Lm1; then A15: F | (the_subsets_of_card (2,S)) <> {} by A9, A12; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_rng_(F_|_(the_subsets_of_card_(2,S)))_implies_x_=_2_)_&_(_x_=_2_implies_x_in_rng_(F_|_(the_subsets_of_card_(2,S)))_)_) let x be set ; ::_thesis: ( ( x in rng (F | (the_subsets_of_card (2,S))) implies x = 2 ) & ( x = 2 implies x in rng (F | (the_subsets_of_card (2,S))) ) ) A16: ( 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 A14, ZFMISC_1:36; hereby ::_thesis: ( x = 2 implies x in rng (F | (the_subsets_of_card (2,S))) ) assume A17: x in rng (F | (the_subsets_of_card (2,S))) ; ::_thesis: x = 2 then ( x = 1 or x = 2 ) by A14, TARSKI:def_2; hence x = 2 by A10, A13, A17; ::_thesis: verum end; assume A18: x = 2 ; ::_thesis: x in rng (F | (the_subsets_of_card (2,S))) A19: not 1 in rng (F | (the_subsets_of_card (2,S))) by A10, A13; assume not x in rng (F | (the_subsets_of_card (2,S))) ; ::_thesis: contradiction hence contradiction by A15, A18, A19, A16, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum end; hence ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by A11, TARSKI:def_1; ::_thesis: verum end; suppose 1 in rng F ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) then consider S being set such that A20: S in dom F and A21: 1 = F . S by FUNCT_1:def_3; S in { X9 where X9 is Subset of X : card X9 = 2 } by A20; then A22: ex X9 being Subset of X st ( S = X9 & card X9 = 2 ) ; then reconsider S = S as Subset of X ; the_subsets_of_card (2,S) = {S} by A22, Lm3; then S in the_subsets_of_card (2,S) by TARSKI:def_1; then A23: (F | (the_subsets_of_card (2,S))) . S = 1 by A21, FUNCT_1:49; take S ; ::_thesis: ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) A24: {S} c= dom F by A20, ZFMISC_1:31; dom (F | (the_subsets_of_card (2,S))) = (dom F) /\ (the_subsets_of_card (2,S)) by RELAT_1:61 .= (dom F) /\ {S} by A22, Lm3 .= {S} by A24, XBOOLE_1:28 ; hence ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by A6, A22, A23, FUNCT_1:4; ::_thesis: verum end; end; end; supposeA25: n + 1 = 2 ; ::_thesis: ex r being Nat st ( r <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r >= 2 & ( for X being finite set for 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) set r = m + 1; take m + 1 ; ::_thesis: ( m + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & m + 1 >= 2 & ( for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) A26: (n + 1) - 1 >= 2 - 1 by A5, XREAL_1:9; (m + 1) + (n + 1) >= 2 + 2 by A4, A5, XREAL_1:7; then ((m + 1) + (n + 1)) - 2 >= 4 - 2 by XREAL_1:9; then A27: m + n = ((m + 1) + (n + 1)) -' 2 by XREAL_0:def_2; ( (m + 1) -' 1 = m & (m + 1) - 1 >= 2 - 1 ) by A4, NAT_D:34, XREAL_1:9; hence m + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A27, A26, Th12; ::_thesis: ( m + 1 >= 2 & ( for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) thus m + 1 >= 2 by A4; ::_thesis: for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) let X be finite set ; ::_thesis: for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) let F be Function of (the_subsets_of_card (2,X)),(Seg 2); ::_thesis: ( card X >= m + 1 implies ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) assume A28: card X >= m + 1 ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) F in Funcs ((the_subsets_of_card (2,X)),(Seg 2)) by FUNCT_2:8; then A29: ex f being Function st ( F = f & dom f = the_subsets_of_card (2,X) & rng f c= Seg 2 ) by FUNCT_2:def_2; percases ( not 2 in rng F or 2 in rng F ) ; supposeA30: not 2 in rng F ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) consider S being Subset of X such that A31: card S = m + 1 by A28, Th10; card 2 <= card S by A4, A31, CARD_1:def_2; then card 2 c= card S by NAT_1:39; then not the_subsets_of_card (2,S) is empty by A31, CARD_1:27, GROUP_10:1; then A32: ex x being set st x in the_subsets_of_card (2,S) by XBOOLE_0:def_1; take S ; ::_thesis: ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) A33: rng (F | (the_subsets_of_card (2,S))) c= rng F by RELAT_1:70; then A34: rng (F | (the_subsets_of_card (2,S))) c= {1,2} by A29, FINSEQ_1:2, XBOOLE_1:1; the_subsets_of_card (2,S) c= the_subsets_of_card (2,X) by Lm1; then A35: F | (the_subsets_of_card (2,S)) <> {} by A29, A32; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_rng_(F_|_(the_subsets_of_card_(2,S)))_implies_x_=_1_)_&_(_x_=_1_implies_x_in_rng_(F_|_(the_subsets_of_card_(2,S)))_)_) let x be set ; ::_thesis: ( ( x in rng (F | (the_subsets_of_card (2,S))) implies x = 1 ) & ( x = 1 implies x in rng (F | (the_subsets_of_card (2,S))) ) ) A36: ( 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 A34, ZFMISC_1:36; hereby ::_thesis: ( x = 1 implies x in rng (F | (the_subsets_of_card (2,S))) ) assume A37: x in rng (F | (the_subsets_of_card (2,S))) ; ::_thesis: x = 1 then ( x = 1 or x = 2 ) by A34, TARSKI:def_2; hence x = 1 by A30, A33, A37; ::_thesis: verum end; assume A38: x = 1 ; ::_thesis: x in rng (F | (the_subsets_of_card (2,S))) A39: not 2 in rng (F | (the_subsets_of_card (2,S))) by A30, A33; assume not x in rng (F | (the_subsets_of_card (2,S))) ; ::_thesis: contradiction hence contradiction by A35, A38, A39, A36, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum end; hence ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by A31, TARSKI:def_1; ::_thesis: verum end; suppose 2 in rng F ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) then consider S being set such that A40: S in dom F and A41: 2 = F . S by FUNCT_1:def_3; S in { X9 where X9 is Subset of X : card X9 = 2 } by A40; then A42: ex X9 being Subset of X st ( S = X9 & card X9 = 2 ) ; then reconsider S = S as Subset of X ; the_subsets_of_card (2,S) = {S} by A42, Lm3; then S in the_subsets_of_card (2,S) by TARSKI:def_1; then A43: (F | (the_subsets_of_card (2,S))) . S = 2 by A41, FUNCT_1:49; take S ; ::_thesis: ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) A44: {S} c= dom F by A40, ZFMISC_1:31; dom (F | (the_subsets_of_card (2,S))) = (dom F) /\ (the_subsets_of_card (2,S)) by RELAT_1:61 .= (dom F) /\ {S} by A42, Lm3 .= {S} by A44, XBOOLE_1:28 ; hence ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by A25, A42, A43, FUNCT_1:4; ::_thesis: verum end; end; end; supposeA45: ( m + 1 > 2 & n + 1 > 2 ) ; ::_thesis: ex r being Nat st ( r <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r >= 2 & ( for X being finite set for 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) set t = (m + n) -' 1; set s = m -' 1; (m + 1) - 2 >= 2 - 2 by A4, XREAL_1:9; then m -' 1 = m - 1 by XREAL_0:def_2; then A46: (m + 1) -' 1 = (m -' 1) + 1 by NAT_D:34; (m + 1) + (n + 1) >= 2 + 2 by A4, A5, XREAL_1:7; then A47: ((m + n) + 2) - 3 >= 4 - 3 by XREAL_1:9; then A48: (m + n) -' 1 = (m + n) - 1 by XREAL_0:def_2; A49: ((m + n) + 1) -' 2 = ((m + n) + 1) - 2 by A47, XREAL_0:def_2; m + n >= 0 ; then A50: ((m + 1) + (n + 1)) -' 2 = ((m + 1) + (n + 1)) - 2 by XREAL_0:def_2 .= ((m + n) -' 1) + 1 by A48 ; consider r2 being Nat such that A51: r2 <= ((m + (n + 1)) -' 2) choose (m -' 1) and r2 >= 2 and A52: for X being finite set for 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 A3, A45, NAT_1:13; consider r1 being Nat such that A53: r1 <= (((m + 1) + n) -' 2) choose ((m + 1) -' 1) and A54: r1 >= 2 and A55: for X being finite set for 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 A2, A45, NAT_1:13; set r = r1 + r2; take r1 + r2 ; ::_thesis: ( r1 + r2 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r1 + r2 >= 2 & ( for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) r1 + r2 <= ((((m + 1) + n) -' 2) choose ((m + 1) -' 1)) + (((m + (n + 1)) -' 2) choose (m -' 1)) by A53, A51, XREAL_1:7; hence r1 + r2 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A48, A49, A50, A46, NEWTON:22; ::_thesis: ( r1 + r2 >= 2 & ( for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) ) r1 + r2 >= 0 + 2 by A54, XREAL_1:7; hence r1 + r2 >= 2 ; ::_thesis: for X being finite set for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) let X be finite set ; ::_thesis: for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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 + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) let F be Function of (the_subsets_of_card (2,X)),(Seg 2); ::_thesis: ( card X >= r1 + r2 implies ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) assume card X >= r1 + r2 ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) then consider S being Subset of X such that A56: card S = r1 + r2 by Th10; consider s being set such that A57: s in S by A54, A56, CARD_1:27, XBOOLE_0:def_1; set B = { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ; set A = { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } ; F in Funcs ((the_subsets_of_card (2,X)),(Seg 2)) by FUNCT_2:8; then A58: ex f being Function st ( F = f & dom f = the_subsets_of_card (2,X) & rng f c= Seg 2 ) by FUNCT_2:def_2; A59: for x being set holds ( x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } iff x in S \ {s} ) proof let x be set ; ::_thesis: ( x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } iff x in S \ {s} ) hereby ::_thesis: ( x in S \ {s} implies x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ) assume A60: x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ; ::_thesis: x in S \ {s} percases ( x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } or x in { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ) by A60, XBOOLE_0:def_3; suppose x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } ; ::_thesis: x in S \ {s} then consider s9 being Element of S such that A61: x = s9 and F . {s,s9} = 1 and A62: {s,s9} in dom F ; now__::_thesis:_not_x_in_{s} assume x in {s} ; ::_thesis: contradiction then A63: x = s by TARSKI:def_1; {s,s9} = {s} \/ {s9} by ENUMSET1:1 .= {s} by A61, A63 ; then {s} in the_subsets_of_card (2,X) by A62; then ex X9 being Subset of X st ( X9 = {s} & card X9 = 2 ) ; hence contradiction by CARD_1:30; ::_thesis: verum end; hence x in S \ {s} by A54, A56, A61, CARD_1:27, XBOOLE_0:def_5; ::_thesis: verum end; suppose x in { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ; ::_thesis: x in S \ {s} then consider s9 being Element of S such that A64: x = s9 and F . {s,s9} = 2 and A65: {s,s9} in dom F ; now__::_thesis:_not_x_in_{s} assume x in {s} ; ::_thesis: contradiction then A66: x = s by TARSKI:def_1; {s,s9} = {s} \/ {s9} by ENUMSET1:1 .= {s} by A64, A66 ; then {s} in the_subsets_of_card (2,X) by A65; then ex X9 being Subset of X st ( X9 = {s} & card X9 = 2 ) ; hence contradiction by CARD_1:30; ::_thesis: verum end; hence x in S \ {s} by A54, A56, A64, CARD_1:27, XBOOLE_0:def_5; ::_thesis: verum end; end; end; assume A67: x in S \ {s} ; ::_thesis: x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } then reconsider s9 = x as Element of S by XBOOLE_0:def_5; not s9 in {s} by A67, XBOOLE_0:def_5; then s <> s9 by TARSKI:def_1; then A68: card {s,s9} = 2 by CARD_2:57; {s,s9} c= S by A57, ZFMISC_1:32; then {s,s9} is Subset of X by XBOOLE_1:1; then A69: {s,s9} in dom F by A58, A68; then A70: F . {s,s9} in rng F by FUNCT_1:3; percases ( F . {s,s9} = 1 or F . {s,s9} = 2 ) by A58, A70, FINSEQ_1:2, TARSKI:def_2; suppose F . {s,s9} = 1 ; ::_thesis: x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } then x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } by A69; hence x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } by XBOOLE_0:def_3; ::_thesis: verum end; suppose F . {s,s9} = 2 ; ::_thesis: x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } then x in { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } by A69; hence x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } by XBOOLE_0:def_3; ::_thesis: verum end; end; end; A71: now__::_thesis:_not__{__s9_where_s9_is_Element_of_S_:_(_F_._{s,s9}_=_1_&_{s,s9}_in_dom_F_)__}__/\__{__s9_where_s9_is_Element_of_S_:_(_F_._{s,s9}_=_2_&_{s,s9}_in_dom_F_)__}__<>_{} assume { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } /\ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } <> {} ; ::_thesis: contradiction then consider x being set such that A72: x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } /\ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } by XBOOLE_0:def_1; x in { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } by A72, XBOOLE_0:def_4; then A73: ex s2 being Element of S st ( x = s2 & F . {s,s2} = 2 & {s,s2} in dom F ) ; x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } by A72, XBOOLE_0:def_4; then ex s1 being Element of S st ( x = s1 & F . {s,s1} = 1 & {s,s1} in dom F ) ; hence contradiction by A73; ::_thesis: verum end; S \ {s} c= S by XBOOLE_1:36; then A74: { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } c= S by A59, TARSKI:1; {s} c= S by A57, ZFMISC_1:31; then A75: card (S \ {s}) = (card S) - (card {s}) by CARD_2:44 .= (r1 + r2) - 1 by A56, CARD_1:30 ; reconsider B = { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } as finite Subset of S by A74, XBOOLE_1:11; reconsider A = { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } as finite Subset of S by A74, XBOOLE_1:11; card (A \/ B) = ((card A) + (card B)) - (card {}) by A71, CARD_2:45 .= (card A) + (card B) ; then A76: (card A) + (card B) = (r1 + r2) - 1 by A59, A75, TARSKI:1; A77: ( card A >= r2 or card B >= r1 ) proof assume card A < r2 ; ::_thesis: card B >= r1 then A78: (card A) + 1 <= r2 by NAT_1:13; assume card B < r1 ; ::_thesis: contradiction then ((card A) + 1) + (card B) < r2 + r1 by A78, XREAL_1:8; hence contradiction by A76; ::_thesis: verum end; percases ( card A >= r2 or card B >= r1 ) by A77; supposeA79: card A >= r2 ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) set F9 = F | (the_subsets_of_card (2,A)); A c= X by XBOOLE_1:1; then (the_subsets_of_card (2,X)) /\ (the_subsets_of_card (2,A)) = the_subsets_of_card (2,A) by Lm1, XBOOLE_1:28; then A80: dom (F | (the_subsets_of_card (2,A))) = the_subsets_of_card (2,A) by A58, RELAT_1:61; rng (F | (the_subsets_of_card (2,A))) c= rng F by RELAT_1:70; then reconsider F9 = F | (the_subsets_of_card (2,A)) as Function of (the_subsets_of_card (2,A)),(Seg 2) by A58, A80, FUNCT_2:2, XBOOLE_1:1; consider S9 being Subset of A such that A81: ( ( card S9 >= m & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) ) by A52, A79; A82: F9 | (the_subsets_of_card (2,S9)) = F | (the_subsets_of_card (2,S9)) by Lm1, RELAT_1:74; A c= X by XBOOLE_1:1; then reconsider S9 = S9 as Subset of X by XBOOLE_1:1; percases ( ( card S9 >= n + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) or ( card S9 >= m & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) ) by A81; supposeA83: ( card S9 >= n + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) take S9 ; ::_thesis: ( ( card S9 >= m + 1 & rng (F | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n + 1 & rng (F | (the_subsets_of_card (2,S9))) = {2} ) ) thus ( ( card S9 >= m + 1 & rng (F | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n + 1 & rng (F | (the_subsets_of_card (2,S9))) = {2} ) ) by A83, Lm1, RELAT_1:74; ::_thesis: verum end; supposeA84: ( card S9 >= m & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) set S99 = S9 \/ {s}; {s} c= X by A57, ZFMISC_1:31; then reconsider S99 = S9 \/ {s} as Subset of X by XBOOLE_1:8; A85: the_subsets_of_card (2,S9) c= the_subsets_of_card (2,S99) by Lm1, XBOOLE_1:7; A86: rng (F | (the_subsets_of_card (2,S9))) = {1} by A84, Lm1, RELAT_1:74; A87: for y being set holds ( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 1 ) proof let y be set ; ::_thesis: ( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 1 ) F | (the_subsets_of_card (2,S9)) c= F | (the_subsets_of_card (2,S99)) by A85, RELAT_1:75; then A88: rng (F | (the_subsets_of_card (2,S9))) c= rng (F | (the_subsets_of_card (2,S99))) by RELAT_1:11; hereby ::_thesis: ( y = 1 implies y in rng (F | (the_subsets_of_card (2,S99))) ) assume y in rng (F | (the_subsets_of_card (2,S99))) ; ::_thesis: y = 1 then consider x being set such that A89: x in dom (F | (the_subsets_of_card (2,S99))) and A90: y = (F | (the_subsets_of_card (2,S99))) . x by FUNCT_1:def_3; A91: x in the_subsets_of_card (2,S99) by A89, RELAT_1:57; A92: x in dom F by A89, RELAT_1:57; x in { S999 where S999 is Subset of S99 : card S999 = 2 } by A89, RELAT_1:57; then consider S999 being Subset of S99 such that A93: x = S999 and A94: card S999 = 2 ; consider s1, s2 being set such that A95: s1 <> s2 and A96: S999 = {s1,s2} by A94, CARD_2:60; A97: s1 in S999 by A96, TARSKI:def_2; A98: s2 in S999 by A96, TARSKI:def_2; percases ( s1 in S9 or s1 in {s} ) by A97, XBOOLE_0:def_3; supposeA99: s1 in S9 ; ::_thesis: y = 1 percases ( s2 in S9 or s2 in {s} ) by A98, XBOOLE_0:def_3; suppose s2 in S9 ; ::_thesis: y = 1 then reconsider x = x as Subset of S9 by A93, A96, A99, ZFMISC_1:32; x in the_subsets_of_card (2,S9) by A93, A94; then A100: x in dom (F | (the_subsets_of_card (2,S9))) by A92, RELAT_1:57; then A101: x in dom ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) by A85, RELAT_1:74; (F | (the_subsets_of_card (2,S9))) . x = ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) . x by A85, RELAT_1:74 .= (F | (the_subsets_of_card (2,S99))) . x by A101, FUNCT_1:47 ; then y in rng (F | (the_subsets_of_card (2,S9))) by A90, A100, FUNCT_1:3; hence y = 1 by A82, A84, TARSKI:def_1; ::_thesis: verum end; supposeA102: s2 in {s} ; ::_thesis: y = 1 s1 in A by A99; then A103: ex s99 being Element of S st ( s1 = s99 & F . {s,s99} = 1 & {s,s99} in dom F ) ; x = {s1,s} by A93, A96, A102, TARSKI:def_1; hence y = 1 by A90, A91, A103, FUNCT_1:49; ::_thesis: verum end; end; end; supposeA104: s1 in {s} ; ::_thesis: y = 1 then A105: s <> s2 by A95, TARSKI:def_1; percases ( s2 in S9 or s2 in {s} ) by A98, XBOOLE_0:def_3; suppose s2 in S9 ; ::_thesis: y = 1 then s2 in A ; then ex s99 being Element of S st ( s2 = s99 & F . {s,s99} = 1 & {s,s99} in dom F ) ; then F . x = 1 by A93, A96, A104, TARSKI:def_1; hence y = 1 by A90, A91, FUNCT_1:49; ::_thesis: verum end; suppose s2 in {s} ; ::_thesis: y = 1 hence y = 1 by A105, TARSKI:def_1; ::_thesis: verum end; end; end; end; end; assume y = 1 ; ::_thesis: y in rng (F | (the_subsets_of_card (2,S99))) then y in rng (F | (the_subsets_of_card (2,S9))) by A86, TARSKI:def_1; hence y in rng (F | (the_subsets_of_card (2,S99))) by A88; ::_thesis: verum end; take S99 ; ::_thesis: ( ( card S99 >= m + 1 & rng (F | (the_subsets_of_card (2,S99))) = {1} ) or ( card S99 >= n + 1 & rng (F | (the_subsets_of_card (2,S99))) = {2} ) ) A106: not s in S9 proof assume s in S9 ; ::_thesis: contradiction then s in A ; then A107: ex s9 being Element of S st ( s = s9 & F . {s,s9} = 1 & {s,s9} in dom F ) ; {s,s} = {s} \/ {s} by ENUMSET1:1 .= {s} ; then {s} in the_subsets_of_card (2,X) by A107; then ex X9 being Subset of X st ( X9 = {s} & card X9 = 2 ) ; hence contradiction by CARD_1:30; ::_thesis: verum end; (card S9) + 1 >= m + 1 by A84, XREAL_1:6; hence ( ( card S99 >= m + 1 & rng (F | (the_subsets_of_card (2,S99))) = {1} ) or ( card S99 >= n + 1 & rng (F | (the_subsets_of_card (2,S99))) = {2} ) ) by A87, A106, CARD_2:41, TARSKI:def_1; ::_thesis: verum end; end; end; supposeA108: card B >= r1 ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) set F9 = F | (the_subsets_of_card (2,B)); B c= X by XBOOLE_1:1; then (the_subsets_of_card (2,X)) /\ (the_subsets_of_card (2,B)) = the_subsets_of_card (2,B) by Lm1, XBOOLE_1:28; then A109: dom (F | (the_subsets_of_card (2,B))) = the_subsets_of_card (2,B) by A58, RELAT_1:61; rng (F | (the_subsets_of_card (2,B))) c= rng F by RELAT_1:70; then reconsider F9 = F | (the_subsets_of_card (2,B)) as Function of (the_subsets_of_card (2,B)),(Seg 2) by A58, A109, FUNCT_2:2, XBOOLE_1:1; consider S9 being Subset of B such that A110: ( ( card S9 >= m + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) ) by A55, A108; A111: F9 | (the_subsets_of_card (2,S9)) = F | (the_subsets_of_card (2,S9)) by Lm1, RELAT_1:74; B c= X by XBOOLE_1:1; then reconsider S9 = S9 as Subset of X by XBOOLE_1:1; percases ( ( card S9 >= m + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) ) by A110; supposeA112: ( card S9 >= m + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) take S9 ; ::_thesis: ( ( card S9 >= m + 1 & rng (F | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n + 1 & rng (F | (the_subsets_of_card (2,S9))) = {2} ) ) thus ( ( card S9 >= m + 1 & rng (F | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n + 1 & rng (F | (the_subsets_of_card (2,S9))) = {2} ) ) by A112, Lm1, RELAT_1:74; ::_thesis: verum end; supposeA113: ( card S9 >= n & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) ; ::_thesis: ex S being Subset of X st ( ( card S >= m + 1 & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) set S99 = S9 \/ {s}; {s} c= X by A57, ZFMISC_1:31; then reconsider S99 = S9 \/ {s} as Subset of X by XBOOLE_1:8; A114: the_subsets_of_card (2,S9) c= the_subsets_of_card (2,S99) by Lm1, XBOOLE_1:7; A115: rng (F | (the_subsets_of_card (2,S9))) = {2} by A113, Lm1, RELAT_1:74; A116: for y being set holds ( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 2 ) proof let y be set ; ::_thesis: ( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 2 ) F | (the_subsets_of_card (2,S9)) c= F | (the_subsets_of_card (2,S99)) by A114, RELAT_1:75; then A117: rng (F | (the_subsets_of_card (2,S9))) c= rng (F | (the_subsets_of_card (2,S99))) by RELAT_1:11; hereby ::_thesis: ( y = 2 implies y in rng (F | (the_subsets_of_card (2,S99))) ) assume y in rng (F | (the_subsets_of_card (2,S99))) ; ::_thesis: y = 2 then consider x being set such that A118: x in dom (F | (the_subsets_of_card (2,S99))) and A119: y = (F | (the_subsets_of_card (2,S99))) . x by FUNCT_1:def_3; A120: x in the_subsets_of_card (2,S99) by A118, RELAT_1:57; A121: x in dom F by A118, RELAT_1:57; x in { S999 where S999 is Subset of S99 : card S999 = 2 } by A118, RELAT_1:57; then consider S999 being Subset of S99 such that A122: x = S999 and A123: card S999 = 2 ; consider s1, s2 being set such that A124: s1 <> s2 and A125: S999 = {s1,s2} by A123, CARD_2:60; A126: s1 in S999 by A125, TARSKI:def_2; A127: s2 in S999 by A125, TARSKI:def_2; percases ( s1 in S9 or s1 in {s} ) by A126, XBOOLE_0:def_3; supposeA128: s1 in S9 ; ::_thesis: y = 2 percases ( s2 in S9 or s2 in {s} ) by A127, XBOOLE_0:def_3; suppose s2 in S9 ; ::_thesis: y = 2 then reconsider x = x as Subset of S9 by A122, A125, A128, ZFMISC_1:32; x in the_subsets_of_card (2,S9) by A122, A123; then A129: x in dom (F | (the_subsets_of_card (2,S9))) by A121, RELAT_1:57; then A130: x in dom ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) by A114, RELAT_1:74; (F | (the_subsets_of_card (2,S9))) . x = ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) . x by A114, RELAT_1:74 .= (F | (the_subsets_of_card (2,S99))) . x by A130, FUNCT_1:47 ; then y in rng (F | (the_subsets_of_card (2,S9))) by A119, A129, FUNCT_1:3; hence y = 2 by A111, A113, TARSKI:def_1; ::_thesis: verum end; supposeA131: s2 in {s} ; ::_thesis: y = 2 s1 in B by A128; then A132: ex s99 being Element of S st ( s1 = s99 & F . {s,s99} = 2 & {s,s99} in dom F ) ; x = {s1,s} by A122, A125, A131, TARSKI:def_1; hence y = 2 by A119, A120, A132, FUNCT_1:49; ::_thesis: verum end; end; end; supposeA133: s1 in {s} ; ::_thesis: y = 2 then A134: s <> s2 by A124, TARSKI:def_1; percases ( s2 in S9 or s2 in {s} ) by A127, XBOOLE_0:def_3; suppose s2 in S9 ; ::_thesis: y = 2 then s2 in B ; then ex s99 being Element of S st ( s2 = s99 & F . {s,s99} = 2 & {s,s99} in dom F ) ; then F . x = 2 by A122, A125, A133, TARSKI:def_1; hence y = 2 by A119, A120, FUNCT_1:49; ::_thesis: verum end; suppose s2 in {s} ; ::_thesis: y = 2 hence y = 2 by A134, TARSKI:def_1; ::_thesis: verum end; end; end; end; end; assume y = 2 ; ::_thesis: y in rng (F | (the_subsets_of_card (2,S99))) then y in rng (F | (the_subsets_of_card (2,S9))) by A115, TARSKI:def_1; hence y in rng (F | (the_subsets_of_card (2,S99))) by A117; ::_thesis: verum end; take S99 ; ::_thesis: ( ( card S99 >= m + 1 & rng (F | (the_subsets_of_card (2,S99))) = {1} ) or ( card S99 >= n + 1 & rng (F | (the_subsets_of_card (2,S99))) = {2} ) ) A135: not s in S9 proof assume s in S9 ; ::_thesis: contradiction then s in B ; then A136: ex s9 being Element of S st ( s = s9 & F . {s,s9} = 2 & {s,s9} in dom F ) ; {s,s} = {s} \/ {s} by ENUMSET1:1 .= {s} ; then {s} in the_subsets_of_card (2,X) by A136; then ex X9 being Subset of X st ( X9 = {s} & card X9 = 2 ) ; hence contradiction by CARD_1:30; ::_thesis: verum end; (card S9) + 1 >= n + 1 by A113, XREAL_1:6; hence ( ( card S99 >= m + 1 & rng (F | (the_subsets_of_card (2,S99))) = {1} ) or ( card S99 >= n + 1 & rng (F | (the_subsets_of_card (2,S99))) = {2} ) ) by A116, A135, CARD_2:41, TARSKI:def_1; ::_thesis: verum end; end; end; end; end; end; end; A137: for n being Nat holds ( S1[ 0 ,n] & S1[n, 0 ] ) ; for m, n being Nat holds S1[m,n] from RAMSEY_1:sch_1(A137, A1); hence ( m >= 2 & n >= 2 implies ex r being Nat st ( r <= ((m + n) -' 2) choose (m -' 1) & r >= 2 & ( for X being finite set for 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} ) ) ) ) ) ; ::_thesis: verum end; theorem :: RAMSEY_1:17 for m being Nat ex r being Nat st for X being finite set for 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 Nat; ::_thesis: ex r being Nat st for X being finite set for 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 ) percases ( m < 2 or m >= 2 ) ; supposeA1: m < 2 ; ::_thesis: ex r being Nat st for X being finite set for 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 ) set r = 1; take 1 ; ::_thesis: for X being finite set for P being a_partition of the_subsets_of_card (2,X) st card X >= 1 & card P = 2 holds ex S being Subset of X st ( card S >= m & S is_homogeneous_for P ) let X be finite set ; ::_thesis: for P being a_partition of the_subsets_of_card (2,X) st card X >= 1 & card P = 2 holds ex S being Subset of X st ( card S >= m & S is_homogeneous_for P ) let P be a_partition of the_subsets_of_card (2,X); ::_thesis: ( card X >= 1 & card P = 2 implies ex S being Subset of X st ( card S >= m & S is_homogeneous_for P ) ) assume card X >= 1 ; ::_thesis: ( not card P = 2 or ex S being Subset of X st ( card S >= m & S is_homogeneous_for P ) ) then consider x being set such that A2: x in X by CARD_1:27, XBOOLE_0:def_1; reconsider S = {x} as Subset of X by A2, ZFMISC_1:31; assume card P = 2 ; ::_thesis: ex S being Subset of X st ( card S >= m & S is_homogeneous_for P ) take S ; ::_thesis: ( card S >= m & S is_homogeneous_for P ) m < 1 + 1 by A1; then m <= 1 by NAT_1:13; hence card S >= m by CARD_1:30; ::_thesis: S is_homogeneous_for P A3: card S = 1 by CARD_1:30; ex p being Element of P st the_subsets_of_card (2,S) c= p proof set p = the Element of P; take the Element of P ; ::_thesis: the_subsets_of_card (2,S) c= the Element of P the_subsets_of_card (2,S) = {} by A3, Th6; hence the_subsets_of_card (2,S) c= the Element of P by XBOOLE_1:2; ::_thesis: verum end; hence S is_homogeneous_for P by Def1; ::_thesis: verum end; suppose m >= 2 ; ::_thesis: ex r being Nat st for X being finite set for 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 ) then consider r being Nat such that r <= ((m + m) -' 2) choose (m -' 1) and A4: r >= 2 and A5: for X being finite set for 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 ; ::_thesis: for X being finite set for 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 ) let X be finite set ; ::_thesis: for 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 ) let P be a_partition of the_subsets_of_card (2,X); ::_thesis: ( card X >= r & card P = 2 implies ex S being Subset of X st ( card S >= m & S is_homogeneous_for P ) ) assume that A6: card X >= r and A7: card P = 2 ; ::_thesis: ex S being Subset of X st ( card S >= m & S is_homogeneous_for P ) 2 <= card X by A4, A6, XXREAL_0:2; then card (Seg 2) <= card X by FINSEQ_1:57; then card (Seg 2) c= card X by NAT_1:39; then card 2 c= card X by FINSEQ_1:55; then reconsider X9 = the_subsets_of_card (2,X) as non empty set by A4, A6, CARD_1:27, GROUP_10:1; reconsider P9 = P as a_partition of X9 ; card P9 = card (Seg 2) by A7, FINSEQ_1:57; then P9, Seg 2 are_equipotent by CARD_1:5; then consider F1 being Function such that A8: F1 is one-to-one and A9: dom F1 = P9 and A10: rng F1 = Seg 2 by WELLORD2:def_4; reconsider F1 = F1 as Function of P9,(Seg 2) by A9, A10, FUNCT_2:1; set F = F1 * (proj P9); reconsider F = F1 * (proj P9) as Function of (the_subsets_of_card (2,X)),(Seg 2) ; consider S being Subset of X such that A11: ( ( 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 A5, A6; take S ; ::_thesis: ( card S >= m & S is_homogeneous_for P ) thus card S >= m by A11; ::_thesis: S is_homogeneous_for P set h = the Element of the_subsets_of_card (2,S); A12: not the_subsets_of_card (2,S) is empty by A11; then A13: the Element of the_subsets_of_card (2,S) in the_subsets_of_card (2,S) ; A14: the_subsets_of_card (2,S) c= the_subsets_of_card (2,X) by Lm1; then reconsider h = the Element of the_subsets_of_card (2,S) as Element of X9 by A13; set E = EqClass (h,P9); reconsider E = EqClass (h,P9) as Element of P by EQREL_1:def_6; A15: F | (the_subsets_of_card (2,S)) is constant by A11; for x being set st x in the_subsets_of_card (2,S) holds x in E proof let x be set ; ::_thesis: ( x in the_subsets_of_card (2,S) implies x in E ) assume A16: x in the_subsets_of_card (2,S) ; ::_thesis: x in E then reconsider x9 = x as Element of the_subsets_of_card (2,X) by A14; reconsider x99 = x as Element of X9 by A14, A16; A17: dom F = the_subsets_of_card (2,X) by FUNCT_2:def_1; then h in (dom F) /\ (the_subsets_of_card (2,S)) by A12, XBOOLE_0:def_4; then A18: h in dom (F | (the_subsets_of_card (2,S))) by RELAT_1:61; x9 in (dom F) /\ (the_subsets_of_card (2,S)) by A16, A17, XBOOLE_0:def_4; then A19: x9 in dom (F | (the_subsets_of_card (2,S))) by RELAT_1:61; F . x9 = (F | (the_subsets_of_card (2,S))) . x9 by A16, FUNCT_1:49 .= (F | (the_subsets_of_card (2,S))) . h by A15, A19, A18, FUNCT_1:def_10 .= F . h by A12, FUNCT_1:49 ; then A20: F1 . ((proj P9) . x9) = (F1 * (proj P9)) . h by A17, FUNCT_1:12 .= F1 . ((proj P9) . h) by A17, FUNCT_1:12 ; (proj P9) . x99 in P9 ; then ( h in E & (proj P9) . h = (proj P9) . x9 ) by A8, A9, A20, EQREL_1:def_6, FUNCT_1:def_4; hence x in E by Th13; ::_thesis: verum end; then the_subsets_of_card (2,S) c= E by TARSKI:def_3; hence S is_homogeneous_for P by Def1; ::_thesis: verum end; end; end;