# Metamath Proof Explorer

## Theorem ramtlecl

Description: The set T of numbers with the Ramsey number property is upward-closed. (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Hypothesis ramtlecl.t
`|- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> ph ) }`
Assertion ramtlecl
`|- ( M e. T -> ( ZZ>= ` M ) C_ T )`

### Proof

Step Hyp Ref Expression
1 ramtlecl.t
` |-  T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> ph ) }`
2 breq1
` |-  ( n = M -> ( n <_ ( # ` s ) <-> M <_ ( # ` s ) ) )`
3 2 imbi1d
` |-  ( n = M -> ( ( n <_ ( # ` s ) -> ph ) <-> ( M <_ ( # ` s ) -> ph ) ) )`
4 3 albidv
` |-  ( n = M -> ( A. s ( n <_ ( # ` s ) -> ph ) <-> A. s ( M <_ ( # ` s ) -> ph ) ) )`
5 4 1 elrab2
` |-  ( M e. T <-> ( M e. NN0 /\ A. s ( M <_ ( # ` s ) -> ph ) ) )`
6 5 simplbi
` |-  ( M e. T -> M e. NN0 )`
7 eluznn0
` |-  ( ( M e. NN0 /\ n e. ( ZZ>= ` M ) ) -> n e. NN0 )`
8 7 ex
` |-  ( M e. NN0 -> ( n e. ( ZZ>= ` M ) -> n e. NN0 ) )`
9 8 ssrdv
` |-  ( M e. NN0 -> ( ZZ>= ` M ) C_ NN0 )`
10 6 9 syl
` |-  ( M e. T -> ( ZZ>= ` M ) C_ NN0 )`
11 5 simprbi
` |-  ( M e. T -> A. s ( M <_ ( # ` s ) -> ph ) )`
12 eluzle
` |-  ( n e. ( ZZ>= ` M ) -> M <_ n )`
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> M <_ n )`
14 nn0ssre
` |-  NN0 C_ RR`
15 ressxr
` |-  RR C_ RR*`
16 14 15 sstri
` |-  NN0 C_ RR*`
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> M e. NN0 )`
18 16 17 sseldi
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> M e. RR* )`
19 6 7 sylan
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> n e. NN0 )`
20 16 19 sseldi
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> n e. RR* )`
21 vex
` |-  s e. _V`
22 hashxrcl
` |-  ( s e. _V -> ( # ` s ) e. RR* )`
23 21 22 mp1i
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> ( # ` s ) e. RR* )`
24 xrletr
` |-  ( ( M e. RR* /\ n e. RR* /\ ( # ` s ) e. RR* ) -> ( ( M <_ n /\ n <_ ( # ` s ) ) -> M <_ ( # ` s ) ) )`
25 18 20 23 24 syl3anc
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> ( ( M <_ n /\ n <_ ( # ` s ) ) -> M <_ ( # ` s ) ) )`
26 13 25 mpand
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> ( n <_ ( # ` s ) -> M <_ ( # ` s ) ) )`
27 26 imim1d
` |-  ( ( M e. T /\ n e. ( ZZ>= ` M ) ) -> ( ( M <_ ( # ` s ) -> ph ) -> ( n <_ ( # ` s ) -> ph ) ) )`
28 27 ralrimdva
` |-  ( M e. T -> ( ( M <_ ( # ` s ) -> ph ) -> A. n e. ( ZZ>= ` M ) ( n <_ ( # ` s ) -> ph ) ) )`
29 28 alimdv
` |-  ( M e. T -> ( A. s ( M <_ ( # ` s ) -> ph ) -> A. s A. n e. ( ZZ>= ` M ) ( n <_ ( # ` s ) -> ph ) ) )`
30 11 29 mpd
` |-  ( M e. T -> A. s A. n e. ( ZZ>= ` M ) ( n <_ ( # ` s ) -> ph ) )`
31 ralcom4
` |-  ( A. n e. ( ZZ>= ` M ) A. s ( n <_ ( # ` s ) -> ph ) <-> A. s A. n e. ( ZZ>= ` M ) ( n <_ ( # ` s ) -> ph ) )`
32 30 31 sylibr
` |-  ( M e. T -> A. n e. ( ZZ>= ` M ) A. s ( n <_ ( # ` s ) -> ph ) )`
33 ssrab
` |-  ( ( ZZ>= ` M ) C_ { n e. NN0 | A. s ( n <_ ( # ` s ) -> ph ) } <-> ( ( ZZ>= ` M ) C_ NN0 /\ A. n e. ( ZZ>= ` M ) A. s ( n <_ ( # ` s ) -> ph ) ) )`
34 10 32 33 sylanbrc
` |-  ( M e. T -> ( ZZ>= ` M ) C_ { n e. NN0 | A. s ( n <_ ( # ` s ) -> ph ) } )`
35 34 1 sseqtrrdi
` |-  ( M e. T -> ( ZZ>= ` M ) C_ T )`