Metamath Proof Explorer

Theorem ramtcl2

Description: The Ramsey number is an integer iff there is a number with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses ramval.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
ramval.t ⊢ T = n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
Assertion ramtcl2 ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ↔ T ≠ ∅

Proof

Step Hyp Ref Expression
1 ramval.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 ramval.t ⊢ T = n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
3 1 2 ramcl2lem ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F = if T = ∅ +∞ sup T ℝ <
4 3 eleq1d ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ↔ if T = ∅ +∞ sup T ℝ < ∈ ℕ 0
5 pnfnre ⊢ +∞ ∉ ℝ
6 5 neli ⊢ ¬ +∞ ∈ ℝ
7 iftrue ⊢ T = ∅ → if T = ∅ +∞ sup T ℝ < = +∞
8 7 eleq1d ⊢ T = ∅ → if T = ∅ +∞ sup T ℝ < ∈ ℕ 0 ↔ +∞ ∈ ℕ 0
9 nn0re ⊢ +∞ ∈ ℕ 0 → +∞ ∈ ℝ
10 8 9 syl6bi ⊢ T = ∅ → if T = ∅ +∞ sup T ℝ < ∈ ℕ 0 → +∞ ∈ ℝ
11 6 10 mtoi ⊢ T = ∅ → ¬ if T = ∅ +∞ sup T ℝ < ∈ ℕ 0
12 11 necon2ai ⊢ if T = ∅ +∞ sup T ℝ < ∈ ℕ 0 → T ≠ ∅
13 4 12 syl6bi ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 → T ≠ ∅
14 1 2 ramtcl ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ T ↔ T ≠ ∅
15 2 ssrab3 ⊢ T ⊆ ℕ 0
16 15 sseli ⊢ M Ramsey F ∈ T → M Ramsey F ∈ ℕ 0
17 14 16 syl6bir ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → T ≠ ∅ → M Ramsey F ∈ ℕ 0
18 13 17 impbid ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ↔ T ≠ ∅