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 )
13 12 adantl 
 |-  ( ( 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*
17 6 adantr 
 |-  ( ( 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 )