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 ⟼ M Ramsey y ∈ R ⟼ if y = x F ⁡ x − 1 F ⁡ y
ramub1.1 ⊢ φ → G : R ⟶ ℕ 0
ramub1.2 ⊢ φ → M − 1 Ramsey G ∈ ℕ 0
Assertion ramub1 ⊢ φ → M Ramsey F ≤ M − 1 Ramsey G + 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 ⟼ M Ramsey y ∈ R ⟼ if y = x F ⁡ x − 1 F ⁡ y
5 ramub1.1 ⊢ φ → G : R ⟶ ℕ 0
6 ramub1.2 ⊢ φ → M − 1 Ramsey G ∈ ℕ 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 − 1 Ramsey G ∈ ℕ 0 → M − 1 Ramsey G + 1 ∈ ℕ 0
13 6 12 syl ⊢ φ → M − 1 Ramsey G + 1 ∈ ℕ 0
14 simprl ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → s = M − 1 Ramsey G + 1
15 6 adantr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → M − 1 Ramsey G ∈ ℕ 0
16 nn0p1nn ⊢ M − 1 Ramsey G ∈ ℕ 0 → M − 1 Ramsey G + 1 ∈ ℕ
17 15 16 syl ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → M − 1 Ramsey G + 1 ∈ ℕ
18 14 17 eqeltrd ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → s ∈ ℕ
19 18 nnnn0d ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → s ∈ ℕ 0
20 hashclb ⊢ s ∈ V → s ∈ Fin ↔ s ∈ ℕ 0
21 20 elv ⊢ s ∈ Fin ↔ s ∈ ℕ 0
22 19 21 sylibr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → s ∈ Fin
23 hashnncl ⊢ s ∈ Fin → s ∈ ℕ ↔ s ≠ ∅
24 22 23 syl ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → s ∈ ℕ ↔ s ≠ ∅
25 18 24 mpbid ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → s ≠ ∅
26 n0 ⊢ s ≠ ∅ ↔ ∃ w w ∈ s
27 25 26 sylib ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → ∃ w w ∈ s
28 1 adantr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → M ∈ ℕ
29 2 adantr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → R ∈ Fin
30 3 adantr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → F : R ⟶ ℕ
31 5 adantr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → G : R ⟶ ℕ 0
32 6 adantr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → M − 1 Ramsey G ∈ ℕ 0
33 22 adantrr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → s ∈ Fin
34 simprll ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → s = M − 1 Ramsey G + 1
35 simprlr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R
36 simprr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ 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 ∖ w a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M − 1 ⟼ f ⁡ v ∪ w = u ∈ s ∖ w a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M − 1 ⟼ f ⁡ u ∪ w
40 28 29 30 4 31 32 7 33 34 35 36 39 ramub1lem2 ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R ∧ w ∈ s → ∃ c ∈ R ∃ z ∈ 𝒫 s F ⁡ c ≤ z ∧ z a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
41 40 expr ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → w ∈ s → ∃ c ∈ R ∃ z ∈ 𝒫 s F ⁡ c ≤ z ∧ z a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
42 41 exlimdv ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → ∃ w w ∈ s → ∃ c ∈ R ∃ z ∈ 𝒫 s F ⁡ c ≤ z ∧ z a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
43 27 42 mpd ⊢ φ ∧ s = M − 1 Ramsey G + 1 ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → ∃ c ∈ R ∃ z ∈ 𝒫 s F ⁡ c ≤ z ∧ z a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
44 7 8 2 11 13 43 ramub2 ⊢ φ → M Ramsey F ≤ M − 1 Ramsey G + 1