Step | Hyp | Ref
| Expression |
1 | | vdwlem10.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | | opeq1 4402 |
. . . . . . 7
⊢ (𝑥 = 1 → 〈𝑥, 𝐾〉 = 〈1, 𝐾〉) |
3 | 2 | breq1d 4663 |
. . . . . 6
⊢ (𝑥 = 1 → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈1, 𝐾〉 PolyAP 𝑓)) |
4 | 3 | orbi1d 739 |
. . . . 5
⊢ (𝑥 = 1 → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
5 | 4 | rexralbidv 3058 |
. . . 4
⊢ (𝑥 = 1 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
6 | 5 | imbi2d 330 |
. . 3
⊢ (𝑥 = 1 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) |
7 | | opeq1 4402 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → 〈𝑥, 𝐾〉 = 〈𝑚, 𝐾〉) |
8 | 7 | breq1d 4663 |
. . . . . 6
⊢ (𝑥 = 𝑚 → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈𝑚, 𝐾〉 PolyAP 𝑓)) |
9 | 8 | orbi1d 739 |
. . . . 5
⊢ (𝑥 = 𝑚 → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
10 | 9 | rexralbidv 3058 |
. . . 4
⊢ (𝑥 = 𝑚 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
11 | 10 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑚 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) |
12 | | opeq1 4402 |
. . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → 〈𝑥, 𝐾〉 = 〈(𝑚 + 1), 𝐾〉) |
13 | 12 | breq1d 4663 |
. . . . . 6
⊢ (𝑥 = (𝑚 + 1) → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓)) |
14 | 13 | orbi1d 739 |
. . . . 5
⊢ (𝑥 = (𝑚 + 1) → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
15 | 14 | rexralbidv 3058 |
. . . 4
⊢ (𝑥 = (𝑚 + 1) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
16 | 15 | imbi2d 330 |
. . 3
⊢ (𝑥 = (𝑚 + 1) → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) |
17 | | opeq1 4402 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → 〈𝑥, 𝐾〉 = 〈𝑀, 𝐾〉) |
18 | 17 | breq1d 4663 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (〈𝑥, 𝐾〉 PolyAP 𝑓 ↔ 〈𝑀, 𝐾〉 PolyAP 𝑓)) |
19 | 18 | orbi1d 739 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
20 | 19 | rexralbidv 3058 |
. . . 4
⊢ (𝑥 = 𝑀 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
21 | 20 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑀 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑥, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) |
22 | | vdw.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Fin) |
23 | | vdwlem9.s |
. . . . . 6
⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓) |
24 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑠 = 𝑅 → (𝑠 ↑𝑚 (1...𝑛)) = (𝑅 ↑𝑚 (1...𝑛))) |
25 | 24 | raleqdv 3144 |
. . . . . . . 8
⊢ (𝑠 = 𝑅 → (∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓)) |
26 | 25 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑠 = 𝑅 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓)) |
27 | 26 | rspcv 3305 |
. . . . . 6
⊢ (𝑅 ∈ Fin →
(∀𝑠 ∈ Fin
∃𝑛 ∈ ℕ
∀𝑓 ∈ (𝑠 ↑𝑚
(1...𝑛))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓)) |
28 | 22, 23, 27 | sylc 65 |
. . . . 5
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓) |
29 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑛 = 𝑤 → (1...𝑛) = (1...𝑤)) |
30 | 29 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑛 = 𝑤 → (𝑅 ↑𝑚 (1...𝑛)) = (𝑅 ↑𝑚 (1...𝑤))) |
31 | 30 | raleqdv 3144 |
. . . . . 6
⊢ (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑓)) |
32 | 31 | cbvrexv 3172 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ ∀𝑓 ∈
(𝑅
↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑓) |
33 | 28, 32 | sylib 208 |
. . . 4
⊢ (𝜑 → ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑓) |
34 | | breq2 4657 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (𝐾 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝑔)) |
35 | 34 | cbvralv 3171 |
. . . . . 6
⊢
(∀𝑓 ∈
(𝑅
↑𝑚 (1...𝑤))𝐾 MonoAP 𝑓 ↔ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑔) |
36 | | 2nn 11185 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
37 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → 𝑤 ∈ ℕ) |
38 | | nnmulcl 11043 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑤
∈ ℕ) → (2 · 𝑤) ∈ ℕ) |
39 | 36, 37, 38 | sylancr 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (2 · 𝑤) ∈
ℕ) |
40 | 22 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → 𝑅 ∈ Fin) |
41 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (1...(2
· 𝑤)) ∈
V |
42 | | elmapg 7870 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Fin ∧ (1...(2
· 𝑤)) ∈ V)
→ (𝑓 ∈ (𝑅 ↑𝑚
(1...(2 · 𝑤)))
↔ 𝑓:(1...(2 ·
𝑤))⟶𝑅)) |
43 | 40, 41, 42 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (𝑓 ∈ (𝑅 ↑𝑚 (1...(2 ·
𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅)) |
44 | 43 | biimpa 501 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (1...(2 ·
𝑤)))) → 𝑓:(1...(2 · 𝑤))⟶𝑅) |
45 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑓:(1...(2 · 𝑤))⟶𝑅) |
46 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1...𝑤) → 𝑦 ∈ ℕ) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℕ) |
48 | 47 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℝ) |
49 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℕ) |
50 | 49 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℝ) |
51 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1...𝑤) → 𝑦 ≤ 𝑤) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ≤ 𝑤) |
53 | 48, 50, 50, 52 | leadd1dd 10641 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (𝑤 + 𝑤)) |
54 | 49 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℂ) |
55 | 54 | 2timesd 11275 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) = (𝑤 + 𝑤)) |
56 | 53, 55 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (2 · 𝑤)) |
57 | 47, 49 | nnaddcld 11067 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ ℕ) |
58 | | nnuz 11723 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) |
59 | 57, 58 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈
(ℤ≥‘1)) |
60 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℕ) |
61 | 60 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℤ) |
62 | | elfz5 12334 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 + 𝑤) ∈ (ℤ≥‘1)
∧ (2 · 𝑤) ∈
ℤ) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤))) |
63 | 59, 61, 62 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤))) |
64 | 56, 63 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (1...(2 · 𝑤))) |
65 | 45, 64 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑓‘(𝑦 + 𝑤)) ∈ 𝑅) |
66 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑥 + 𝑤) = (𝑦 + 𝑤)) |
67 | 66 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑓‘(𝑥 + 𝑤)) = (𝑓‘(𝑦 + 𝑤))) |
68 | 67 | cbvmptv 4750 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) = (𝑦 ∈ (1...𝑤) ↦ (𝑓‘(𝑦 + 𝑤))) |
69 | 65, 68 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅) |
70 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢
(1...𝑤) ∈
V |
71 | | elmapg 7870 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ V) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑𝑚 (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅)) |
72 | 40, 70, 71 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑𝑚 (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅)) |
73 | 72 | biimpar 502 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑𝑚 (1...𝑤))) |
74 | 69, 73 | syldan 487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑𝑚 (1...𝑤))) |
75 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (𝐾 MonoAP 𝑔 ↔ 𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))))) |
76 | 75 | rspcv 3305 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅 ↑𝑚 (1...𝑤)) → (∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑔 → 𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))))) |
77 | 74, 76 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑔 → 𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))))) |
78 | | 2nn0 11309 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
79 | | vdwlem9.k |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) |
80 | 79 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈
(ℤ≥‘2)) |
81 | | eluznn0 11757 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ0 ∧ 𝐾 ∈ (ℤ≥‘2))
→ 𝐾 ∈
ℕ0) |
82 | 78, 80, 81 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈
ℕ0) |
83 | 70, 82, 69 | vdwmc 15682 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) |
84 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑅 ∈ Fin) |
85 | 80 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝐾 ∈
(ℤ≥‘2)) |
86 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑤 ∈ ℕ) |
87 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑓:(1...(2 · 𝑤))⟶𝑅) |
88 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V |
89 | | simprll 802 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑎 ∈ ℕ) |
90 | | simprlr 803 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑑 ∈ ℕ) |
91 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐})) |
92 | 84, 85, 86, 87, 88, 89, 90, 91, 68 | vdwlem8 15692 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 〈1, 𝐾〉 PolyAP 𝑓) |
93 | 92 | orcd 407 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |
94 | 93 | expr 643 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
95 | 94 | rexlimdvva 3038 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
96 | 95 | exlimdv 1861 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡(𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
97 | 83, 96 | sylbid 230 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
98 | 77, 97 | syld 47 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑔 → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
99 | 44, 98 | syldan 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅 ↑𝑚 (1...(2 ·
𝑤)))) → (∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑔 → (〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
100 | 99 | ralrimdva 2969 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑔 → ∀𝑓 ∈ (𝑅 ↑𝑚 (1...(2 ·
𝑤)))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
101 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑛 = (2 · 𝑤) → (1...𝑛) = (1...(2 · 𝑤))) |
102 | 101 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑛 = (2 · 𝑤) → (𝑅 ↑𝑚 (1...𝑛)) = (𝑅 ↑𝑚 (1...(2 ·
𝑤)))) |
103 | 102 | raleqdv 3144 |
. . . . . . . 8
⊢ (𝑛 = (2 · 𝑤) → (∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...(2 ·
𝑤)))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
104 | 103 | rspcev 3309 |
. . . . . . 7
⊢ (((2
· 𝑤) ∈ ℕ
∧ ∀𝑓 ∈
(𝑅
↑𝑚 (1...(2 · 𝑤)))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |
105 | 39, 100, 104 | syl6an 568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑔 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
106 | 35, 105 | syl5bi 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ) → (∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
107 | 106 | rexlimdva 3031 |
. . . 4
⊢ (𝜑 → (∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
108 | 33, 107 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈1, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |
109 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (〈𝑚, 𝐾〉 PolyAP 𝑓 ↔ 〈𝑚, 𝐾〉 PolyAP 𝑔)) |
110 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP 𝑔)) |
111 | 109, 110 | orbi12d 746 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ((〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) |
112 | 111 | cbvralv 3171 |
. . . . . . . 8
⊢
(∀𝑓 ∈
(𝑅
↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) |
113 | 30 | raleqdv 3144 |
. . . . . . . 8
⊢ (𝑛 = 𝑤 → (∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) |
114 | 112, 113 | syl5bb 272 |
. . . . . . 7
⊢ (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) |
115 | 114 | cbvrexv 3172 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ∀𝑓 ∈
(𝑅
↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) |
116 | 22 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → 𝑅 ∈ Fin) |
117 | | fzfi 12771 |
. . . . . . . . . 10
⊢
(1...𝑤) ∈
Fin |
118 | | mapfi 8262 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ Fin) → (𝑅 ↑𝑚
(1...𝑤)) ∈
Fin) |
119 | 116, 117,
118 | sylancl 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → (𝑅 ↑𝑚 (1...𝑤)) ∈ Fin) |
120 | 23 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓) |
121 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑣 → (1...𝑛) = (1...𝑣)) |
122 | 121 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑣 → (𝑠 ↑𝑚 (1...𝑛)) = (𝑠 ↑𝑚 (1...𝑣))) |
123 | 122 | raleqdv 3144 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑣 → (∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑣))𝐾 MonoAP 𝑓)) |
124 | 123 | cbvrexv 3172 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ ∀𝑓 ∈
(𝑠
↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑣))𝐾 MonoAP 𝑓) |
125 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑅 ↑𝑚 (1...𝑤)) → (𝑠 ↑𝑚 (1...𝑣)) = ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))) |
126 | 125 | raleqdv 3144 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑅 ↑𝑚 (1...𝑤)) → (∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) |
127 | 126 | rexbidv 3052 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝑅 ↑𝑚 (1...𝑤)) → (∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) |
128 | 124, 127 | syl5bb 272 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑅 ↑𝑚 (1...𝑤)) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) |
129 | 128 | rspcv 3305 |
. . . . . . . . 9
⊢ ((𝑅 ↑𝑚
(1...𝑤)) ∈ Fin →
(∀𝑠 ∈ Fin
∃𝑛 ∈ ℕ
∀𝑓 ∈ (𝑠 ↑𝑚
(1...𝑛))𝐾 MonoAP 𝑓 → ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) |
130 | 119, 120,
129 | sylc 65 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓) |
131 | | simprll 802 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓))) → 𝑤 ∈ ℕ) |
132 | | simprrl 804 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓))) → 𝑣 ∈ ℕ) |
133 | | nnmulcl 11043 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ ∧ 𝑣
∈ ℕ) → (2 · 𝑣) ∈ ℕ) |
134 | 36, 133 | mpan 706 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ℕ → (2
· 𝑣) ∈
ℕ) |
135 | | nnmulcl 11043 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ ∧ (2
· 𝑣) ∈ ℕ)
→ (𝑤 · (2
· 𝑣)) ∈
ℕ) |
136 | 134, 135 | sylan2 491 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ ∧ 𝑣 ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈
ℕ) |
137 | 131, 132,
136 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓))) → (𝑤 · (2 · 𝑣)) ∈ ℕ) |
138 | | simp1l 1085 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → 𝜑) |
139 | 138, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → 𝑅 ∈ Fin) |
140 | 138, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → 𝐾 ∈
(ℤ≥‘2)) |
141 | 138, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑𝑚 (1...𝑛))𝐾 MonoAP 𝑓) |
142 | | simp1r 1086 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → 𝑚 ∈ ℕ) |
143 | | simp2ll 1128 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → 𝑤 ∈ ℕ) |
144 | | simp2lr 1129 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) |
145 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑘 → (〈𝑚, 𝐾〉 PolyAP 𝑔 ↔ 〈𝑚, 𝐾〉 PolyAP 𝑘)) |
146 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑘 → ((𝐾 + 1) MonoAP 𝑔 ↔ (𝐾 + 1) MonoAP 𝑘)) |
147 | 145, 146 | orbi12d 746 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑘 → ((〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ (〈𝑚, 𝐾〉 PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘))) |
148 | 147 | cbvralv 3171 |
. . . . . . . . . . . . . 14
⊢
(∀𝑔 ∈
(𝑅
↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑘 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘)) |
149 | 144, 148 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → ∀𝑘 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘)) |
150 | | simp2rl 1130 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → 𝑣 ∈ ℕ) |
151 | | simp2rr 1131 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓) |
152 | | simp3 1063 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) |
153 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢
(1...(𝑤 · (2
· 𝑣))) ∈
V |
154 | | elmapg 7870 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Fin ∧ (1...(𝑤 · (2 · 𝑣))) ∈ V) → (ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣)))) ↔ ℎ:(1...(𝑤 · (2 · 𝑣)))⟶𝑅)) |
155 | 139, 153,
154 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → (ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣)))) ↔ ℎ:(1...(𝑤 · (2 · 𝑣)))⟶𝑅)) |
156 | 152, 155 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → ℎ:(1...(𝑤 · (2 · 𝑣)))⟶𝑅) |
157 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑢 → (𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))) = (𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))) |
158 | 157 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) |
159 | 158 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1...𝑤) ↦ (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) |
160 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝑥 − 1) = (𝑧 − 1)) |
161 | 160 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → ((𝑥 − 1) + 𝑣) = ((𝑧 − 1) + 𝑣)) |
162 | 161 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (𝑤 · ((𝑥 − 1) + 𝑣)) = (𝑤 · ((𝑧 − 1) + 𝑣))) |
163 | 162 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))) = (𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))) |
164 | 163 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))) |
165 | 164 | mpteq2dv 4745 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))) |
166 | 159, 165 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑦 ∈ (1...𝑤) ↦ (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))) |
167 | 166 | cbvmptv 4750 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑣) ↦ (𝑦 ∈ (1...𝑤) ↦ (ℎ‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))))) = (𝑧 ∈ (1...𝑣) ↦ (𝑢 ∈ (1...𝑤) ↦ (ℎ‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))) |
168 | 139, 140,
141, 142, 143, 149, 150, 151, 156, 167 | vdwlem9 15693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) ∧ ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) → (〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) |
169 | 168 | 3expia 1267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓))) → (ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣)))) → (〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ))) |
170 | 169 | ralrimiv 2965 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓))) → ∀ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) |
171 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (1...𝑛) = (1...(𝑤 · (2 · 𝑣)))) |
172 | 171 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (𝑅 ↑𝑚 (1...𝑛)) = (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))) |
173 | 172 | raleqdv 3144 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
174 | | breq2 4657 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = ℎ → (〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ↔ 〈(𝑚 + 1), 𝐾〉 PolyAP ℎ)) |
175 | | breq2 4657 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = ℎ → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP ℎ)) |
176 | 174, 175 | orbi12d 746 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ℎ → ((〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ))) |
177 | 176 | cbvralv 3171 |
. . . . . . . . . . . 12
⊢
(∀𝑓 ∈
(𝑅
↑𝑚 (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) |
178 | 173, 177 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ℎ ∈ (𝑅 ↑𝑚 (1...(𝑤 · (2 · 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ))) |
179 | 178 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝑤 · (2 · 𝑣)) ∈ ℕ ∧
∀ℎ ∈ (𝑅 ↑𝑚
(1...(𝑤 · (2
· 𝑣))))(〈(𝑚 + 1), 𝐾〉 PolyAP ℎ ∨ (𝐾 + 1) MonoAP ℎ)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |
180 | 137, 170,
179 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |
181 | 180 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑤)) ↑𝑚
(1...𝑣))𝐾 MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |
182 | 130, 181 | rexlimddv 3035 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |
183 | 182 | rexlimdvaa 3032 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑤))(〈𝑚, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
184 | 115, 183 | syl5bi 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
185 | 184 | expcom 451 |
. . . 4
⊢ (𝑚 ∈ ℕ → (𝜑 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) |
186 | 185 | a2d 29 |
. . 3
⊢ (𝑚 ∈ ℕ → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑚, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈(𝑚 + 1), 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))) |
187 | 6, 11, 16, 21, 108, 186 | nnind 11038 |
. 2
⊢ (𝑀 ∈ ℕ → (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))) |
188 | 1, 187 | mpcom 38 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑𝑚 (1...𝑛))(〈𝑀, 𝐾〉 PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) |