# 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 } ) ) )