Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ramcl Structured version   Visualization version   GIF version

Theorem ramcl 15571
 Description: Ramsey's theorem: the Ramsey number is an integer for every finite coloring and set of upper bounds. (Contributed by Mario Carneiro, 23-Apr-2015.)
Assertion
Ref Expression
ramcl ((𝑀 ∈ ℕ0𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈ ℕ0)

Proof of Theorem ramcl
Dummy variables 𝑓 𝑥 𝑔 𝑘 𝑚 𝑛 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0ex 11175 . . . 4 0 ∈ V
2 simpr 476 . . . 4 ((𝑀 ∈ ℕ0𝑅 ∈ Fin) → 𝑅 ∈ Fin)
3 elmapg 7757 . . . 4 ((ℕ0 ∈ V ∧ 𝑅 ∈ Fin) → (𝐹 ∈ (ℕ0𝑚 𝑅) ↔ 𝐹:𝑅⟶ℕ0))
41, 2, 3sylancr 694 . . 3 ((𝑀 ∈ ℕ0𝑅 ∈ Fin) → (𝐹 ∈ (ℕ0𝑚 𝑅) ↔ 𝐹:𝑅⟶ℕ0))
5 oveq1 6556 . . . . . . . . 9 (𝑥 = 0 → (𝑥 Ramsey 𝑓) = (0 Ramsey 𝑓))
65eleq1d 2672 . . . . . . . 8 (𝑥 = 0 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (0 Ramsey 𝑓) ∈ ℕ0))
76ralbidv 2969 . . . . . . 7 (𝑥 = 0 → (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ ∀𝑓 ∈ (ℕ0𝑚 𝑅)(0 Ramsey 𝑓) ∈ ℕ0))
87imbi2d 329 . . . . . 6 (𝑥 = 0 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(0 Ramsey 𝑓) ∈ ℕ0)))
9 oveq1 6556 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 Ramsey 𝑓) = (𝑚 Ramsey 𝑓))
109eleq1d 2672 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑚 Ramsey 𝑓) ∈ ℕ0))
1110ralbidv 2969 . . . . . . 7 (𝑥 = 𝑚 → (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0))
1211imbi2d 329 . . . . . 6 (𝑥 = 𝑚 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0)))
13 oveq1 6556 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → (𝑥 Ramsey 𝑓) = ((𝑚 + 1) Ramsey 𝑓))
1413eleq1d 2672 . . . . . . . 8 (𝑥 = (𝑚 + 1) → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
1514ralbidv 2969 . . . . . . 7 (𝑥 = (𝑚 + 1) → (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ ∀𝑓 ∈ (ℕ0𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
1615imbi2d 329 . . . . . 6 (𝑥 = (𝑚 + 1) → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)))
17 oveq1 6556 . . . . . . . . 9 (𝑥 = 𝑀 → (𝑥 Ramsey 𝑓) = (𝑀 Ramsey 𝑓))
1817eleq1d 2672 . . . . . . . 8 (𝑥 = 𝑀 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑀 Ramsey 𝑓) ∈ ℕ0))
1918ralbidv 2969 . . . . . . 7 (𝑥 = 𝑀 → (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈ ℕ0))
2019imbi2d 329 . . . . . 6 (𝑥 = 𝑀 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈ ℕ0)))
21 elmapi 7765 . . . . . . . 8 (𝑓 ∈ (ℕ0𝑚 𝑅) → 𝑓:𝑅⟶ℕ0)
22 0ramcl 15565 . . . . . . . 8 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ0) → (0 Ramsey 𝑓) ∈ ℕ0)
2321, 22sylan2 490 . . . . . . 7 ((𝑅 ∈ Fin ∧ 𝑓 ∈ (ℕ0𝑚 𝑅)) → (0 Ramsey 𝑓) ∈ ℕ0)
2423ralrimiva 2949 . . . . . 6 (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(0 Ramsey 𝑓) ∈ ℕ0)
25 oveq2 6557 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑚 Ramsey 𝑓) = (𝑚 Ramsey 𝑔))
2625eleq1d 2672 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑚 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑚 Ramsey 𝑔) ∈ ℕ0))
2726cbvralv 3147 . . . . . . . . 9 (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 ↔ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)
28 simpll 786 . . . . . . . . . . . . . 14 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (𝑓 ∈ (ℕ0𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → 𝑅 ∈ Fin)
2921ad2antrl 760 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (𝑓 ∈ (ℕ0𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → 𝑓:𝑅⟶ℕ0)
3029ffvelrnda 6267 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (𝑓 ∈ (ℕ0𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) ∧ 𝑘𝑅) → (𝑓𝑘) ∈ ℕ0)
3128, 30fsumnn0cl 14314 . . . . . . . . . . . . 13 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (𝑓 ∈ (ℕ0𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → Σ𝑘𝑅 (𝑓𝑘) ∈ ℕ0)
32 eqeq2 2621 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (Σ𝑘𝑅 (𝑘) = 𝑥 ↔ Σ𝑘𝑅 (𝑘) = 0))
3332anbi2d 736 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) ↔ (:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 0)))
3433imbi1d 330 . . . . . . . . . . . . . . . . . 18 (𝑥 = 0 → (((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 0) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
3534albidv 1836 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 0) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
3635imbi2d 329 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 0) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))))
37 eqeq2 2621 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑛 → (Σ𝑘𝑅 (𝑘) = 𝑥 ↔ Σ𝑘𝑅 (𝑘) = 𝑛))
3837anbi2d 736 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑛 → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) ↔ (:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛)))
3938imbi1d 330 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑛 → (((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
4039albidv 1836 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑛 → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
4140imbi2d 329 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑛 → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))))
42 eqeq2 2621 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑛 + 1) → (Σ𝑘𝑅 (𝑘) = 𝑥 ↔ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)))
4342anbi2d 736 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑛 + 1) → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) ↔ (:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1))))
4443imbi1d 330 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑛 + 1) → (((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
4544albidv 1836 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑛 + 1) → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
4645imbi2d 329 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑛 + 1) → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))))
47 eqeq2 2621 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = Σ𝑘𝑅 (𝑓𝑘) → (Σ𝑘𝑅 (𝑘) = 𝑥 ↔ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)))
4847anbi2d 736 . . . . . . . . . . . . . . . . . . 19 (𝑥 = Σ𝑘𝑅 (𝑓𝑘) → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) ↔ (:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘))))
4948imbi1d 330 . . . . . . . . . . . . . . . . . 18 (𝑥 = Σ𝑘𝑅 (𝑓𝑘) → (((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
5049albidv 1836 . . . . . . . . . . . . . . . . 17 (𝑥 = Σ𝑘𝑅 (𝑓𝑘) → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
5150imbi2d 329 . . . . . . . . . . . . . . . 16 (𝑥 = Σ𝑘𝑅 (𝑓𝑘) → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))))
52 simplll 794 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → 𝑅 ∈ Fin)
53 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . 24 ((:𝑅⟶ℕ0𝑘𝑅) → (𝑘) ∈ ℕ0)
5453adantll 746 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑘𝑅) → (𝑘) ∈ ℕ0)
5554nn0red 11229 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑘𝑅) → (𝑘) ∈ ℝ)
5654nn0ge0d 11231 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑘𝑅) → 0 ≤ (𝑘))
5752, 55, 56fsum00 14371 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → (Σ𝑘𝑅 (𝑘) = 0 ↔ ∀𝑘𝑅 (𝑘) = 0))
58 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘) ∈ V
5958rgenw 2908 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑅 (𝑘) ∈ V
60 mpteqb 6207 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑘𝑅 (𝑘) ∈ V → ((𝑘𝑅 ↦ (𝑘)) = (𝑘𝑅 ↦ 0) ↔ ∀𝑘𝑅 (𝑘) = 0))
6159, 60ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑅 ↦ (𝑘)) = (𝑘𝑅 ↦ 0) ↔ ∀𝑘𝑅 (𝑘) = 0)
6257, 61syl6bbr 277 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → (Σ𝑘𝑅 (𝑘) = 0 ↔ (𝑘𝑅 ↦ (𝑘)) = (𝑘𝑅 ↦ 0)))
63 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → :𝑅⟶ℕ0)
6463feqmptd 6159 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → = (𝑘𝑅 ↦ (𝑘)))
65 fconstmpt 5085 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 × {0}) = (𝑘𝑅 ↦ 0)
6665a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → (𝑅 × {0}) = (𝑘𝑅 ↦ 0))
6764, 66eqeq12d 2625 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → ( = (𝑅 × {0}) ↔ (𝑘𝑅 ↦ (𝑘)) = (𝑘𝑅 ↦ 0)))
6862, 67bitr4d 270 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → (Σ𝑘𝑅 (𝑘) = 0 ↔ = (𝑅 × {0})))
69 xpeq1 5052 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 = ∅ → (𝑅 × {0}) = (∅ × {0}))
70 0xp 5122 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∅ × {0}) = ∅
7169, 70syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 = ∅ → (𝑅 × {0}) = ∅)
7271oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 = ∅ → ((𝑚 + 1) Ramsey (𝑅 × {0})) = ((𝑚 + 1) Ramsey ∅))
73 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → 𝑚 ∈ ℕ0)
74 peano2nn0 11210 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → (𝑚 + 1) ∈ ℕ0)
76 ram0 15564 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 + 1) ∈ ℕ0 → ((𝑚 + 1) Ramsey ∅) = (𝑚 + 1))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → ((𝑚 + 1) Ramsey ∅) = (𝑚 + 1))
7872, 77sylan9eqr 2666 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 = ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) = (𝑚 + 1))
7975adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 = ∅) → (𝑚 + 1) ∈ ℕ0)
8078, 79eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 = ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈ ℕ0)
8175adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → (𝑚 + 1) ∈ ℕ0)
82 simp-4l 802 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → 𝑅 ∈ Fin)
83 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → 𝑅 ≠ ∅)
84 ramz 15567 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 + 1) ∈ ℕ0𝑅 ∈ Fin ∧ 𝑅 ≠ ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) = 0)
8581, 82, 83, 84syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) = 0)
86 0nn0 11184 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℕ0
8785, 86syl6eqel 2696 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈ ℕ0)
8880, 87pm2.61dane 2869 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈ ℕ0)
89 oveq2 6557 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑅 × {0}) → ((𝑚 + 1) Ramsey ) = ((𝑚 + 1) Ramsey (𝑅 × {0})))
9089eleq1d 2672 . . . . . . . . . . . . . . . . . . . 20 ( = (𝑅 × {0}) → (((𝑚 + 1) Ramsey ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈ ℕ0))
9188, 90syl5ibrcom 236 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → ( = (𝑅 × {0}) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))
9268, 91sylbid 229 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ :𝑅⟶ℕ0) → (Σ𝑘𝑅 (𝑘) = 0 → ((𝑚 + 1) Ramsey ) ∈ ℕ0))
9392expimpd 627 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 0) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))
9493alrimiv 1842 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 0) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))
95 ffn 5958 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑅⟶ℕ0𝑓 Fn 𝑅)
9695ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → 𝑓 Fn 𝑅)
97 ffnfv 6295 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑅⟶ℕ ↔ (𝑓 Fn 𝑅 ∧ ∀𝑥𝑅 (𝑓𝑥) ∈ ℕ))
9897baib 942 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑅 → (𝑓:𝑅⟶ℕ ↔ ∀𝑥𝑅 (𝑓𝑥) ∈ ℕ))
9996, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → (𝑓:𝑅⟶ℕ ↔ ∀𝑥𝑅 (𝑓𝑥) ∈ ℕ))
100 simplr 788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) → 𝑚 ∈ ℕ0)
101100ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑚 ∈ ℕ0)
102101, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 + 1) ∈ ℕ0)
103 simp-4l 802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑅 ∈ Fin)
104 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑓:𝑅⟶ℕ)
105 nnssnn0 11172 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℕ ⊆ ℕ0
106 fss 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑅⟶ℕ ∧ ℕ ⊆ ℕ0) → 𝑓:𝑅⟶ℕ0)
107104, 105, 106sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑓:𝑅⟶ℕ0)
108101nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑚 ∈ ℂ)
109 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℂ
110 pncan 10166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
111108, 109, 110sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) − 1) = 𝑚)
112111oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) = (𝑚 Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))))
113103adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → 𝑅 ∈ Fin)
114 mptexg 6389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ Fin → (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) ∈ V)
115113, 114syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) ∈ V)
116 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))
117104ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → (𝑓𝑥) ∈ ℕ)
118 nnm1nn0 11211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓𝑥) ∈ ℕ → ((𝑓𝑥) − 1) ∈ ℕ0)
119117, 118syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → ((𝑓𝑥) − 1) ∈ ℕ0)
120119adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) ∧ 𝑦𝑅) → ((𝑓𝑥) − 1) ∈ ℕ0)
121107adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → 𝑓:𝑅⟶ℕ0)
122121ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) ∧ 𝑦𝑅) → (𝑓𝑦) ∈ ℕ0)
123120, 122ifcld 4081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) ∧ 𝑦𝑅) → if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)) ∈ ℕ0)
124 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))
125123, 124fmptd 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))):𝑅⟶ℕ0)
126 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → 𝑓:𝑅⟶ℕ)
127 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → 𝑥𝑅)
128 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑓:𝑅⟶ℕ ∧ 𝑘𝑅) → (𝑓𝑘) ∈ ℕ)
1291283ad2antl2 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → (𝑓𝑘) ∈ ℕ)
130129nncnd 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → (𝑓𝑘) ∈ ℂ)
131130subid1d 10260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → ((𝑓𝑘) − 0) = (𝑓𝑘))
132131ifeq2d 4055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → if(𝑘 = 𝑥, ((𝑓𝑘) − 1), ((𝑓𝑘) − 0)) = if(𝑘 = 𝑥, ((𝑓𝑘) − 1), (𝑓𝑘)))
133 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 = 𝑥 → (𝑓𝑘) = (𝑓𝑥))
134133adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) ∧ 𝑘 = 𝑥) → (𝑓𝑘) = (𝑓𝑥))
135134oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) ∧ 𝑘 = 𝑥) → ((𝑓𝑘) − 1) = ((𝑓𝑥) − 1))
136135ifeq1da 4066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → if(𝑘 = 𝑥, ((𝑓𝑘) − 1), (𝑓𝑘)) = if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)))
137132, 136eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = if(𝑘 = 𝑥, ((𝑓𝑘) − 1), ((𝑓𝑘) − 0)))
138 ovif2 6636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓𝑘) − if(𝑘 = 𝑥, 1, 0)) = if(𝑘 = 𝑥, ((𝑓𝑘) − 1), ((𝑓𝑘) − 0))
139137, 138syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = ((𝑓𝑘) − if(𝑘 = 𝑥, 1, 0)))
140139sumeq2dv 14281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = Σ𝑘𝑅 ((𝑓𝑘) − if(𝑘 = 𝑥, 1, 0)))
141 simp1 1054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → 𝑅 ∈ Fin)
142 0cn 9911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 0 ∈ ℂ
143109, 142keepel 4105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 if(𝑘 = 𝑥, 1, 0) ∈ ℂ
144143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) ∧ 𝑘𝑅) → if(𝑘 = 𝑥, 1, 0) ∈ ℂ)
145141, 130, 144fsumsub 14362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → Σ𝑘𝑅 ((𝑓𝑘) − if(𝑘 = 𝑥, 1, 0)) = (Σ𝑘𝑅 (𝑓𝑘) − Σ𝑘𝑅 if(𝑘 = 𝑥, 1, 0)))
146 elsng 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑘𝑅 → (𝑘 ∈ {𝑥} ↔ 𝑘 = 𝑥))
147146ifbid 4058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑘𝑅 → if(𝑘 ∈ {𝑥}, 1, 0) = if(𝑘 = 𝑥, 1, 0))
148147sumeq2i 14277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Σ𝑘𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = Σ𝑘𝑅 if(𝑘 = 𝑥, 1, 0)
149 simp3 1056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → 𝑥𝑅)
150149snssd 4281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → {𝑥} ⊆ 𝑅)
151 sumhash 15438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑅 ∈ Fin ∧ {𝑥} ⊆ 𝑅) → Σ𝑘𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = (#‘{𝑥}))
152141, 150, 151syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → Σ𝑘𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = (#‘{𝑥}))
153 hashsng 13020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑥𝑅 → (#‘{𝑥}) = 1)
154149, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → (#‘{𝑥}) = 1)
155152, 154eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → Σ𝑘𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = 1)
156148, 155syl5eqr 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → Σ𝑘𝑅 if(𝑘 = 𝑥, 1, 0) = 1)
157156oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → (Σ𝑘𝑅 (𝑓𝑘) − Σ𝑘𝑅 if(𝑘 = 𝑥, 1, 0)) = (Σ𝑘𝑅 (𝑓𝑘) − 1))
158140, 145, 1573eqtrd 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥𝑅) → Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = (Σ𝑘𝑅 (𝑓𝑘) − 1))
159113, 126, 127, 158syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = (Σ𝑘𝑅 (𝑓𝑘) − 1))
160 simplrl 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))
161160oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → (Σ𝑘𝑅 (𝑓𝑘) − 1) = ((𝑛 + 1) − 1))
162 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) → 𝑛 ∈ ℕ0)
163162ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → 𝑛 ∈ ℕ0)
164163nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → 𝑛 ∈ ℂ)
165 pncan 10166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
166164, 109, 165sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → ((𝑛 + 1) − 1) = 𝑛)
167159, 161, 1663eqtrd 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = 𝑛)
168125, 167jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → ((𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))):𝑅⟶ℕ0 ∧ Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = 𝑛))
169 feq1 5939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → (:𝑅⟶ℕ0 ↔ (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))):𝑅⟶ℕ0))
170 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → (𝑘) = ((𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))‘𝑘))
171 equequ1 1939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 = 𝑘 → (𝑦 = 𝑥𝑘 = 𝑥))
172 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 = 𝑘 → (𝑓𝑦) = (𝑓𝑘))
173171, 172ifbieq2d 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 = 𝑘 → if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)) = if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)))
174 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑓𝑥) − 1) ∈ V
175 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓𝑘) ∈ V
176174, 175ifex 4106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) ∈ V
177173, 124, 176fvmpt 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑘𝑅 → ((𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))‘𝑘) = if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)))
178170, 177sylan9eq 2664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) ∧ 𝑘𝑅) → (𝑘) = if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)))
179178sumeq2dv 14281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)))
180179eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → (Σ𝑘𝑅 (𝑘) = 𝑛 ↔ Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = 𝑛))
181169, 180anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) ↔ ((𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))):𝑅⟶ℕ0 ∧ Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = 𝑛)))
182 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → ((𝑚 + 1) Ramsey ) = ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))
183182eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → (((𝑚 + 1) Ramsey ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))) ∈ ℕ0))
184181, 183imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) → (((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ (((𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))):𝑅⟶ℕ0 ∧ Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = 𝑛) → ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))) ∈ ℕ0)))
185184spcgv 3266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) ∈ V → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) → (((𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))):𝑅⟶ℕ0 ∧ Σ𝑘𝑅 if(𝑘 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑘)) = 𝑛) → ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))) ∈ ℕ0)))
186115, 116, 168, 185syl3c 64 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥𝑅) → ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))) ∈ ℕ0)
187 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) = (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))
188186, 187fmptd 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))):𝑅⟶ℕ0)
189 elmapg 7757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℕ0 ∈ V ∧ 𝑅 ∈ Fin) → ((𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) ∈ (ℕ0𝑚 𝑅) ↔ (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))):𝑅⟶ℕ0))
1901, 103, 189sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) ∈ (ℕ0𝑚 𝑅) ↔ (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))):𝑅⟶ℕ0))
191188, 190mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) ∈ (ℕ0𝑚 𝑅))
192 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) → ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)
193192ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)
194 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 = (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) → (𝑚 Ramsey 𝑔) = (𝑚 Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))))
195194eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 = (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) → ((𝑚 Ramsey 𝑔) ∈ ℕ0 ↔ (𝑚 Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) ∈ ℕ0))
196195rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) ∈ (ℕ0𝑚 𝑅) → (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 → (𝑚 Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) ∈ ℕ0))
197191, 193, 196sylc 63 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) ∈ ℕ0)
198112, 197eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) ∈ ℕ0)
199 peano2nn0 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) ∈ ℕ0 → ((((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) + 1) ∈ ℕ0)
200198, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) + 1) ∈ ℕ0)
201 nn0p1nn 11209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ)
202100, 201syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) → (𝑚 + 1) ∈ ℕ)
203202ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 + 1) ∈ ℕ)
204 equequ1 1939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = 𝑤 → (𝑦 = 𝑥𝑤 = 𝑥))
205 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = 𝑤 → (𝑓𝑦) = (𝑓𝑤))
206204, 205ifbieq2d 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = 𝑤 → if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)) = if(𝑤 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑤)))
207206cbvmptv 4678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) = (𝑤𝑅 ↦ if(𝑤 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑤)))
208 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = 𝑧 → (𝑤 = 𝑥𝑤 = 𝑧))
209 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = 𝑧 → (𝑓𝑥) = (𝑓𝑧))
210209oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = 𝑧 → ((𝑓𝑥) − 1) = ((𝑓𝑧) − 1))
211208, 210ifbieq1d 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = 𝑧 → if(𝑤 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑤)) = if(𝑤 = 𝑧, ((𝑓𝑧) − 1), (𝑓𝑤)))
212211mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = 𝑧 → (𝑤𝑅 ↦ if(𝑤 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑤))) = (𝑤𝑅 ↦ if(𝑤 = 𝑧, ((𝑓𝑧) − 1), (𝑓𝑤))))
213207, 212syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = 𝑧 → (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))) = (𝑤𝑅 ↦ if(𝑤 = 𝑧, ((𝑓𝑧) − 1), (𝑓𝑤))))
214213oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑧 → ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))) = ((𝑚 + 1) Ramsey (𝑤𝑅 ↦ if(𝑤 = 𝑧, ((𝑓𝑧) − 1), (𝑓𝑤)))))
215214cbvmptv 4678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦))))) = (𝑧𝑅 ↦ ((𝑚 + 1) Ramsey (𝑤𝑅 ↦ if(𝑤 = 𝑧, ((𝑓𝑧) − 1), (𝑓𝑤)))))
216203, 103, 104, 215, 188, 198ramub1 15570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) Ramsey 𝑓) ≤ ((((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) + 1))
217 ramubcl 15560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑚 + 1) ∈ ℕ0𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ0) ∧ (((((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) + 1) ∈ ℕ0 ∧ ((𝑚 + 1) Ramsey 𝑓) ≤ ((((𝑚 + 1) − 1) Ramsey (𝑥𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝑓𝑥) − 1), (𝑓𝑦)))))) + 1))) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)
218102, 103, 107, 200, 216, 217syl32anc 1326 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)
219218expr 641 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1)) → (𝑓:𝑅⟶ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
220219adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → (𝑓:𝑅⟶ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
22199, 220sylbird 249 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → (∀𝑥𝑅 (𝑓𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
222 rexnal 2978 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑥𝑅 ¬ (𝑓𝑥) ∈ ℕ ↔ ¬ ∀𝑥𝑅 (𝑓𝑥) ∈ ℕ)
223 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → 𝑓:𝑅⟶ℕ0)
224223ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) ∧ 𝑥𝑅) → (𝑓𝑥) ∈ ℕ0)
225 elnn0 11171 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑥) ∈ ℕ0 ↔ ((𝑓𝑥) ∈ ℕ ∨ (𝑓𝑥) = 0))
226224, 225sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) ∧ 𝑥𝑅) → ((𝑓𝑥) ∈ ℕ ∨ (𝑓𝑥) = 0))
227226ord 391 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) ∧ 𝑥𝑅) → (¬ (𝑓𝑥) ∈ ℕ → (𝑓𝑥) = 0))
228202ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → (𝑚 + 1) ∈ ℕ)
229 simp-4l 802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → 𝑅 ∈ Fin)
230228, 229, 2233jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → ((𝑚 + 1) ∈ ℕ ∧ 𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ0))
231 ramz2 15566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑚 + 1) ∈ ℕ ∧ 𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ0) ∧ (𝑥𝑅 ∧ (𝑓𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) = 0)
232230, 231sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) ∧ (𝑥𝑅 ∧ (𝑓𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) = 0)
233232, 86syl6eqel 2696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) ∧ (𝑥𝑅 ∧ (𝑓𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)
234233expr 641 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) ∧ 𝑥𝑅) → ((𝑓𝑥) = 0 → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
235227, 234syld 46 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) ∧ 𝑥𝑅) → (¬ (𝑓𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
236235rexlimdva 3013 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → (∃𝑥𝑅 ¬ (𝑓𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
237222, 236syl5bir 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → (¬ ∀𝑥𝑅 (𝑓𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
238221, 237pm2.61d 169 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) ∧ ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)
239238exp31 628 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) → ((𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)))
240239alrimdv 1844 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) → ∀𝑓((𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)))
241 feq1 5939 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑓 → (:𝑅⟶ℕ0𝑓:𝑅⟶ℕ0))
242 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = 𝑓 → (𝑘) = (𝑓𝑘))
243242sumeq2sdv 14282 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = 𝑓 → Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘))
244243eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑓 → (Σ𝑘𝑅 (𝑘) = (𝑛 + 1) ↔ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1)))
245241, 244anbi12d 743 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑓 → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) ↔ (𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1))))
246 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . 23 ( = 𝑓 → ((𝑚 + 1) Ramsey ) = ((𝑚 + 1) Ramsey 𝑓))
247246eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑓 → (((𝑚 + 1) Ramsey ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
248245, 247imbi12d 333 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑓 → (((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ((𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)))
249248cbvalv 2261 . . . . . . . . . . . . . . . . . . . 20 (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ ∀𝑓((𝑓:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑓𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
250240, 249syl6ibr 241 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0𝑛 ∈ ℕ0)) → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
251250anassrs 678 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ 𝑛 ∈ ℕ0) → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
252251expcom 450 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))))
253252a2d 29 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)) → (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))))
25436, 41, 46, 51, 94, 253nn0ind 11348 . . . . . . . . . . . . . . 15 𝑘𝑅 (𝑓𝑘) ∈ ℕ0 → (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
255254com12 32 . . . . . . . . . . . . . 14 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → (Σ𝑘𝑅 (𝑓𝑘) ∈ ℕ0 → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
256255adantrl 748 . . . . . . . . . . . . 13 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (𝑓 ∈ (ℕ0𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → (Σ𝑘𝑅 (𝑓𝑘) ∈ ℕ0 → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0)))
25731, 256mpd 15 . . . . . . . . . . . 12 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (𝑓 ∈ (ℕ0𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → ∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0))
258243biantrud 527 . . . . . . . . . . . . . . 15 ( = 𝑓 → (:𝑅⟶ℕ0 ↔ (:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘))))
259258, 241bitr3d 269 . . . . . . . . . . . . . 14 ( = 𝑓 → ((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) ↔ 𝑓:𝑅⟶ℕ0))
260259, 247imbi12d 333 . . . . . . . . . . . . 13 ( = 𝑓 → (((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) ↔ (𝑓:𝑅⟶ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)))
261260spv 2248 . . . . . . . . . . . 12 (∀((:𝑅⟶ℕ0 ∧ Σ𝑘𝑅 (𝑘) = Σ𝑘𝑅 (𝑓𝑘)) → ((𝑚 + 1) Ramsey ) ∈ ℕ0) → (𝑓:𝑅⟶ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
262257, 29, 261sylc 63 . . . . . . . . . . 11 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ (𝑓 ∈ (ℕ0𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)
263262expr 641 . . . . . . . . . 10 (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ (ℕ0𝑚 𝑅)) → (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
264263ralrimdva 2952 . . . . . . . . 9 ((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) → (∀𝑔 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 → ∀𝑓 ∈ (ℕ0𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
26527, 264syl5bi 231 . . . . . . . 8 ((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) → (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 → ∀𝑓 ∈ (ℕ0𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0))
266265expcom 450 . . . . . . 7 (𝑚 ∈ ℕ0 → (𝑅 ∈ Fin → (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 → ∀𝑓 ∈ (ℕ0𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)))
267266a2d 29 . . . . . 6 (𝑚 ∈ ℕ0 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0) → (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈ ℕ0)))
2688, 12, 16, 20, 24, 267nn0ind 11348 . . . . 5 (𝑀 ∈ ℕ0 → (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈ ℕ0))
269268imp 444 . . . 4 ((𝑀 ∈ ℕ0𝑅 ∈ Fin) → ∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈ ℕ0)
270 oveq2 6557 . . . . . 6 (𝑓 = 𝐹 → (𝑀 Ramsey 𝑓) = (𝑀 Ramsey 𝐹))
271270eleq1d 2672 . . . . 5 (𝑓 = 𝐹 → ((𝑀 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑀 Ramsey 𝐹) ∈ ℕ0))
272271rspccv 3279 . . . 4 (∀𝑓 ∈ (ℕ0𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈ ℕ0 → (𝐹 ∈ (ℕ0𝑚 𝑅) → (𝑀 Ramsey 𝐹) ∈ ℕ0))
273269, 272syl 17 . . 3 ((𝑀 ∈ ℕ0𝑅 ∈ Fin) → (𝐹 ∈ (ℕ0𝑚 𝑅) → (𝑀 Ramsey 𝐹) ∈ ℕ0))
2744, 273sylbird 249 . 2 ((𝑀 ∈ ℕ0𝑅 ∈ Fin) → (𝐹:𝑅⟶ℕ0 → (𝑀 Ramsey 𝐹) ∈ ℕ0))
2752743impia 1253 1 ((𝑀 ∈ ℕ0𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈ ℕ0)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↑𝑚 cmap 7744  Fincfn 7841  ℂcc 9813  0cc0 9815  1c1 9816   + caddc 9818   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ0cn0 11169  #chash 12979  Σcsu 14264   Ramsey cram 15541 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-ram 15543 This theorem is referenced by:  ramsey  15572
 Copyright terms: Public domain W3C validator