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:sCM⟶R→∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
Assertion ramub ⊢φ→MRamseyF≤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:sCM⟶R→∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
7 breq1 ⊢n=N→n≤s↔N≤s
8 7 imbi1d ⊢n=N→n≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔N≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
9 8 albidv ⊢n=N→∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔∀sN≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
10 elmapi ⊢f∈RsCM→f:sCM⟶R
11 6 ancom2s ⊢φ∧f:sCM⟶R∧N≤s→∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
12 11 expr ⊢φ∧f:sCM⟶R→N≤s→∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
13 10 12 sylan2 ⊢φ∧f∈RsCM→N≤s→∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
14 13 ralrimdva ⊢φ→N≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
15 14 alrimiv ⊢φ→∀sN≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
16 9 5 15 elrabd ⊢φ→N∈n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
17 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
18 1 17 ramtub ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0∧N∈n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c→MRamseyF≤N
19 2 3 4 16 18 syl31anc ⊢φ→MRamseyF≤N