:: 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;