# Metamath Proof Explorer

## Theorem ramtcl

Description: The Ramsey number has the Ramsey number property if any number does. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses ramval.c
`|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
ramval.t
`|- T = { 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 } ) ) ) }`
Assertion ramtcl
`|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. T <-> T =/= (/) ) )`

### Proof

Step Hyp Ref Expression
1 ramval.c
` |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
2 ramval.t
` |-  T = { 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 } ) ) ) }`
3 ne0i
` |-  ( ( M Ramsey F ) e. T -> T =/= (/) )`
4 1 2 ramcl2lem
` |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = if ( T = (/) , +oo , inf ( T , RR , < ) ) )`
5 ifnefalse
` |-  ( T =/= (/) -> if ( T = (/) , +oo , inf ( T , RR , < ) ) = inf ( T , RR , < ) )`
6 4 5 sylan9eq
` |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> ( M Ramsey F ) = inf ( T , RR , < ) )`
7 2 ssrab3
` |-  T C_ NN0`
8 nn0uz
` |-  NN0 = ( ZZ>= ` 0 )`
9 7 8 sseqtri
` |-  T C_ ( ZZ>= ` 0 )`
10 9 a1i
` |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> T C_ ( ZZ>= ` 0 ) )`
11 infssuzcl
` |-  ( ( T C_ ( ZZ>= ` 0 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T )`
12 10 11 sylan
` |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T )`
13 6 12 eqeltrd
` |-  ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ T =/= (/) ) -> ( M Ramsey F ) e. T )`
14 13 ex
` |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( T =/= (/) -> ( M Ramsey F ) e. T ) )`
15 3 14 impbid2
` |-  ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. T <-> T =/= (/) ) )`