| Step | Hyp | Ref
| Expression |
| 1 | | nn0ex 12532 |
. . . 4
⊢
ℕ0 ∈ V |
| 2 | | simpr 484 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
𝑅 ∈
Fin) |
| 3 | | elmapg 8879 |
. . . 4
⊢
((ℕ0 ∈ V ∧ 𝑅 ∈ Fin) → (𝐹 ∈ (ℕ0
↑m 𝑅)
↔ 𝐹:𝑅⟶ℕ0)) |
| 4 | 1, 2, 3 | sylancr 587 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
(𝐹 ∈
(ℕ0 ↑m 𝑅) ↔ 𝐹:𝑅⟶ℕ0)) |
| 5 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 Ramsey 𝑓) = (0 Ramsey 𝑓)) |
| 6 | 5 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (0 Ramsey
𝑓) ∈
ℕ0)) |
| 7 | 6 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑m 𝑅)(0 Ramsey 𝑓) ∈
ℕ0)) |
| 8 | 7 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(0
Ramsey 𝑓) ∈
ℕ0))) |
| 9 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑚 → (𝑥 Ramsey 𝑓) = (𝑚 Ramsey 𝑓)) |
| 10 | 9 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑚 Ramsey 𝑓) ∈
ℕ0)) |
| 11 | 10 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑓) ∈
ℕ0)) |
| 12 | 11 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑚 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑓) ∈
ℕ0))) |
| 13 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = (𝑚 + 1) → (𝑥 Ramsey 𝑓) = ((𝑚 + 1) Ramsey 𝑓)) |
| 14 | 13 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = (𝑚 + 1) → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 15 | 14 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → (∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑m 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 16 | 15 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = (𝑚 + 1) → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
| 17 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → (𝑥 Ramsey 𝑓) = (𝑀 Ramsey 𝑓)) |
| 18 | 17 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑀 Ramsey 𝑓) ∈
ℕ0)) |
| 19 | 18 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑀 Ramsey 𝑓) ∈
ℕ0)) |
| 20 | 19 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(𝑀 Ramsey 𝑓) ∈
ℕ0))) |
| 21 | | elmapi 8889 |
. . . . . . . 8
⊢ (𝑓 ∈ (ℕ0
↑m 𝑅)
→ 𝑓:𝑅⟶ℕ0) |
| 22 | | 0ramcl 17061 |
. . . . . . . 8
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ0) → (0
Ramsey 𝑓) ∈
ℕ0) |
| 23 | 21, 22 | sylan2 593 |
. . . . . . 7
⊢ ((𝑅 ∈ Fin ∧ 𝑓 ∈ (ℕ0
↑m 𝑅))
→ (0 Ramsey 𝑓) ∈
ℕ0) |
| 24 | 23 | ralrimiva 3146 |
. . . . . 6
⊢ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)(0
Ramsey 𝑓) ∈
ℕ0) |
| 25 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑚 Ramsey 𝑓) = (𝑚 Ramsey 𝑔)) |
| 26 | 25 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((𝑚 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑚 Ramsey 𝑔) ∈
ℕ0)) |
| 27 | 26 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈
ℕ0) |
| 28 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑m 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → 𝑅 ∈ Fin) |
| 29 | 21 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑m 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → 𝑓:𝑅⟶ℕ0) |
| 30 | 29 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑m 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈
ℕ0) |
| 31 | 28, 30 | fsumnn0cl 15772 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑m 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) →
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) ∈
ℕ0) |
| 32 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 0 → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥 ↔ Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0)) |
| 33 | 32 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0))) |
| 34 | 33 | imbi1d 341 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 35 | 34 | albidv 1920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 36 | 35 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
| 37 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑛 → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥 ↔ Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛)) |
| 38 | 37 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑛 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛))) |
| 39 | 38 | imbi1d 341 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑛 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 40 | 39 | albidv 1920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑛 → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 41 | 40 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑛 → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧
∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
| 42 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑛 + 1) → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥 ↔ Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1))) |
| 43 | 42 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑛 + 1) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)))) |
| 44 | 43 | imbi1d 341 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑛 + 1) → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 45 | 44 | albidv 1920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑛 + 1) → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 46 | 45 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑛 + 1) → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧
∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
| 47 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥 ↔ Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘))) |
| 48 | 47 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)))) |
| 49 | 48 | imbi1d 341 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 50 | 49 | albidv 1920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 51 | 50 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0) ∧
∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ↔ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
| 52 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → 𝑅 ∈ Fin) |
| 53 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:𝑅⟶ℕ0 ∧ 𝑘 ∈ 𝑅) → (ℎ‘𝑘) ∈
ℕ0) |
| 54 | 53 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑘 ∈ 𝑅) → (ℎ‘𝑘) ∈
ℕ0) |
| 55 | 54 | nn0red 12588 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑘 ∈ 𝑅) → (ℎ‘𝑘) ∈ ℝ) |
| 56 | 54 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑘 ∈ 𝑅) → 0 ≤ (ℎ‘𝑘)) |
| 57 | 52, 55, 56 | fsum00 15834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 ↔ ∀𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0)) |
| 58 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ‘𝑘) ∈ V |
| 59 | 58 | rgenw 3065 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
∀𝑘 ∈
𝑅 (ℎ‘𝑘) ∈ V |
| 60 | | mpteqb 7035 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑘 ∈
𝑅 (ℎ‘𝑘) ∈ V → ((𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0) ↔ ∀𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0)) |
| 61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0) ↔ ∀𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) |
| 62 | 57, 61 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 ↔ (𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0))) |
| 63 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ℎ:𝑅⟶ℕ0) |
| 64 | 63 | feqmptd 6977 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ℎ = (𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘))) |
| 65 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 × {0}) = (𝑘 ∈ 𝑅 ↦ 0) |
| 66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (𝑅 × {0}) = (𝑘 ∈ 𝑅 ↦ 0)) |
| 67 | 64, 66 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (ℎ = (𝑅 × {0}) ↔ (𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0))) |
| 68 | 62, 67 | bitr4d 282 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 ↔ ℎ = (𝑅 × {0}))) |
| 69 | | xpeq1 5699 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑅 = ∅ → (𝑅 × {0}) = (∅ ×
{0})) |
| 70 | | 0xp 5784 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∅
× {0}) = ∅ |
| 71 | 69, 70 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 = ∅ → (𝑅 × {0}) =
∅) |
| 72 | 71 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 = ∅ → ((𝑚 + 1) Ramsey (𝑅 × {0})) = ((𝑚 + 1) Ramsey ∅)) |
| 73 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → 𝑚 ∈
ℕ0) |
| 74 | | peano2nn0 12566 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
| 75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (𝑚 + 1) ∈
ℕ0) |
| 76 | | ram0 17060 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 + 1) ∈ ℕ0
→ ((𝑚 + 1) Ramsey
∅) = (𝑚 +
1)) |
| 77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ((𝑚 + 1) Ramsey ∅) = (𝑚 + 1)) |
| 78 | 72, 77 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) = (𝑚 + 1)) |
| 79 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → (𝑚 + 1) ∈
ℕ0) |
| 80 | 78, 79 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0) |
| 81 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → (𝑚 + 1) ∈
ℕ0) |
| 82 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → 𝑅 ∈ Fin) |
| 83 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → 𝑅 ≠ ∅) |
| 84 | | ramz 17063 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑚 + 1) ∈ ℕ0
∧ 𝑅 ∈ Fin ∧
𝑅 ≠ ∅) →
((𝑚 + 1) Ramsey (𝑅 × {0})) =
0) |
| 85 | 81, 82, 83, 84 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) = 0) |
| 86 | | 0nn0 12541 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℕ0 |
| 87 | 85, 86 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0) |
| 88 | 80, 87 | pm2.61dane 3029 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0) |
| 89 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑅 × {0}) → ((𝑚 + 1) Ramsey ℎ) = ((𝑚 + 1) Ramsey (𝑅 × {0}))) |
| 90 | 89 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = (𝑅 × {0}) → (((𝑚 + 1) Ramsey ℎ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0)) |
| 91 | 88, 90 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (ℎ = (𝑅 × {0}) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
| 92 | 68, 91 | sylbid 240 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
| 93 | 92 | expimpd 453 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
| 94 | 93 | alrimiv 1927 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
| 95 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑅⟶ℕ0 → 𝑓 Fn 𝑅) |
| 96 | 95 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → 𝑓 Fn 𝑅) |
| 97 | | ffnfv 7139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑅⟶ℕ ↔ (𝑓 Fn 𝑅 ∧ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ)) |
| 98 | 97 | baib 535 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑅 → (𝑓:𝑅⟶ℕ ↔ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ)) |
| 99 | 96, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (𝑓:𝑅⟶ℕ ↔ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ)) |
| 100 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ 𝑚 ∈
ℕ0) |
| 101 | 100 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑚 ∈ ℕ0) |
| 102 | 101, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 + 1) ∈
ℕ0) |
| 103 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑅 ∈ Fin) |
| 104 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑓:𝑅⟶ℕ) |
| 105 | | nnssnn0 12529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ℕ
⊆ ℕ0 |
| 106 | | fss 6752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓:𝑅⟶ℕ ∧ ℕ ⊆
ℕ0) → 𝑓:𝑅⟶ℕ0) |
| 107 | 104, 105,
106 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑓:𝑅⟶ℕ0) |
| 108 | 101 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑚 ∈ ℂ) |
| 109 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 ∈
ℂ |
| 110 | | pncan 11514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑚 + 1)
− 1) = 𝑚) |
| 111 | 108, 109,
110 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) − 1) = 𝑚) |
| 112 | 111 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (((𝑚 + 1) − 1) Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) = (𝑚 Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))))) |
| 113 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑔 = (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) → (𝑚 Ramsey 𝑔) = (𝑚 Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))))) |
| 114 | 113 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑔 = (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) → ((𝑚 Ramsey 𝑔) ∈ ℕ0 ↔ (𝑚 Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) ∈
ℕ0)) |
| 115 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈
ℕ0) |
| 116 | 115 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈
ℕ0) |
| 117 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑅 ∈ Fin) |
| 118 | 117 | mptexd 7244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) ∈ V) |
| 119 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
| 120 | 104 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → (𝑓‘𝑥) ∈ ℕ) |
| 121 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑓‘𝑥) ∈ ℕ → ((𝑓‘𝑥) − 1) ∈
ℕ0) |
| 122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → ((𝑓‘𝑥) − 1) ∈
ℕ0) |
| 123 | 122 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) ∧ 𝑦 ∈ 𝑅) → ((𝑓‘𝑥) − 1) ∈
ℕ0) |
| 124 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑓:𝑅⟶ℕ0) |
| 125 | 124 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) ∧ 𝑦 ∈ 𝑅) → (𝑓‘𝑦) ∈
ℕ0) |
| 126 | 123, 125 | ifcld 4572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) ∧ 𝑦 ∈ 𝑅) → if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)) ∈
ℕ0) |
| 127 | 126 | fmpttd 7135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0) |
| 128 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑓:𝑅⟶ℕ) |
| 129 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ 𝑅) |
| 130 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑓:𝑅⟶ℕ ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈ ℕ) |
| 131 | 130 | 3ad2antl2 1187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈ ℕ) |
| 132 | 131 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈ ℂ) |
| 133 | 132 | subid1d 11609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → ((𝑓‘𝑘) − 0) = (𝑓‘𝑘)) |
| 134 | 133 | ifeq2d 4546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), ((𝑓‘𝑘) − 0)) = if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), (𝑓‘𝑘))) |
| 135 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑘 = 𝑥 → (𝑓‘𝑘) = (𝑓‘𝑥)) |
| 136 | 135 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) ∧ 𝑘 = 𝑥) → (𝑓‘𝑘) = (𝑓‘𝑥)) |
| 137 | 136 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) ∧ 𝑘 = 𝑥) → ((𝑓‘𝑘) − 1) = ((𝑓‘𝑥) − 1)) |
| 138 | 137 | ifeq1da 4557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), (𝑓‘𝑘)) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
| 139 | 134, 138 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), ((𝑓‘𝑘) − 0))) |
| 140 | | ovif2 7532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0)) = if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), ((𝑓‘𝑘) − 0)) |
| 141 | 139, 140 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0))) |
| 142 | 141 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = Σ𝑘 ∈ 𝑅 ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0))) |
| 143 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → 𝑅 ∈ Fin) |
| 144 | | 0cn 11253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 0 ∈
ℂ |
| 145 | 109, 144 | ifcli 4573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ if(𝑘 = 𝑥, 1, 0) ∈ ℂ |
| 146 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, 1, 0) ∈ ℂ) |
| 147 | 143, 132,
146 | fsumsub 15824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0)) = (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0))) |
| 148 | | elsng 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑘 ∈ 𝑅 → (𝑘 ∈ {𝑥} ↔ 𝑘 = 𝑥)) |
| 149 | 148 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑘 ∈ 𝑅 → if(𝑘 ∈ {𝑥}, 1, 0) = if(𝑘 = 𝑥, 1, 0)) |
| 150 | 149 | sumeq2i 15734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
Σ𝑘 ∈
𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0) |
| 151 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ 𝑅) |
| 152 | 151 | snssd 4809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → {𝑥} ⊆ 𝑅) |
| 153 | | sumhash 16934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑅 ∈ Fin ∧ {𝑥} ⊆ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = (♯‘{𝑥})) |
| 154 | 143, 152,
153 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = (♯‘{𝑥})) |
| 155 | | hashsng 14408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑥 ∈ 𝑅 → (♯‘{𝑥}) = 1) |
| 156 | 151, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → (♯‘{𝑥}) = 1) |
| 157 | 154, 156 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = 1) |
| 158 | 150, 157 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0) = 1) |
| 159 | 158 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0)) = (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − 1)) |
| 160 | 142, 147,
159 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − 1)) |
| 161 | 117, 128,
129, 160 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − 1)) |
| 162 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) |
| 163 | 162 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − 1) = ((𝑛 + 1) − 1)) |
| 164 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) → 𝑛 ∈
ℕ0) |
| 165 | 164 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑛 ∈ ℕ0) |
| 166 | 165 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑛 ∈ ℂ) |
| 167 | | pncan 11514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
| 168 | 166, 109,
167 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → ((𝑛 + 1) − 1) = 𝑛) |
| 169 | 161, 163,
168 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛) |
| 170 | 127, 169 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛)) |
| 171 | | feq1 6716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (ℎ:𝑅⟶ℕ0 ↔ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0)) |
| 172 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (ℎ‘𝑘) = ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))‘𝑘)) |
| 173 | | equequ1 2024 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑦 = 𝑘 → (𝑦 = 𝑥 ↔ 𝑘 = 𝑥)) |
| 174 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑦 = 𝑘 → (𝑓‘𝑦) = (𝑓‘𝑘)) |
| 175 | 173, 174 | ifbieq2d 4552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 = 𝑘 → if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
| 176 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) |
| 177 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑓‘𝑥) − 1) ∈ V |
| 178 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓‘𝑘) ∈ V |
| 179 | 177, 178 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) ∈ V |
| 180 | 175, 176,
179 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑘 ∈ 𝑅 → ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))‘𝑘) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
| 181 | 172, 180 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) ∧ 𝑘 ∈ 𝑅) → (ℎ‘𝑘) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
| 182 | 181 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
| 183 | 182 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛 ↔ Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛)) |
| 184 | 171, 183 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) ↔ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛))) |
| 185 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → ((𝑚 + 1) Ramsey ℎ) = ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) |
| 186 | 185 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (((𝑚 + 1) Ramsey ℎ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) ∈
ℕ0)) |
| 187 | 184, 186 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛) → ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) ∈
ℕ0))) |
| 188 | 187 | spcgv 3596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) ∈ V → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) → (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛) → ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) ∈
ℕ0))) |
| 189 | 118, 119,
170, 188 | syl3c 66 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) ∈
ℕ0) |
| 190 | 189 | fmpttd 7135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))):𝑅⟶ℕ0) |
| 191 | | elmapg 8879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((ℕ0 ∈ V ∧ 𝑅 ∈ Fin) → ((𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) ∈ (ℕ0
↑m 𝑅)
↔ (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))):𝑅⟶ℕ0)) |
| 192 | 1, 103, 191 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) ∈ (ℕ0
↑m 𝑅)
↔ (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))):𝑅⟶ℕ0)) |
| 193 | 190, 192 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) ∈ (ℕ0
↑m 𝑅)) |
| 194 | 114, 116,
193 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) ∈
ℕ0) |
| 195 | 112, 194 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (((𝑚 + 1) − 1) Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) ∈
ℕ0) |
| 196 | | peano2nn0 12566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑚 + 1) − 1) Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) ∈ ℕ0 →
((((𝑚 + 1) − 1)
Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) + 1) ∈
ℕ0) |
| 197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((((𝑚 + 1) − 1) Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) + 1) ∈
ℕ0) |
| 198 | | nn0p1nn 12565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) |
| 199 | 100, 198 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑚 + 1) ∈
ℕ) |
| 200 | 199 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 + 1) ∈ ℕ) |
| 201 | | equequ1 2024 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = 𝑤 → (𝑦 = 𝑥 ↔ 𝑤 = 𝑥)) |
| 202 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = 𝑤 → (𝑓‘𝑦) = (𝑓‘𝑤)) |
| 203 | 201, 202 | ifbieq2d 4552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = 𝑤 → if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)) = if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤))) |
| 204 | 203 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) = (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤))) |
| 205 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = 𝑧 → (𝑤 = 𝑥 ↔ 𝑤 = 𝑧)) |
| 206 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧)) |
| 207 | 206 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥) − 1) = ((𝑓‘𝑧) − 1)) |
| 208 | 205, 207 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = 𝑧 → if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤)) = if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤))) |
| 209 | 208 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤))) = (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤)))) |
| 210 | 204, 209 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) = (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤)))) |
| 211 | 210 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑧 → ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) = ((𝑚 + 1) Ramsey (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤))))) |
| 212 | 211 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) = (𝑧 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤))))) |
| 213 | 200, 103,
104, 212, 190, 195 | ramub1 17066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) Ramsey 𝑓) ≤ ((((𝑚 + 1) − 1) Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) + 1)) |
| 214 | | ramubcl 17056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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) |
| 215 | 102, 103,
107, 197, 213, 214 | syl32anc 1380 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
| 216 | 215 | expr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → (𝑓:𝑅⟶ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 217 | 216 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (𝑓:𝑅⟶ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 218 | 99, 217 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 219 | | rexnal 3100 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃𝑥 ∈
𝑅 ¬ (𝑓‘𝑥) ∈ ℕ ↔ ¬ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ) |
| 220 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → 𝑓:𝑅⟶ℕ0) |
| 221 | 220 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → (𝑓‘𝑥) ∈
ℕ0) |
| 222 | | elnn0 12528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓‘𝑥) ∈ ℕ0 ↔ ((𝑓‘𝑥) ∈ ℕ ∨ (𝑓‘𝑥) = 0)) |
| 223 | 221, 222 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → ((𝑓‘𝑥) ∈ ℕ ∨ (𝑓‘𝑥) = 0)) |
| 224 | 223 | ord 865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → (¬ (𝑓‘𝑥) ∈ ℕ → (𝑓‘𝑥) = 0)) |
| 225 | 199 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (𝑚 + 1) ∈ ℕ) |
| 226 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → 𝑅 ∈ Fin) |
| 227 | 225, 226,
220 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → ((𝑚 + 1) ∈ ℕ ∧ 𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ0)) |
| 228 | | ramz2 17062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑚 + 1) ∈ ℕ ∧ 𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ0) ∧ (𝑥 ∈ 𝑅 ∧ (𝑓‘𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) = 0) |
| 229 | 227, 228 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ (𝑥 ∈ 𝑅 ∧ (𝑓‘𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) = 0) |
| 230 | 229, 86 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ (𝑥 ∈ 𝑅 ∧ (𝑓‘𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
| 231 | 230 | expr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → ((𝑓‘𝑥) = 0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 232 | 224, 231 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → (¬ (𝑓‘𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 233 | 232 | rexlimdva 3155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (∃𝑥 ∈ 𝑅 ¬ (𝑓‘𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 234 | 219, 233 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (¬ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 235 | 218, 234 | pm2.61d 179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
| 236 | 235 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) → ((𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
| 237 | 236 | alrimdv 1929 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) →
∀𝑓((𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
| 238 | | feq1 6716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑓 → (ℎ:𝑅⟶ℕ0 ↔ 𝑓:𝑅⟶ℕ0)) |
| 239 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = 𝑓 → (ℎ‘𝑘) = (𝑓‘𝑘)) |
| 240 | 239 | sumeq2sdv 15739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = 𝑓 → Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) |
| 241 | 240 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑓 → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1) ↔ Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) |
| 242 | 238, 241 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑓 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) ↔ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)))) |
| 243 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑓 → ((𝑚 + 1) Ramsey ℎ) = ((𝑚 + 1) Ramsey 𝑓)) |
| 244 | 243 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑓 → (((𝑚 + 1) Ramsey ℎ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 245 | 242, 244 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑓 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
| 246 | 245 | cbvalvw 2035 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀𝑓((𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 247 | 237, 246 | imbitrrdi 252 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 248 | 247 | anassrs 467 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 249 | 248 | expcom 413 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ0
→ (((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
(∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
| 250 | 249 | a2d 29 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
→ ((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) → (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
| 251 | 36, 41, 46, 51, 94, 250 | nn0ind 12713 |
. . . . . . . . . . . . . . 15
⊢
(Σ𝑘 ∈
𝑅 (𝑓‘𝑘) ∈ ℕ0 → (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 252 | 251 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) ∈ ℕ0 →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 253 | 252 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑m 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) →
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) ∈ ℕ0 →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
| 254 | 31, 253 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑m 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
| 255 | 240 | biantrud 531 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝑓 → (ℎ:𝑅⟶ℕ0 ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)))) |
| 256 | 255, 238 | bitr3d 281 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝑓 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) ↔ 𝑓:𝑅⟶ℕ0)) |
| 257 | 256, 244 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑓 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ (𝑓:𝑅⟶ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
| 258 | 257 | spvv 1996 |
. . . . . . . . . . . 12
⊢
(∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) → (𝑓:𝑅⟶ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 259 | 254, 29, 258 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑m 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
| 260 | 259 | expr 456 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ 𝑓 ∈
(ℕ0 ↑m 𝑅)) → (∀𝑔 ∈ (ℕ0
↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 261 | 260 | ralrimdva 3154 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
→ (∀𝑔 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 →
∀𝑓 ∈
(ℕ0 ↑m 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 262 | 27, 261 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
→ (∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 →
∀𝑓 ∈
(ℕ0 ↑m 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
| 263 | 262 | expcom 413 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝑅 ∈ Fin →
(∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 →
∀𝑓 ∈
(ℕ0 ↑m 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
| 264 | 263 | a2d 29 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ ((𝑅 ∈ Fin
→ ∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0) → (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑m 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
| 265 | 8, 12, 16, 20, 24, 264 | nn0ind 12713 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑅 ∈ Fin →
∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑀 Ramsey 𝑓) ∈
ℕ0)) |
| 266 | 265 | imp 406 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑀 Ramsey 𝑓) ∈
ℕ0) |
| 267 | | oveq2 7439 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑀 Ramsey 𝑓) = (𝑀 Ramsey 𝐹)) |
| 268 | 267 | eleq1d 2826 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝑀 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
| 269 | 268 | rspccv 3619 |
. . . 4
⊢
(∀𝑓 ∈
(ℕ0 ↑m 𝑅)(𝑀 Ramsey 𝑓) ∈ ℕ0 → (𝐹 ∈ (ℕ0
↑m 𝑅)
→ (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
| 270 | 266, 269 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
(𝐹 ∈
(ℕ0 ↑m 𝑅) → (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
| 271 | 4, 270 | sylbird 260 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
(𝐹:𝑅⟶ℕ0 → (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
| 272 | 271 | 3impia 1118 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin ∧
𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈
ℕ0) |