Metamath Proof Explorer

Theorem ramub

Description: The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypotheses rami.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
rami.m ⊢ φ → M ∈ ℕ 0
rami.r ⊢ φ → R ∈ V
rami.f ⊢ φ → F : R ⟶ ℕ 0
ramub.n ⊢ φ → N ∈ ℕ 0
ramub.i ⊢ φ ∧ N ≤ s ∧ f : s C M ⟶ R → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
Assertion ramub ⊢ φ → M Ramsey F ≤ N

Proof

Step Hyp Ref Expression
1 rami.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 rami.m ⊢ φ → M ∈ ℕ 0
3 rami.r ⊢ φ → R ∈ V
4 rami.f ⊢ φ → F : R ⟶ ℕ 0
5 ramub.n ⊢ φ → N ∈ ℕ 0
6 ramub.i ⊢ φ ∧ N ≤ s ∧ f : s C M ⟶ R → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
7 breq1 ⊢ n = N → n ≤ s ↔ N ≤ s
8 7 imbi1d ⊢ n = N → n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ N ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
9 8 albidv ⊢ n = N → ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ ∀ s N ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
10 elmapi ⊢ f ∈ R s C M → f : s C M ⟶ R
11 6 ancom2s ⊢ φ ∧ f : s C M ⟶ R ∧ N ≤ s → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
12 11 expr ⊢ φ ∧ f : s C M ⟶ R → N ≤ s → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
13 10 12 sylan2 ⊢ φ ∧ f ∈ R s C M → N ≤ s → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
14 13 ralrimdva ⊢ φ → N ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
15 14 alrimiv ⊢ φ → ∀ s N ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
16 9 5 15 elrabd ⊢ φ → N ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
17 eqid ⊢ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c = n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
18 1 17 ramtub ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ N ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c → M Ramsey F ≤ N
19 2 3 4 16 18 syl31anc ⊢ φ → M Ramsey F ≤ N