| Step | Hyp | Ref
| Expression |
| 1 | | ovex 7464 |
. . 3
⊢
(1...𝑊) ∈
V |
| 2 | | 2nn0 12543 |
. . . 4
⊢ 2 ∈
ℕ0 |
| 3 | | vdwlem7.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) |
| 4 | | eluznn0 12959 |
. . . 4
⊢ ((2
∈ ℕ0 ∧ 𝐾 ∈ (ℤ≥‘2))
→ 𝐾 ∈
ℕ0) |
| 5 | 2, 3, 4 | sylancr 587 |
. . 3
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 6 | | vdwlem7.g |
. . 3
⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅) |
| 7 | | vdwlem7.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 8 | | eqid 2737 |
. . 3
⊢
(1...𝑀) = (1...𝑀) |
| 9 | 1, 5, 6, 7, 8 | vdwpc 17018 |
. 2
⊢ (𝜑 → (〈𝑀, 𝐾〉 PolyAP 𝐺 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑀))(∀𝑖 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀))) |
| 10 | | vdwlem3.v |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ ℕ) |
| 11 | 10 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑉 ∈ ℕ) |
| 12 | | vdwlem3.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ ℕ) |
| 13 | 12 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑊 ∈ ℕ) |
| 14 | | vdwlem4.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Fin) |
| 15 | 14 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑅 ∈ Fin) |
| 16 | | vdwlem4.h |
. . . . . 6
⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
| 17 | 16 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
| 18 | | vdwlem4.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))))) |
| 19 | 7 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑀 ∈ ℕ) |
| 20 | 6 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐺:(1...𝑊)⟶𝑅) |
| 21 | 3 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐾 ∈
(ℤ≥‘2)) |
| 22 | | vdwlem7.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℕ) |
| 23 | 22 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐴 ∈ ℕ) |
| 24 | | vdwlem7.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℕ) |
| 25 | 24 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐷 ∈ ℕ) |
| 26 | | vdwlem7.s |
. . . . . 6
⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺})) |
| 27 | 26 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺})) |
| 28 | | simplrl 777 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑎 ∈ ℕ) |
| 29 | | simplrr 778 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑑 ∈ (ℕ ↑m
(1...𝑀))) |
| 30 | | nnex 12272 |
. . . . . . 7
⊢ ℕ
∈ V |
| 31 | | ovex 7464 |
. . . . . . 7
⊢
(1...𝑀) ∈
V |
| 32 | 30, 31 | elmap 8911 |
. . . . . 6
⊢ (𝑑 ∈ (ℕ
↑m (1...𝑀))
↔ 𝑑:(1...𝑀)⟶ℕ) |
| 33 | 29, 32 | sylib 218 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑑:(1...𝑀)⟶ℕ) |
| 34 | | simprl 771 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → ∀𝑖 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))})) |
| 35 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (𝑑‘𝑖) = (𝑑‘𝑘)) |
| 36 | 35 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑎 + (𝑑‘𝑖)) = (𝑎 + (𝑑‘𝑘))) |
| 37 | 36, 35 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘))) |
| 38 | 36 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (𝐺‘(𝑎 + (𝑑‘𝑖))) = (𝐺‘(𝑎 + (𝑑‘𝑘)))) |
| 39 | 38 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → {(𝐺‘(𝑎 + (𝑑‘𝑖)))} = {(𝐺‘(𝑎 + (𝑑‘𝑘)))}) |
| 40 | 39 | imaeq2d 6078 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) = (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))})) |
| 41 | 37, 40 | sseq12d 4017 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ↔ ((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))}))) |
| 42 | 41 | cbvralvw 3237 |
. . . . . 6
⊢
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑘 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))})) |
| 43 | 34, 42 | sylib 218 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → ∀𝑘 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))})) |
| 44 | 38 | cbvmptv 5255 |
. . . . 5
⊢ (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖)))) = (𝑘 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑘)))) |
| 45 | | simprr 773 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀) |
| 46 | | eqid 2737 |
. . . . 5
⊢ (𝑎 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) = (𝑎 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) |
| 47 | | eqid 2737 |
. . . . 5
⊢ (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝑑‘𝑗)) + (𝑊 · 𝐷))) = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝑑‘𝑗)) + (𝑊 · 𝐷))) |
| 48 | 11, 13, 15, 17, 18, 19, 20, 21, 23, 25, 27, 28, 33, 43, 44, 45, 46, 47 | vdwlem6 17024 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺)) |
| 49 | 48 | ex 412 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) →
((∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))) |
| 50 | 49 | rexlimdvva 3213 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑀))(∀𝑖 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))) |
| 51 | 9, 50 | sylbid 240 |
1
⊢ (𝜑 → (〈𝑀, 𝐾〉 PolyAP 𝐺 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))) |