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∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c

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→MRamseyF∈ℕ0
3 eqid ⊢n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c=n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
4 1 3 ramtcl2 ⊢M∈ℕ0∧R∈Fin∧F:R⟶ℕ0→MRamseyF∈ℕ0↔n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c≠∅
5 2 4 mpbid ⊢M∈ℕ0∧R∈Fin∧F:R⟶ℕ0→n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c≠∅
6 rabn0 ⊢n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c≠∅↔∃n∈ℕ0∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
7 5 6 sylib ⊢M∈ℕ0∧R∈Fin∧F:R⟶ℕ0→∃n∈ℕ0∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c