Metamath Proof Explorer

Theorem ramsey

Description: Ramsey's theorem with the definition of Ramsey ( df-ram ) eliminated. If M is an integer, R is a specified finite set of colors, and F : R --> NN0 is a set of lower bounds for each color, then there is an n such that for every set s of size greater than n and every coloring f of the set ( s C M ) of all M -element subsets of s , there is a color c and a subset x C_ s such that x is larger than F ( c ) and the M -element subsets of x are monochromatic with color c . This is the hypergraph version of Ramsey's theorem; the version for simple graphs is the case M = 2 . This is Metamath 100 proof #31. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypothesis ramsey.c 
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
Assertion ramsey 
|- ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> E. n e. NN0 A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )

Proof

Step Hyp Ref Expression
1 ramsey.c 
 |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 ramcl 
 |-  ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> ( M Ramsey F ) e. NN0 )
3 eqid 
 |-  { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) } = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }
4 1 3 ramtcl2 
 |-  ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) } =/= (/) ) )
5 2 4 mpbid 
 |-  ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) } =/= (/) )
6 rabn0 
 |-  ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) } =/= (/) <-> E. n e. NN0 A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
7 5 6 sylib 
 |-  ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> E. n e. NN0 A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )