Metamath Proof Explorer

Theorem rami

Description: The defining property of a Ramsey number. (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
rami.x ⊢φ→MRamseyF∈ℕ0
rami.s ⊢φ→S∈W
rami.l ⊢φ→MRamseyF≤S
rami.g ⊢φ→G:SCM⟶R
Assertion rami ⊢φ→∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆G-1c

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 rami.x ⊢φ→MRamseyF∈ℕ0
6 rami.s ⊢φ→S∈W
7 rami.l ⊢φ→MRamseyF≤S
8 rami.g ⊢φ→G:SCM⟶R
9 cnveq ⊢f=G→f-1=G-1
10 9 imaeq1d ⊢f=G→f-1c=G-1c
11 10 sseq2d ⊢f=G→xCM⊆f-1c↔xCM⊆G-1c
12 11 anbi2d ⊢f=G→F⁡c≤x∧xCM⊆f-1c↔F⁡c≤x∧xCM⊆G-1c
13 12 2rexbidv ⊢f=G→∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆f-1c↔∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆G-1c
14 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
15 1 14 ramtcl2 ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0→MRamseyF∈ℕ0↔n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c≠∅
16 1 14 ramtcl ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0→MRamseyF∈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≠∅
17 15 16 bitr4d ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0→MRamseyF∈ℕ0↔MRamseyF∈n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
18 2 3 4 17 syl3anc ⊢φ→MRamseyF∈ℕ0↔MRamseyF∈n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
19 5 18 mpbid ⊢φ→MRamseyF∈n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
20 breq1 ⊢n=MRamseyF→n≤s↔MRamseyF≤s
21 20 imbi1d ⊢n=MRamseyF→n≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔MRamseyF≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
22 21 albidv ⊢n=MRamseyF→∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔∀sMRamseyF≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
23 22 elrab ⊢MRamseyF∈n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔MRamseyF∈ℕ0∧∀sMRamseyF≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
24 23 simprbi ⊢MRamseyF∈n∈ℕ0|∀sn≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c→∀sMRamseyF≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
25 19 24 syl ⊢φ→∀sMRamseyF≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c
26 fveq2 ⊢s=S→s=S
27 26 breq2d ⊢s=S→MRamseyF≤s↔MRamseyF≤S
28 oveq1 ⊢s=S→sCM=SCM
29 28 oveq2d ⊢s=S→RsCM=RSCM
30 pweq ⊢s=S→𝒫s=𝒫S
31 30 rexeqdv ⊢s=S→∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔∃x∈𝒫SF⁡c≤x∧xCM⊆f-1c
32 31 rexbidv ⊢s=S→∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆f-1c
33 29 32 raleqbidv ⊢s=S→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔∀f∈RSCM∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆f-1c
34 27 33 imbi12d ⊢s=S→MRamseyF≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c↔MRamseyF≤S→∀f∈RSCM∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆f-1c
35 34 spcgv ⊢S∈W→∀sMRamseyF≤s→∀f∈RsCM∃c∈R∃x∈𝒫sF⁡c≤x∧xCM⊆f-1c→MRamseyF≤S→∀f∈RSCM∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆f-1c
36 6 25 7 35 syl3c ⊢φ→∀f∈RSCM∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆f-1c
37 ovex ⊢SCM∈V
38 elmapg ⊢R∈V∧SCM∈V→G∈RSCM↔G:SCM⟶R
39 3 37 38 sylancl ⊢φ→G∈RSCM↔G:SCM⟶R
40 8 39 mpbird ⊢φ→G∈RSCM
41 13 36 40 rspcdva ⊢φ→∃c∈R∃x∈𝒫SF⁡c≤x∧xCM⊆G-1c