Metamath Proof Explorer

Theorem rami

Description: The defining property of a Ramsey number. (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 )
rami.x 
|- ( ph -> ( M Ramsey F ) e. NN0 )
rami.s 
|- ( ph -> S e. W )
rami.l 
|- ( ph -> ( M Ramsey F ) <_ ( # ` S ) )
rami.g 
|- ( ph -> G : ( S C M ) --> R )
Assertion rami 
|- ( ph -> E. c e. R E. x e. ~P S ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) )

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 rami.x 
 |-  ( ph -> ( M Ramsey F ) e. NN0 )
6 rami.s 
 |-  ( ph -> S e. W )
7 rami.l 
 |-  ( ph -> ( M Ramsey F ) <_ ( # ` S ) )
8 rami.g 
 |-  ( ph -> G : ( S C M ) --> R )
9 cnveq 
 |-  ( f = G -> `' f = `' G )
10 9 imaeq1d 
 |-  ( f = G -> ( `' f " { c } ) = ( `' G " { c } ) )
11 10 sseq2d 
 |-  ( f = G -> ( ( x C M ) C_ ( `' f " { c } ) <-> ( x C M ) C_ ( `' G " { c } ) ) )
12 11 anbi2d 
 |-  ( f = G -> ( ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) <-> ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) ) )
13 12 2rexbidv 
 |-  ( f = G -> ( E. c e. R E. x e. ~P S ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) <-> E. c e. R E. x e. ~P S ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) ) )
14 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 } ) ) ) }
15 1 14 ramtcl2 
 |-  ( ( M e. NN0 /\ R e. V /\ 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 } ) ) ) } =/= (/) ) )
16 1 14 ramtcl 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) 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 } ) ) ) } <-> { 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 15 16 bitr4d 
 |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> ( M Ramsey F ) 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 } ) ) ) } ) )
18 2 3 4 17 syl3anc 
 |-  ( ph -> ( ( M Ramsey F ) e. NN0 <-> ( M Ramsey F ) 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 } ) ) ) } ) )
19 5 18 mpbid 
 |-  ( ph -> ( M Ramsey F ) 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 } ) ) ) } )
20 breq1 
 |-  ( n = ( M Ramsey F ) -> ( n <_ ( # ` s ) <-> ( M Ramsey F ) <_ ( # ` s ) ) )
21 20 imbi1d 
 |-  ( n = ( M Ramsey F ) -> ( ( 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 ) <_ ( # ` 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 } ) ) ) ) )
22 21 albidv 
 |-  ( n = ( M Ramsey F ) -> ( 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 ( ( M Ramsey F ) <_ ( # ` 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 } ) ) ) ) )
23 22 elrab 
 |-  ( ( M Ramsey F ) 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 ) e. NN0 /\ A. s ( ( M Ramsey F ) <_ ( # ` 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 } ) ) ) ) )
24 23 simprbi 
 |-  ( ( M Ramsey F ) 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 } ) ) ) } -> A. s ( ( M Ramsey F ) <_ ( # ` 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 } ) ) ) )
25 19 24 syl 
 |-  ( ph -> A. s ( ( M Ramsey F ) <_ ( # ` 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 } ) ) ) )
26 fveq2 
 |-  ( s = S -> ( # ` s ) = ( # ` S ) )
27 26 breq2d 
 |-  ( s = S -> ( ( M Ramsey F ) <_ ( # ` s ) <-> ( M Ramsey F ) <_ ( # ` S ) ) )
28 oveq1 
 |-  ( s = S -> ( s C M ) = ( S C M ) )
29 28 oveq2d 
 |-  ( s = S -> ( R ^m ( s C M ) ) = ( R ^m ( S C M ) ) )
30 pweq 
 |-  ( s = S -> ~P s = ~P S )
31 30 rexeqdv 
 |-  ( s = S -> ( E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) <-> E. x e. ~P S ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
32 31 rexbidv 
 |-  ( s = S -> ( E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) <-> E. c e. R E. x e. ~P S ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
33 29 32 raleqbidv 
 |-  ( s = 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. 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 } ) ) ) )
34 27 33 imbi12d 
 |-  ( s = S -> ( ( ( M Ramsey F ) <_ ( # ` 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 ) <_ ( # ` 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 } ) ) ) ) )
35 34 spcgv 
 |-  ( S e. W -> ( A. s ( ( M Ramsey F ) <_ ( # ` 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 ) <_ ( # ` 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 } ) ) ) ) )
36 6 25 7 35 syl3c 
 |-  ( ph -> 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 } ) ) )
37 ovex 
 |-  ( S C M ) e. _V
38 elmapg 
 |-  ( ( R e. V /\ ( S C M ) e. _V ) -> ( G e. ( R ^m ( S C M ) ) <-> G : ( S C M ) --> R ) )
39 3 37 38 sylancl 
 |-  ( ph -> ( G e. ( R ^m ( S C M ) ) <-> G : ( S C M ) --> R ) )
40 8 39 mpbird 
 |-  ( ph -> G e. ( R ^m ( S C M ) ) )
41 13 36 40 rspcdva 
 |-  ( ph -> E. c e. R E. x e. ~P S ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) )