Metamath Proof Explorer

Theorem ramtub

Description: The Ramsey number is a lower bound on the set of all numbers 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 ramtub ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ A ∈ T → M Ramsey F ≤ A

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 = ∅ +∞ inf T ℝ <
4 n0i ⊢ A ∈ T → ¬ T = ∅
5 4 iffalsed ⊢ A ∈ T → if T = ∅ +∞ inf T ℝ < = inf T ℝ <
6 3 5 sylan9eq ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ A ∈ T → M Ramsey F = inf T ℝ <
7 2 ssrab3 ⊢ T ⊆ ℕ 0
8 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
9 7 8 sseqtri ⊢ T ⊆ ℤ ≥ 0
10 9 a1i ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → T ⊆ ℤ ≥ 0
11 infssuzle ⊢ T ⊆ ℤ ≥ 0 ∧ A ∈ T → inf T ℝ < ≤ A
12 10 11 sylan ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ A ∈ T → inf T ℝ < ≤ A
13 6 12 eqbrtrd ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ A ∈ T → M Ramsey F ≤ A