Metamath Proof Explorer

Theorem ramub1

Description: Inductive step for Ramsey's theorem, in the form of an explicit upper bound. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m ⊢φ→M∈ℕ
ramub1.r ⊢φ→R∈Fin
ramub1.f ⊢φ→F:R⟶ℕ
ramub1.g ⊢G=x∈R⟼MRamseyy∈R⟼ify=xF⁡x−1F⁡y
ramub1.1 ⊢φ→G:R⟶ℕ0
ramub1.2 ⊢φ→M−1RamseyG∈ℕ0
Assertion ramub1 ⊢φ→MRamseyF≤M−1RamseyG+1

Proof

Step Hyp Ref Expression
1 ramub1.m ⊢φ→M∈ℕ
2 ramub1.r ⊢φ→R∈Fin
3 ramub1.f ⊢φ→F:R⟶ℕ
4 ramub1.g ⊢G=x∈R⟼MRamseyy∈R⟼ify=xF⁡x−1F⁡y
5 ramub1.1 ⊢φ→G:R⟶ℕ0
6 ramub1.2 ⊢φ→M−1RamseyG∈ℕ0
7 eqid ⊢a∈V,i∈ℕ0⟼b∈𝒫a|b=i=a∈V,i∈ℕ0⟼b∈𝒫a|b=i
8 1 nnnn0d ⊢φ→M∈ℕ0
9 nnssnn0 ⊢ℕ⊆ℕ0
10 fss ⊢F:R⟶ℕ∧ℕ⊆ℕ0→F:R⟶ℕ0
11 3 9 10 sylancl ⊢φ→F:R⟶ℕ0
12 peano2nn0 ⊢M−1RamseyG∈ℕ0→M−1RamseyG+1∈ℕ0
13 6 12 syl ⊢φ→M−1RamseyG+1∈ℕ0
14 simprl ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→s=M−1RamseyG+1
15 6 adantr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→M−1RamseyG∈ℕ0
16 nn0p1nn ⊢M−1RamseyG∈ℕ0→M−1RamseyG+1∈ℕ
17 15 16 syl ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→M−1RamseyG+1∈ℕ
18 14 17 eqeltrd ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→s∈ℕ
19 18 nnnn0d ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→s∈ℕ0
20 hashclb ⊢s∈V→s∈Fin↔s∈ℕ0
21 20 elv ⊢s∈Fin↔s∈ℕ0
22 19 21 sylibr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→s∈Fin
23 hashnncl ⊢s∈Fin→s∈ℕ↔s≠∅
24 22 23 syl ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→s∈ℕ↔s≠∅
25 18 24 mpbid ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→s≠∅
26 n0 ⊢s≠∅↔∃ww∈s
27 25 26 sylib ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→∃ww∈s
28 1 adantr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→M∈ℕ
29 2 adantr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→R∈Fin
30 3 adantr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→F:R⟶ℕ
31 5 adantr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→G:R⟶ℕ0
32 6 adantr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→M−1RamseyG∈ℕ0
33 22 adantrr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→s∈Fin
34 simprll ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→s=M−1RamseyG+1
35 simprlr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R
36 simprr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→w∈s
37 uneq1 ⊢v=u→v∪w=u∪w
38 37 fveq2d ⊢v=u→f⁡v∪w=f⁡u∪w
39 38 cbvmptv ⊢v∈s∖wa∈V,i∈ℕ0⟼b∈𝒫a|b=iM−1⟼f⁡v∪w=u∈s∖wa∈V,i∈ℕ0⟼b∈𝒫a|b=iM−1⟼f⁡u∪w
40 28 29 30 4 31 32 7 33 34 35 36 39 ramub1lem2 ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R∧w∈s→∃c∈R∃z∈𝒫sF⁡c≤z∧za∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
41 40 expr ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→w∈s→∃c∈R∃z∈𝒫sF⁡c≤z∧za∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
42 41 exlimdv ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→∃ww∈s→∃c∈R∃z∈𝒫sF⁡c≤z∧za∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
43 27 42 mpd ⊢φ∧s=M−1RamseyG+1∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶R→∃c∈R∃z∈𝒫sF⁡c≤z∧za∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
44 7 8 2 11 13 43 ramub2 ⊢φ→MRamseyF≤M−1RamseyG+1