Step | Hyp | Ref
| Expression |
1 | | nn0ex 11175 |
. . . 4
⊢
ℕ0 ∈ V |
2 | | simpr 476 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
𝑅 ∈
Fin) |
3 | | elmapg 7757 |
. . . 4
⊢
((ℕ0 ∈ V ∧ 𝑅 ∈ Fin) → (𝐹 ∈ (ℕ0
↑𝑚 𝑅) ↔ 𝐹:𝑅⟶ℕ0)) |
4 | 1, 2, 3 | sylancr 694 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
(𝐹 ∈
(ℕ0 ↑𝑚 𝑅) ↔ 𝐹:𝑅⟶ℕ0)) |
5 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 Ramsey 𝑓) = (0 Ramsey 𝑓)) |
6 | 5 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (0 Ramsey
𝑓) ∈
ℕ0)) |
7 | 6 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(0 Ramsey 𝑓) ∈
ℕ0)) |
8 | 7 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(0 Ramsey 𝑓) ∈
ℕ0))) |
9 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑚 → (𝑥 Ramsey 𝑓) = (𝑚 Ramsey 𝑓)) |
10 | 9 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑚 Ramsey 𝑓) ∈
ℕ0)) |
11 | 10 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈
ℕ0)) |
12 | 11 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = 𝑚 → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈
ℕ0))) |
13 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = (𝑚 + 1) → (𝑥 Ramsey 𝑓) = ((𝑚 + 1) Ramsey 𝑓)) |
14 | 13 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = (𝑚 + 1) → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
15 | 14 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → (∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
16 | 15 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = (𝑚 + 1) → ((𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0) ↔ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
17 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → (𝑥 Ramsey 𝑓) = (𝑀 Ramsey 𝑓)) |
18 | 17 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → ((𝑥 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑀 Ramsey 𝑓) ∈
ℕ0)) |
19 | 18 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(𝑥 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈
ℕ0)) |
20 | 19 | imbi2d 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) |
23 | 21, 22 | sylan2 490 |
. . . . . . 7
⊢ ((𝑅 ∈ Fin ∧ 𝑓 ∈ (ℕ0
↑𝑚 𝑅)) → (0 Ramsey 𝑓) ∈
ℕ0) |
24 | 23 | ralrimiva 2949 |
. . . . . 6
⊢ (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)(0 Ramsey 𝑓) ∈
ℕ0) |
25 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑚 Ramsey 𝑓) = (𝑚 Ramsey 𝑔)) |
26 | 25 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((𝑚 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑚 Ramsey 𝑔) ∈
ℕ0)) |
27 | 26 | cbvralv 3147 |
. . . . . . . . 9
⊢
(∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 ↔
∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈
ℕ0) |
28 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → 𝑅 ∈ Fin) |
29 | 21 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → 𝑓:𝑅⟶ℕ0) |
30 | 29 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈
ℕ0) |
31 | 28, 30 | fsumnn0cl 14314 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) →
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) ∈
ℕ0) |
32 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 0 → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥 ↔ Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0)) |
33 | 32 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0))) |
34 | 33 | imbi1d 330 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
35 | 34 | albidv 1836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
36 | 35 | imbi2d 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
⊢ (𝑥 = 𝑛 → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥 ↔ Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛)) |
38 | 37 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑛 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛))) |
39 | 38 | imbi1d 330 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑛 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
40 | 39 | albidv 1836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑛 → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
41 | 40 | imbi2d 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))) |
43 | 42 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑛 + 1) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)))) |
44 | 43 | imbi1d 330 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑛 + 1) → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
45 | 44 | albidv 1836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑛 + 1) → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
46 | 45 | imbi2d 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
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥 ↔ Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘))) |
48 | 47 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)))) |
49 | 48 | imbi1d 330 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
50 | 49 | albidv 1836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑥) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
51 | 50 | imbi2d 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) |
54 | 53 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑘 ∈ 𝑅) → (ℎ‘𝑘) ∈
ℕ0) |
55 | 54 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑘 ∈ 𝑅) → (ℎ‘𝑘) ∈ ℝ) |
56 | 54 | nn0ge0d 11231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑘 ∈ 𝑅) → 0 ≤ (ℎ‘𝑘)) |
57 | 52, 55, 56 | fsum00 14371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 ↔ ∀𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0)) |
58 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ‘𝑘) ∈ V |
59 | 58 | rgenw 2908 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
∀𝑘 ∈
𝑅 (ℎ‘𝑘) ∈ V |
60 | | mpteqb 6207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑘 ∈
𝑅 (ℎ‘𝑘) ∈ V → ((𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0) ↔ ∀𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0)) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0) ↔ ∀𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) |
62 | 57, 61 | syl6bbr 277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 ↔ (𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0))) |
63 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ℎ:𝑅⟶ℕ0) |
64 | 63 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ℎ = (𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘))) |
65 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 × {0}) = (𝑘 ∈ 𝑅 ↦ 0) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (𝑅 × {0}) = (𝑘 ∈ 𝑅 ↦ 0)) |
67 | 64, 66 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (ℎ = (𝑅 × {0}) ↔ (𝑘 ∈ 𝑅 ↦ (ℎ‘𝑘)) = (𝑘 ∈ 𝑅 ↦ 0))) |
68 | 62, 67 | bitr4d 270 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 ↔ ℎ = (𝑅 × {0}))) |
69 | | xpeq1 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑅 = ∅ → (𝑅 × {0}) = (∅ ×
{0})) |
70 | | 0xp 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∅
× {0}) = ∅ |
71 | 69, 70 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 = ∅ → (𝑅 × {0}) =
∅) |
72 | 71 | oveq2d 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) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (𝑚 + 1) ∈
ℕ0) |
76 | | ram0 15564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 + 1) ∈ ℕ0
→ ((𝑚 + 1) Ramsey
∅) = (𝑚 +
1)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ((𝑚 + 1) Ramsey ∅) = (𝑚 + 1)) |
78 | 72, 77 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) = (𝑚 + 1)) |
79 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → (𝑚 + 1) ∈
ℕ0) |
80 | 78, 79 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 = ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0) |
81 | 75 | adantr 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) |
85 | 81, 82, 83, 84 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) = 0) |
86 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℕ0 |
87 | 85, 86 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) ∧ 𝑅 ≠ ∅) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0) |
88 | 80, 87 | pm2.61dane 2869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0) |
89 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑅 × {0}) → ((𝑚 + 1) Ramsey ℎ) = ((𝑚 + 1) Ramsey (𝑅 × {0}))) |
90 | 89 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = (𝑅 × {0}) → (((𝑚 + 1) Ramsey ℎ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey (𝑅 × {0})) ∈
ℕ0)) |
91 | 88, 90 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) → (ℎ = (𝑅 × {0}) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
92 | 68, 91 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ ℎ:𝑅⟶ℕ0) →
(Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0 → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
93 | 92 | expimpd 627 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
94 | 93 | alrimiv 1842 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 0) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
95 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑅⟶ℕ0 → 𝑓 Fn 𝑅) |
96 | 95 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → 𝑓 Fn 𝑅) |
97 | | ffnfv 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑅⟶ℕ ↔ (𝑓 Fn 𝑅 ∧ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ)) |
98 | 97 | baib 942 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑅 → (𝑓:𝑅⟶ℕ ↔ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ)) |
99 | 96, 98 | syl 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) |
101 | 100 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑚 ∈ ℕ0) |
102 | 101, 74 | syl 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) |
107 | 104, 105,
106 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → 𝑓:𝑅⟶ℕ0) |
108 | 101 | nn0cnd 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) = 𝑚) |
111 | 108, 109,
110 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) − 1) = 𝑚) |
112 | 111 | oveq1d 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), (𝑓‘𝑦))))))) |
113 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑅 ∈ Fin) |
114 | | mptexg 6389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑅 ∈ Fin → (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) ∈ V) |
115 | 113, 114 | syl 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)) |
117 | 104 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → (𝑓‘𝑥) ∈ ℕ) |
118 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑓‘𝑥) ∈ ℕ → ((𝑓‘𝑥) − 1) ∈
ℕ0) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → ((𝑓‘𝑥) − 1) ∈
ℕ0) |
120 | 119 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) ∧ 𝑦 ∈ 𝑅) → ((𝑓‘𝑥) − 1) ∈
ℕ0) |
121 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑓:𝑅⟶ℕ0) |
122 | 121 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) ∧ 𝑦 ∈ 𝑅) → (𝑓‘𝑦) ∈
ℕ0) |
123 | 120, 122 | ifcld 4081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) ∧ 𝑦 ∈ 𝑅) → if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)) ∈
ℕ0) |
124 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) |
125 | 123, 124 | fmptd 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
⊢ ((𝑓:𝑅⟶ℕ ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈ ℕ) |
129 | 128 | 3ad2antl2 1217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈ ℕ) |
130 | 129 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → (𝑓‘𝑘) ∈ ℂ) |
131 | 130 | subid1d 10260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → ((𝑓‘𝑘) − 0) = (𝑓‘𝑘)) |
132 | 131 | ifeq2d 4055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), ((𝑓‘𝑘) − 0)) = if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), (𝑓‘𝑘))) |
133 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑘 = 𝑥 → (𝑓‘𝑘) = (𝑓‘𝑥)) |
134 | 133 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) ∧ 𝑘 = 𝑥) → (𝑓‘𝑘) = (𝑓‘𝑥)) |
135 | 134 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) ∧ 𝑘 = 𝑥) → ((𝑓‘𝑘) − 1) = ((𝑓‘𝑥) − 1)) |
136 | 135 | ifeq1da 4066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), (𝑓‘𝑘)) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
137 | 132, 136 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), ((𝑓‘𝑘) − 0))) |
138 | | ovif2 6636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0)) = if(𝑘 = 𝑥, ((𝑓‘𝑘) − 1), ((𝑓‘𝑘) − 0)) |
139 | 137, 138 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0))) |
140 | 139 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = Σ𝑘 ∈ 𝑅 ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0))) |
141 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → 𝑅 ∈ Fin) |
142 | | 0cn 9911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 0 ∈
ℂ |
143 | 109, 142 | keepel 4105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ if(𝑘 = 𝑥, 1, 0) ∈ ℂ |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) ∧ 𝑘 ∈ 𝑅) → if(𝑘 = 𝑥, 1, 0) ∈ ℂ) |
145 | 141, 130,
144 | fsumsub 14362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 ((𝑓‘𝑘) − if(𝑘 = 𝑥, 1, 0)) = (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0))) |
146 | | elsng 4139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑘 ∈ 𝑅 → (𝑘 ∈ {𝑥} ↔ 𝑘 = 𝑥)) |
147 | 146 | ifbid 4058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑘 ∈ 𝑅 → if(𝑘 ∈ {𝑥}, 1, 0) = if(𝑘 = 𝑥, 1, 0)) |
148 | 147 | sumeq2i 14277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
Σ𝑘 ∈
𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0) |
149 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ 𝑅) |
150 | 149 | snssd 4281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → {𝑥} ⊆ 𝑅) |
151 | | sumhash 15438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑅 ∈ Fin ∧ {𝑥} ⊆ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = (#‘{𝑥})) |
152 | 141, 150,
151 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = (#‘{𝑥})) |
153 | | hashsng 13020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑥 ∈ 𝑅 → (#‘{𝑥}) = 1) |
154 | 149, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → (#‘{𝑥}) = 1) |
155 | 152, 154 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 ∈ {𝑥}, 1, 0) = 1) |
156 | 148, 155 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0) = 1) |
157 | 156 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, 1, 0)) = (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − 1)) |
158 | 140, 145,
157 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑅 ∈ Fin ∧ 𝑓:𝑅⟶ℕ ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = (Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) − 1)) |
159 | 113, 126,
127, 158 | syl3anc 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)) |
161 | 160 | oveq1d 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) |
163 | 162 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑛 ∈ ℕ0) |
164 | 163 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → 𝑛 ∈ ℂ) |
165 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
166 | 164, 109,
165 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → ((𝑛 + 1) − 1) = 𝑛) |
167 | 159, 161,
166 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) ∧ 𝑥 ∈ 𝑅) → Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛) |
168 | 125, 167 | jca 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
⊢ (𝑦 = 𝑘 → (𝑓‘𝑦) = (𝑓‘𝑘)) |
173 | 171, 172 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 = 𝑘 → if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
174 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑓‘𝑥) − 1) ∈ V |
175 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓‘𝑘) ∈ V |
176 | 174, 175 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) ∈ V |
177 | 173, 124,
176 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑘 ∈ 𝑅 → ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))‘𝑘) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
178 | 170, 177 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) ∧ 𝑘 ∈ 𝑅) → (ℎ‘𝑘) = if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
179 | 178 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘))) |
180 | 179 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛 ↔ Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛)) |
181 | 169, 180 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) ↔ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛))) |
182 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → ((𝑚 + 1) Ramsey ℎ) = ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) |
183 | 182 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (((𝑚 + 1) Ramsey ℎ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) ∈
ℕ0)) |
184 | 181, 183 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛) → ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) ∈
ℕ0))) |
185 | 184 | spcgv 3266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) ∈ V → (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) → (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))):𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 if(𝑘 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑘)) = 𝑛) → ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) ∈
ℕ0))) |
186 | 115, 116,
168, 185 | syl3c 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), (𝑓‘𝑦))))) |
188 | 186, 187 | fmptd 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)) |
190 | 1, 103, 189 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) ∈ (ℕ0
↑𝑚 𝑅) ↔ (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))):𝑅⟶ℕ0)) |
191 | 188, 190 | mpbird 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) |
193 | 192 | ad2antrr 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), (𝑓‘𝑦))))))) |
195 | 194 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑔 = (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) → ((𝑚 Ramsey 𝑔) ∈ ℕ0 ↔ (𝑚 Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) ∈
ℕ0)) |
196 | 195 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) ∈ (ℕ0
↑𝑚 𝑅) → (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 → (𝑚 Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) ∈
ℕ0)) |
197 | 191, 193,
196 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 Ramsey (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))))) ∈
ℕ0) |
198 | 112, 197 | eqeltrd 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) |
200 | 198, 199 | syl 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) ∈
ℕ) |
202 | 100, 201 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑚 + 1) ∈
ℕ) |
203 | 202 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → (𝑚 + 1) ∈ ℕ) |
204 | | equequ1 1939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = 𝑤 → (𝑦 = 𝑥 ↔ 𝑤 = 𝑥)) |
205 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = 𝑤 → (𝑓‘𝑦) = (𝑓‘𝑤)) |
206 | 204, 205 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = 𝑤 → if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)) = if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤))) |
207 | 206 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) = (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤))) |
208 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = 𝑧 → (𝑤 = 𝑥 ↔ 𝑤 = 𝑧)) |
209 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧)) |
210 | 209 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥) − 1) = ((𝑓‘𝑧) − 1)) |
211 | 208, 210 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = 𝑧 → if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤)) = if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤))) |
212 | 211 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑤))) = (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤)))) |
213 | 207, 212 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))) = (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤)))) |
214 | 213 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑧 → ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦)))) = ((𝑚 + 1) Ramsey (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤))))) |
215 | 214 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝑓‘𝑥) − 1), (𝑓‘𝑦))))) = (𝑧 ∈ 𝑅 ↦ ((𝑚 + 1) Ramsey (𝑤 ∈ 𝑅 ↦ if(𝑤 = 𝑧, ((𝑓‘𝑧) − 1), (𝑓‘𝑤))))) |
216 | 203, 103,
104, 215, 188, 198 | ramub1 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) |
218 | 102, 103,
107, 200, 216, 217 | syl32anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1) ∧ 𝑓:𝑅⟶ℕ)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
219 | 218 | expr 641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → (𝑓:𝑅⟶ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
220 | 219 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (𝑓:𝑅⟶ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
221 | 99, 220 | sylbird 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) |
224 | 223 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → (𝑓‘𝑥) ∈
ℕ0) |
225 | | elnn0 11171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓‘𝑥) ∈ ℕ0 ↔ ((𝑓‘𝑥) ∈ ℕ ∨ (𝑓‘𝑥) = 0)) |
226 | 224, 225 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → ((𝑓‘𝑥) ∈ ℕ ∨ (𝑓‘𝑥) = 0)) |
227 | 226 | ord 391 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → (¬ (𝑓‘𝑥) ∈ ℕ → (𝑓‘𝑥) = 0)) |
228 | 202 | ad2antrr 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) |
230 | 228, 229,
223 | 3jca 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) |
232 | 230, 231 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ (𝑥 ∈ 𝑅 ∧ (𝑓‘𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) = 0) |
233 | 232, 86 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ (𝑥 ∈ 𝑅 ∧ (𝑓‘𝑥) = 0)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
234 | 233 | expr 641 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → ((𝑓‘𝑥) = 0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
235 | 227, 234 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) ∧ 𝑥 ∈ 𝑅) → (¬ (𝑓‘𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
236 | 235 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (∃𝑥 ∈ 𝑅 ¬ (𝑓‘𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
237 | 222, 236 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → (¬ ∀𝑥 ∈ 𝑅 (𝑓‘𝑥) ∈ ℕ → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
238 | 221, 237 | pm2.61d 169 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ ∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) ∧ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
239 | 238 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) → ((𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
240 | 239 | alrimdv 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
⊢ (ℎ = 𝑓 → (ℎ‘𝑘) = (𝑓‘𝑘)) |
243 | 242 | sumeq2sdv 14282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = 𝑓 → Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) |
244 | 243 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑓 → (Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1) ↔ Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1))) |
245 | 241, 244 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑓 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) ↔ (𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)))) |
246 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = 𝑓 → ((𝑚 + 1) Ramsey ℎ) = ((𝑚 + 1) Ramsey 𝑓)) |
247 | 246 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑓 → (((𝑚 + 1) Ramsey ℎ) ∈ ℕ0 ↔ ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
248 | 245, 247 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑓 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ ((𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
249 | 248 | cbvalv 2261 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔
∀𝑓((𝑓:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
250 | 240, 249 | syl6ibr 241 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
251 | 250 | anassrs 678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
252 | 251 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ0
→ (((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
(∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
253 | 252 | a2d 29 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
→ ((((𝑅 ∈ Fin
∧ 𝑚 ∈
ℕ0) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = 𝑛) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0)) → (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = (𝑛 + 1)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)))) |
254 | 36, 41, 46, 51, 94, 253 | nn0ind 11348 |
. . . . . . . . . . . . . . 15
⊢
(Σ𝑘 ∈
𝑅 (𝑓‘𝑘) ∈ ℕ0 → (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
255 | 254 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ ∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0) →
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) ∈ ℕ0 →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
256 | 255 | adantrl 748 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) →
(Σ𝑘 ∈ 𝑅 (𝑓‘𝑘) ∈ ℕ0 →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0))) |
257 | 31, 256 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) →
∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈
ℕ0)) |
258 | 243 | biantrud 527 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝑓 → (ℎ:𝑅⟶ℕ0 ↔ (ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)))) |
259 | 258, 241 | bitr3d 269 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝑓 → ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) ↔ 𝑓:𝑅⟶ℕ0)) |
260 | 259, 247 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑓 → (((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) ↔ (𝑓:𝑅⟶ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
261 | 260 | spv 2248 |
. . . . . . . . . . . 12
⊢
(∀ℎ((ℎ:𝑅⟶ℕ0 ∧
Σ𝑘 ∈ 𝑅 (ℎ‘𝑘) = Σ𝑘 ∈ 𝑅 (𝑓‘𝑘)) → ((𝑚 + 1) Ramsey ℎ) ∈ ℕ0) → (𝑓:𝑅⟶ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
262 | 257, 29, 261 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ (𝑓 ∈
(ℕ0 ↑𝑚 𝑅) ∧ ∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0)) → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0) |
263 | 262 | expr 641 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
∧ 𝑓 ∈
(ℕ0 ↑𝑚 𝑅)) → (∀𝑔 ∈ (ℕ0
↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 → ((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
264 | 263 | ralrimdva 2952 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
→ (∀𝑔 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑔) ∈ ℕ0 →
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
265 | 27, 264 | syl5bi 231 |
. . . . . . . 8
⊢ ((𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0)
→ (∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 →
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0)) |
266 | 265 | expcom 450 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝑅 ∈ Fin →
(∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0 →
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
267 | 266 | a2d 29 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ ((𝑅 ∈ Fin
→ ∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑚 Ramsey 𝑓) ∈ ℕ0) → (𝑅 ∈ Fin → ∀𝑓 ∈ (ℕ0
↑𝑚 𝑅)((𝑚 + 1) Ramsey 𝑓) ∈
ℕ0))) |
268 | 8, 12, 16, 20, 24, 267 | nn0ind 11348 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑅 ∈ Fin →
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈
ℕ0)) |
269 | 268 | imp 444 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈
ℕ0) |
270 | | oveq2 6557 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑀 Ramsey 𝑓) = (𝑀 Ramsey 𝐹)) |
271 | 270 | eleq1d 2672 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝑀 Ramsey 𝑓) ∈ ℕ0 ↔ (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
272 | 271 | rspccv 3279 |
. . . 4
⊢
(∀𝑓 ∈
(ℕ0 ↑𝑚 𝑅)(𝑀 Ramsey 𝑓) ∈ ℕ0 → (𝐹 ∈ (ℕ0
↑𝑚 𝑅) → (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
273 | 269, 272 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
(𝐹 ∈
(ℕ0 ↑𝑚 𝑅) → (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
274 | 4, 273 | sylbird 249 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin) →
(𝐹:𝑅⟶ℕ0 → (𝑀 Ramsey 𝐹) ∈
ℕ0)) |
275 | 274 | 3impia 1253 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ Fin ∧
𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈
ℕ0) |