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 ∈ ℕ 0 | ∀ s n ≤ s → φ
Assertion ramtlecl ⊢ M ∈ T → ℤ ≥ M ⊆ T

Proof

Step Hyp Ref Expression
1 ramtlecl.t ⊢ T = n ∈ ℕ 0 | ∀ s n ≤ s → φ
2 breq1 ⊢ n = M → n ≤ s ↔ M ≤ s
3 2 imbi1d ⊢ n = M → n ≤ s → φ ↔ M ≤ s → φ
4 3 albidv ⊢ n = M → ∀ s n ≤ s → φ ↔ ∀ s M ≤ s → φ
5 4 1 elrab2 ⊢ M ∈ T ↔ M ∈ ℕ 0 ∧ ∀ s M ≤ s → φ
6 5 simplbi ⊢ M ∈ T → M ∈ ℕ 0
7 eluznn0 ⊢ M ∈ ℕ 0 ∧ n ∈ ℤ ≥ M → n ∈ ℕ 0
8 7 ex ⊢ M ∈ ℕ 0 → n ∈ ℤ ≥ M → n ∈ ℕ 0
9 8 ssrdv ⊢ M ∈ ℕ 0 → ℤ ≥ M ⊆ ℕ 0
10 6 9 syl ⊢ M ∈ T → ℤ ≥ M ⊆ ℕ 0
11 5 simprbi ⊢ M ∈ T → ∀ s M ≤ s → φ
12 eluzle ⊢ n ∈ ℤ ≥ M → M ≤ n
13 12 adantl ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → M ≤ n
14 nn0ssre ⊢ ℕ 0 ⊆ ℝ
15 ressxr ⊢ ℝ ⊆ ℝ *
16 14 15 sstri ⊢ ℕ 0 ⊆ ℝ *
17 6 adantr ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → M ∈ ℕ 0
18 16 17 sselid ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → M ∈ ℝ *
19 6 7 sylan ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → n ∈ ℕ 0
20 16 19 sselid ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → n ∈ ℝ *
21 vex ⊢ s ∈ V
22 hashxrcl ⊢ s ∈ V → s ∈ ℝ *
23 21 22 mp1i ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → s ∈ ℝ *
24 xrletr ⊢ M ∈ ℝ * ∧ n ∈ ℝ * ∧ s ∈ ℝ * → M ≤ n ∧ n ≤ s → M ≤ s
25 18 20 23 24 syl3anc ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → M ≤ n ∧ n ≤ s → M ≤ s
26 13 25 mpand ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → n ≤ s → M ≤ s
27 26 imim1d ⊢ M ∈ T ∧ n ∈ ℤ ≥ M → M ≤ s → φ → n ≤ s → φ
28 27 ralrimdva ⊢ M ∈ T → M ≤ s → φ → ∀ n ∈ ℤ ≥ M n ≤ s → φ
29 28 alimdv ⊢ M ∈ T → ∀ s M ≤ s → φ → ∀ s ∀ n ∈ ℤ ≥ M n ≤ s → φ
30 11 29 mpd ⊢ M ∈ T → ∀ s ∀ n ∈ ℤ ≥ M n ≤ s → φ
31 ralcom4 ⊢ ∀ n ∈ ℤ ≥ M ∀ s n ≤ s → φ ↔ ∀ s ∀ n ∈ ℤ ≥ M n ≤ s → φ
32 30 31 sylibr ⊢ M ∈ T → ∀ n ∈ ℤ ≥ M ∀ s n ≤ s → φ
33 ssrab ⊢ ℤ ≥ M ⊆ n ∈ ℕ 0 | ∀ s n ≤ s → φ ↔ ℤ ≥ M ⊆ ℕ 0 ∧ ∀ n ∈ ℤ ≥ M ∀ s n ≤ s → φ
34 10 32 33 sylanbrc ⊢ M ∈ T → ℤ ≥ M ⊆ n ∈ ℕ 0 | ∀ s n ≤ s → φ
35 34 1 sseqtrrdi ⊢ M ∈ T → ℤ ≥ M ⊆ T