Metamath Proof Explorer

Theorem ramcl2

Description: The Ramsey number is either a nonnegative integer or plus infinity. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Assertion ramcl2 ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ∪ +∞

Proof

Step Hyp Ref Expression
1 eqid ⊢ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 eqid ⊢ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c = n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
3 1 2 ramcl2lem ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F = if n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c = ∅ +∞ sup n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c ℝ <
4 iftrue ⊢ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c = ∅ → if n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c = ∅ +∞ sup n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c ℝ < = +∞
5 3 4 sylan9eq ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c = ∅ → M Ramsey F = +∞
6 ssun2 ⊢ +∞ ⊆ ℕ 0 ∪ +∞
7 pnfex ⊢ +∞ ∈ V
8 7 snss ⊢ +∞ ∈ ℕ 0 ∪ +∞ ↔ +∞ ⊆ ℕ 0 ∪ +∞
9 6 8 mpbir ⊢ +∞ ∈ ℕ 0 ∪ +∞
10 5 9 eqeltrdi ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c = ∅ → M Ramsey F ∈ ℕ 0 ∪ +∞
11 ssun1 ⊢ ℕ 0 ⊆ ℕ 0 ∪ +∞
12 1 2 ramtcl2 ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ↔ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c ≠ ∅
13 12 biimpar ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c ≠ ∅ → M Ramsey F ∈ ℕ 0
14 11 13 sseldi ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c ≠ ∅ → M Ramsey F ∈ ℕ 0 ∪ +∞
15 10 14 pm2.61dane ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ∪ +∞