Metamath Proof Explorer

Theorem ramsey

Description: Ramsey's theorem with the definition of Ramsey ( df-ram ) eliminated. If M is an integer, R is a specified finite set of colors, and F : R --> NN0 is a set of lower bounds for each color, then there is an n such that for every set s of size greater than n and every coloring f of the set ( s C M ) of all M -element subsets of s , there is a color c and a subset x C_ s such that x is larger than F ( c ) and the M -element subsets of x are monochromatic with color c . This is the hypergraph version of Ramsey's theorem; the version for simple graphs is the case M = 2 . This is Metamath 100 proof #31. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypothesis ramsey.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
Assertion ramsey ⊢ M ∈ ℕ 0 ∧ R ∈ Fin ∧ F : R ⟶ ℕ 0 → ∃ n ∈ ℕ 0 ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c

Proof

Step Hyp Ref Expression
1 ramsey.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 ramcl ⊢ M ∈ ℕ 0 ∧ R ∈ Fin ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0
3 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
4 1 3 ramtcl2 ⊢ M ∈ ℕ 0 ∧ R ∈ Fin ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ↔ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ≠ ∅
5 2 4 mpbid ⊢ M ∈ ℕ 0 ∧ R ∈ Fin ∧ F : R ⟶ ℕ 0 → n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ≠ ∅
6 rabn0 ⊢ 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
7 5 6 sylib ⊢ M ∈ ℕ 0 ∧ R ∈ Fin ∧ F : R ⟶ ℕ 0 → ∃ n ∈ ℕ 0 ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c