Metamath Proof Explorer

Theorem ramub

Description: The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypotheses rami.c 
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
rami.m 
|- ( ph -> M e. NN0 )
rami.r 
|- ( ph -> R e. V )
rami.f 
|- ( ph -> F : R --> NN0 )
ramub.n 
|- ( ph -> N e. NN0 )
ramub.i 
|- ( ( ph /\ ( N <_ ( # ` s ) /\ f : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) )
Assertion ramub 
|- ( ph -> ( M Ramsey F ) <_ N )

Proof

Step Hyp Ref Expression
1 rami.c 
 |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 rami.m 
 |-  ( ph -> M e. NN0 )
3 rami.r 
 |-  ( ph -> R e. V )
4 rami.f 
 |-  ( ph -> F : R --> NN0 )
5 ramub.n 
 |-  ( ph -> N e. NN0 )
6 ramub.i 
 |-  ( ( ph /\ ( N <_ ( # ` s ) /\ f : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) )
7 breq1 
 |-  ( n = N -> ( n <_ ( # ` s ) <-> N <_ ( # ` s ) ) )
8 7 imbi1d 
 |-  ( n = N -> ( ( 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 <_ ( # ` 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 } ) ) ) ) )
9 8 albidv 
 |-  ( n = N -> ( 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 } ) ) ) <-> 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 } ) ) ) ) )
10 elmapi 
 |-  ( f e. ( R ^m ( s C M ) ) -> f : ( s C M ) --> R )
11 6 ancom2s 
 |-  ( ( ph /\ ( f : ( s C M ) --> R /\ N <_ ( # ` s ) ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) )
12 11 expr 
 |-  ( ( ph /\ f : ( s C M ) --> R ) -> ( N <_ ( # ` s ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
13 10 12 sylan2 
 |-  ( ( ph /\ f e. ( R ^m ( s C M ) ) ) -> ( N <_ ( # ` s ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
14 13 ralrimdva 
 |-  ( ph -> ( 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 } ) ) ) )
15 14 alrimiv 
 |-  ( ph -> 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 } ) ) ) )
16 9 5 15 elrabd 
 |-  ( ph -> N 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 } ) ) ) } )
17 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 } ) ) ) }
18 1 17 ramtub 
 |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ N 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 } ) ) ) } ) -> ( M Ramsey F ) <_ N )
19 2 3 4 16 18 syl31anc 
 |-  ( ph -> ( M Ramsey F ) <_ N )