| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vdwlem10.m | . 2
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 2 |  | opeq1 4873 | . . . . . . 7
⊢ (𝑥 = 1 → 〈𝑥, 𝐾〉 = 〈1, 𝐾〉) | 
| 3 | 2 | breq1d 5153 | . . . . . 6
⊢ (𝑥 = 1 → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈1, 𝐾〉 PolyAP 𝑓)) | 
| 4 | 3 | orbi1d 917 | . . . . 5
⊢ (𝑥 = 1 → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 5 | 4 | rexralbidv 3223 | . . . 4
⊢ (𝑥 = 1 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 6 | 5 | imbi2d 340 | . . 3
⊢ (𝑥 = 1 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) | 
| 7 |  | opeq1 4873 | . . . . . . 7
⊢ (𝑥 = 𝑚 → 〈𝑥, 𝐾〉 = 〈𝑚, 𝐾〉) | 
| 8 | 7 | breq1d 5153 | . . . . . 6
⊢ (𝑥 = 𝑚 → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈𝑚, 𝐾〉 PolyAP 𝑓)) | 
| 9 | 8 | orbi1d 917 | . . . . 5
⊢ (𝑥 = 𝑚 → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 10 | 9 | rexralbidv 3223 | . . . 4
⊢ (𝑥 = 𝑚 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 11 | 10 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑚 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) | 
| 12 |  | opeq1 4873 | . . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → 〈𝑥, 𝐾〉 = 〈(𝑚 + 1), 𝐾〉) | 
| 13 | 12 | breq1d 5153 | . . . . . 6
⊢ (𝑥 = (𝑚 + 1) → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓)) | 
| 14 | 13 | orbi1d 917 | . . . . 5
⊢ (𝑥 = (𝑚 + 1) → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 15 | 14 | rexralbidv 3223 | . . . 4
⊢ (𝑥 = (𝑚 + 1) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 16 | 15 | imbi2d 340 | . . 3
⊢ (𝑥 = (𝑚 + 1) → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) | 
| 17 |  | opeq1 4873 | . . . . . . 7
⊢ (𝑥 = 𝑀 → 〈𝑥, 𝐾〉 = 〈𝑀, 𝐾〉) | 
| 18 | 17 | breq1d 5153 | . . . . . 6
⊢ (𝑥 = 𝑀 → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈𝑀, 𝐾〉 PolyAP 𝑓)) | 
| 19 | 18 | orbi1d 917 | . . . . 5
⊢ (𝑥 = 𝑀 → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 20 | 19 | rexralbidv 3223 | . . . 4
⊢ (𝑥 = 𝑀 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 21 | 20 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑀 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) | 
| 22 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑠 = 𝑅 → (𝑠 ↑m (1...𝑛)) = (𝑅 ↑m (1...𝑛))) | 
| 23 | 22 | raleqdv 3326 | . . . . . . 7
⊢ (𝑠 = 𝑅 → (∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))𝐾 MonoAP 𝑓)) | 
| 24 | 23 | rexbidv 3179 | . . . . . 6
⊢ (𝑠 = 𝑅 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))𝐾 MonoAP 𝑓)) | 
| 25 |  | vdwlem9.s | . . . . . 6
⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓) | 
| 26 |  | vdw.r | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Fin) | 
| 27 | 24, 25, 26 | rspcdva 3623 | . . . . 5
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))𝐾 MonoAP 𝑓) | 
| 28 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑛 = 𝑤 → (1...𝑛) = (1...𝑤)) | 
| 29 | 28 | oveq2d 7447 | . . . . . . 7
⊢ (𝑛 = 𝑤 → (𝑅 ↑m (1...𝑛)) = (𝑅 ↑m (1...𝑤))) | 
| 30 | 29 | raleqdv 3326 | . . . . . 6
⊢ (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅 ↑m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑓)) | 
| 31 | 30 | cbvrexvw 3238 | . . . . 5
⊢
(∃𝑛 ∈
ℕ ∀𝑓 ∈
(𝑅 ↑m
(1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑓) | 
| 32 | 27, 31 | sylib 218 | . . . 4
⊢ (𝜑 → ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑓) | 
| 33 |  | breq2 5147 | . . . . . . 7
⊢ (𝑓 = 𝑔 → (𝐾 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝑔)) | 
| 34 | 33 | cbvralvw 3237 | . . . . . 6
⊢
(∀𝑓 ∈
(𝑅 ↑m
(1...𝑤))𝐾 MonoAP 𝑓 ↔ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑔) | 
| 35 |  | 2nn 12339 | . . . . . . . 8
⊢ 2 ∈
ℕ | 
| 36 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → 𝑤 ∈ ℕ) | 
| 37 |  | nnmulcl 12290 | . . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑤
∈ ℕ) → (2 · 𝑤) ∈ ℕ) | 
| 38 | 35, 36, 37 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (2 · 𝑤) ∈
ℕ) | 
| 39 | 26 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → 𝑅 ∈ Fin) | 
| 40 |  | ovex 7464 | . . . . . . . . . . 11
⊢ (1...(2
· 𝑤)) ∈
V | 
| 41 |  | elmapg 8879 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Fin ∧ (1...(2
· 𝑤)) ∈ V)
→ (𝑓 ∈ (𝑅 ↑m (1...(2
· 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅)) | 
| 42 | 39, 40, 41 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (𝑓 ∈ (𝑅 ↑m (1...(2 · 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅)) | 
| 43 | 42 | biimpa 476 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅 ↑m (1...(2 · 𝑤)))) → 𝑓:(1...(2 · 𝑤))⟶𝑅) | 
| 44 |  | simplr 769 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑓:(1...(2 · 𝑤))⟶𝑅) | 
| 45 |  | elfznn 13593 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1...𝑤) → 𝑦 ∈ ℕ) | 
| 46 | 45 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℕ) | 
| 47 | 46 | nnred 12281 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℝ) | 
| 48 |  | simpllr 776 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℕ) | 
| 49 | 48 | nnred 12281 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℝ) | 
| 50 |  | elfzle2 13568 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1...𝑤) → 𝑦 ≤ 𝑤) | 
| 51 | 50 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ≤ 𝑤) | 
| 52 | 47, 49, 49, 51 | leadd1dd 11877 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (𝑤 + 𝑤)) | 
| 53 | 48 | nncnd 12282 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℂ) | 
| 54 | 53 | 2timesd 12509 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) = (𝑤 + 𝑤)) | 
| 55 | 52, 54 | breqtrrd 5171 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (2 · 𝑤)) | 
| 56 | 46, 48 | nnaddcld 12318 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ ℕ) | 
| 57 |  | nnuz 12921 | . . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) | 
| 58 | 56, 57 | eleqtrdi 2851 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈
(ℤ≥‘1)) | 
| 59 | 38 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℕ) | 
| 60 | 59 | nnzd 12640 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℤ) | 
| 61 |  | elfz5 13556 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 + 𝑤) ∈ (ℤ≥‘1)
∧ (2 · 𝑤) ∈
ℤ) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤))) | 
| 62 | 58, 60, 61 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤))) | 
| 63 | 55, 62 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (1...(2 · 𝑤))) | 
| 64 | 44, 63 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑓‘(𝑦 + 𝑤)) ∈ 𝑅) | 
| 65 |  | fvoveq1 7454 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑓‘(𝑥 + 𝑤)) = (𝑓‘(𝑦 + 𝑤))) | 
| 66 | 65 | cbvmptv 5255 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) = (𝑦 ∈ (1...𝑤) ↦ (𝑓‘(𝑦 + 𝑤))) | 
| 67 | 64, 66 | fmptd 7134 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅) | 
| 68 |  | ovex 7464 | . . . . . . . . . . . . . 14
⊢
(1...𝑤) ∈
V | 
| 69 |  | elmapg 8879 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ V) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅)) | 
| 70 | 39, 68, 69 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅)) | 
| 71 | 70 | biimpar 477 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑m (1...𝑤))) | 
| 72 | 67, 71 | syldan 591 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑m (1...𝑤))) | 
| 73 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑔 = (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (𝐾 MonoAP 𝑔 ↔ 𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))))) | 
| 74 | 73 | rspcv 3618 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑m (1...𝑤)) → (∀𝑔 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑔 → 𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))))) | 
| 75 | 72, 74 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑔 → 𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))))) | 
| 76 |  | 2nn0 12543 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 | 
| 77 |  | vdwlem9.k | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) | 
| 78 | 77 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈
(ℤ≥‘2)) | 
| 79 |  | eluznn0 12959 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℕ0 ∧ 𝐾 ∈ (ℤ≥‘2))
→ 𝐾 ∈
ℕ0) | 
| 80 | 76, 78, 79 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈
ℕ0) | 
| 81 | 68, 80, 67 | vdwmc 17016 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) | 
| 82 | 39 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑅 ∈ Fin) | 
| 83 | 78 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝐾 ∈
(ℤ≥‘2)) | 
| 84 |  | simpllr 776 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑤 ∈ ℕ) | 
| 85 |  | simplr 769 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑓:(1...(2 · 𝑤))⟶𝑅) | 
| 86 |  | vex 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V | 
| 87 |  | simprll 779 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑎 ∈ ℕ) | 
| 88 |  | simprlr 780 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑑 ∈ ℕ) | 
| 89 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐})) | 
| 90 | 82, 83, 84, 85, 86, 87, 88, 89, 66 | vdwlem8 17026 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 〈1, 𝐾〉 PolyAP 𝑓) | 
| 91 | 90 | orcd 874 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) | 
| 92 | 91 | expr 456 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 93 | 92 | rexlimdvva 3213 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 94 | 93 | exlimdv 1933 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 95 | 81, 94 | sylbid 240 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 96 | 75, 95 | syld 47 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑔 → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 97 | 43, 96 | syldan 591 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅 ↑m (1...(2 · 𝑤)))) → (∀𝑔 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑔 → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 98 | 97 | ralrimdva 3154 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑔 → ∀𝑓 ∈ (𝑅 ↑m (1...(2 · 𝑤)))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 99 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑛 = (2 · 𝑤) → (1...𝑛) = (1...(2 · 𝑤))) | 
| 100 | 99 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑛 = (2 · 𝑤) → (𝑅 ↑m (1...𝑛)) = (𝑅 ↑m (1...(2 · 𝑤)))) | 
| 101 | 100 | raleqdv 3326 | . . . . . . . 8
⊢ (𝑛 = (2 · 𝑤) → (∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅 ↑m (1...(2 · 𝑤)))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 102 | 101 | rspcev 3622 | . . . . . . 7
⊢ (((2
· 𝑤) ∈ ℕ
∧ ∀𝑓 ∈
(𝑅 ↑m
(1...(2 · 𝑤)))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) | 
| 103 | 38, 98, 102 | syl6an 684 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑔 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 104 | 34, 103 | biimtrid 242 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (∀𝑓 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 105 | 104 | rexlimdva 3155 | . . . 4
⊢ (𝜑 → (∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 106 | 32, 105 | mpd 15 | . . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) | 
| 107 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (〈𝑚, 𝐾〉 PolyAP 𝑓 ↔ 〈𝑚, 𝐾〉 PolyAP 𝑔)) | 
| 108 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP 𝑔)) | 
| 109 | 107, 108 | orbi12d 919 | . . . . . . . . 9
⊢ (𝑓 = 𝑔 → ((〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) | 
| 110 | 109 | cbvralvw 3237 | . . . . . . . 8
⊢
(∀𝑓 ∈
(𝑅 ↑m
(1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) | 
| 111 | 29 | raleqdv 3326 | . . . . . . . 8
⊢ (𝑛 = 𝑤 → (∀𝑔 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) | 
| 112 | 110, 111 | bitrid 283 | . . . . . . 7
⊢ (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) | 
| 113 | 112 | cbvrexvw 3238 | . . . . . 6
⊢
(∃𝑛 ∈
ℕ ∀𝑓 ∈
(𝑅 ↑m
(1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) | 
| 114 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑣 → (1...𝑛) = (1...𝑣)) | 
| 115 | 114 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑣 → (𝑠 ↑m (1...𝑛)) = (𝑠 ↑m (1...𝑣))) | 
| 116 | 115 | raleqdv 3326 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑣 → (∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑠 ↑m (1...𝑣))𝐾 MonoAP 𝑓)) | 
| 117 | 116 | cbvrexvw 3238 | . . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕ ∀𝑓 ∈
(𝑠 ↑m
(1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑣))𝐾 MonoAP 𝑓) | 
| 118 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑠 = (𝑅 ↑m (1...𝑤)) → (𝑠 ↑m (1...𝑣)) = ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))) | 
| 119 | 118 | raleqdv 3326 | . . . . . . . . . . 11
⊢ (𝑠 = (𝑅 ↑m (1...𝑤)) → (∀𝑓 ∈ (𝑠 ↑m (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) | 
| 120 | 119 | rexbidv 3179 | . . . . . . . . . 10
⊢ (𝑠 = (𝑅 ↑m (1...𝑤)) → (∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) | 
| 121 | 117, 120 | bitrid 283 | . . . . . . . . 9
⊢ (𝑠 = (𝑅 ↑m (1...𝑤)) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) | 
| 122 | 25 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓) | 
| 123 | 26 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → 𝑅 ∈ Fin) | 
| 124 |  | fzfi 14013 | . . . . . . . . . 10
⊢
(1...𝑤) ∈
Fin | 
| 125 |  | mapfi 9388 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ Fin) → (𝑅 ↑m (1...𝑤)) ∈ Fin) | 
| 126 | 123, 124,
125 | sylancl 586 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → (𝑅 ↑m (1...𝑤)) ∈ Fin) | 
| 127 | 121, 122,
126 | rspcdva 3623 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓) | 
| 128 |  | simprll 779 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → 𝑤 ∈ ℕ) | 
| 129 |  | simprrl 781 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → 𝑣 ∈ ℕ) | 
| 130 |  | nnmulcl 12290 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℕ ∧ 𝑣
∈ ℕ) → (2 · 𝑣) ∈ ℕ) | 
| 131 | 35, 130 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑣 ∈ ℕ → (2
· 𝑣) ∈
ℕ) | 
| 132 |  | nnmulcl 12290 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ ∧ (2
· 𝑣) ∈ ℕ)
→ (𝑤 · (2
· 𝑣)) ∈
ℕ) | 
| 133 | 131, 132 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ ∧ 𝑣 ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈
ℕ) | 
| 134 | 128, 129,
133 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → (𝑤 · (2 · 𝑣)) ∈ ℕ) | 
| 135 |  | simp1l 1198 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → 𝜑) | 
| 136 | 135, 26 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → 𝑅 ∈ Fin) | 
| 137 | 135, 77 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → 𝐾 ∈
(ℤ≥‘2)) | 
| 138 | 135, 25 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓) | 
| 139 |  | simp1r 1199 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → 𝑚 ∈ ℕ) | 
| 140 |  | simp2ll 1241 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → 𝑤 ∈ ℕ) | 
| 141 |  | simp2lr 1242 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) | 
| 142 |  | breq2 5147 | . . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑘 → (〈𝑚, 𝐾〉 PolyAP 𝑔 ↔ 〈𝑚, 𝐾〉 PolyAP 𝑘)) | 
| 143 |  | breq2 5147 | . . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑘 → ((𝐾 + 1) MonoAP 𝑔 ↔ (𝐾 + 1) MonoAP 𝑘)) | 
| 144 | 142, 143 | orbi12d 919 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑘 → ((〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ (〈𝑚, 𝐾〉 PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘))) | 
| 145 | 144 | cbvralvw 3237 | . . . . . . . . . . . . . 14
⊢
(∀𝑔 ∈
(𝑅 ↑m
(1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑘 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘)) | 
| 146 | 141, 145 | sylib 218 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑘 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘)) | 
| 147 |  | simp2rl 1243 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → 𝑣 ∈ ℕ) | 
| 148 |  | simp2rr 1244 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓) | 
| 149 |  | simp3 1139 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) | 
| 150 |  | ovex 7464 | . . . . . . . . . . . . . . 15
⊢
(1...(𝑤 · (2
· 𝑣))) ∈
V | 
| 151 |  | elmapg 8879 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Fin ∧ (1...(𝑤 · (2 · 𝑣))) ∈ V) → (ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣)))) ↔ ℎ:(1...(𝑤 · (2 · 𝑣)))⟶𝑅)) | 
| 152 | 136, 150,
151 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → (ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣)))) ↔ ℎ:(1...(𝑤 · (2 · 𝑣)))⟶𝑅)) | 
| 153 | 149, 152 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → ℎ:(1...(𝑤 · (2 · 𝑣)))⟶𝑅) | 
| 154 |  | fvoveq1 7454 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) | 
| 155 | 154 | cbvmptv 5255 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1...𝑤) ↦ (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) | 
| 156 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝑥 − 1) = (𝑧 − 1)) | 
| 157 | 156 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → ((𝑥 − 1) + 𝑣) = ((𝑧 − 1) + 𝑣)) | 
| 158 | 157 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (𝑤 · ((𝑥 − 1) + 𝑣)) = (𝑤 · ((𝑧 − 1) + 𝑣))) | 
| 159 | 158 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))) = (𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))) | 
| 160 | 159 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))) | 
| 161 | 160 | mpteq2dv 5244 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))) | 
| 162 | 155, 161 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑦 ∈ (1...𝑤) ↦ (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))) | 
| 163 | 162 | cbvmptv 5255 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑣) ↦ (𝑦 ∈ (1...𝑤) ↦ (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))))) = (𝑧 ∈ (1...𝑣) ↦ (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))) | 
| 164 | 136, 137,
138, 139, 140, 146, 147, 148, 153, 163 | vdwlem9 17027 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) → (〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) | 
| 165 | 164 | 3expia 1122 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → (ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣)))) → (〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ))) | 
| 166 | 165 | ralrimiv 3145 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ∀ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) | 
| 167 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (1...𝑛) = (1...(𝑤 · (2 · 𝑣)))) | 
| 168 | 167 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (𝑅 ↑m (1...𝑛)) = (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))) | 
| 169 | 168 | raleqdv 3326 | . . . . . . . . . . . 12
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 170 |  | breq2 5147 | . . . . . . . . . . . . . 14
⊢ (𝑓 = ℎ → (〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ↔ 〈(𝑚 + 1), 𝐾〉 PolyAP ℎ)) | 
| 171 |  | breq2 5147 | . . . . . . . . . . . . . 14
⊢ (𝑓 = ℎ → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP ℎ)) | 
| 172 | 170, 171 | orbi12d 919 | . . . . . . . . . . . . 13
⊢ (𝑓 = ℎ → ((〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ))) | 
| 173 | 172 | cbvralvw 3237 | . . . . . . . . . . . 12
⊢
(∀𝑓 ∈
(𝑅 ↑m
(1...(𝑤 · (2
· 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) | 
| 174 | 169, 173 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ))) | 
| 175 | 174 | rspcev 3622 | . . . . . . . . . 10
⊢ (((𝑤 · (2 · 𝑣)) ∈ ℕ ∧
∀ℎ ∈ (𝑅 ↑m (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) | 
| 176 | 134, 166,
175 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) | 
| 177 | 176 | anassrs 467 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) | 
| 178 | 127, 177 | rexlimddv 3161 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) | 
| 179 | 178 | rexlimdvaa 3156 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅 ↑m (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 180 | 113, 179 | biimtrid 242 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 181 | 180 | expcom 413 | . . . 4
⊢ (𝑚 ∈ ℕ → (𝜑 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) | 
| 182 | 181 | a2d 29 | . . 3
⊢ (𝑚 ∈ ℕ → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) | 
| 183 | 6, 11, 16, 21, 106, 182 | nnind 12284 | . 2
⊢ (𝑀 ∈ ℕ → (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) | 
| 184 | 1, 183 | mpcom 38 | 1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |