MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwlem10 Structured version   Visualization version   GIF version

Theorem vdwlem10 17028
Description: Lemma for vdw 17032. Set up secondary induction on 𝑀. (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdw.r (𝜑𝑅 ∈ Fin)
vdwlem9.k (𝜑𝐾 ∈ (ℤ‘2))
vdwlem9.s (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓)
vdwlem10.m (𝜑𝑀 ∈ ℕ)
Assertion
Ref Expression
vdwlem10 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
Distinct variable groups:   𝜑,𝑛,𝑓   𝑓,𝑠,𝐾,𝑛   𝑓,𝑀,𝑛   𝑅,𝑓,𝑛,𝑠   𝜑,𝑓
Allowed substitution hints:   𝜑(𝑠)   𝑀(𝑠)

Proof of Theorem vdwlem10
Dummy variables 𝑎 𝑐 𝑑 𝑔 𝑘 𝑚 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vdwlem10.m . 2 (𝜑𝑀 ∈ ℕ)
2 opeq1 4873 . . . . . . 7 (𝑥 = 1 → ⟨𝑥, 𝐾⟩ = ⟨1, 𝐾⟩)
32breq1d 5153 . . . . . 6 (𝑥 = 1 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨1, 𝐾⟩ PolyAP 𝑓))
43orbi1d 917 . . . . 5 (𝑥 = 1 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
54rexralbidv 3223 . . . 4 (𝑥 = 1 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
65imbi2d 340 . . 3 (𝑥 = 1 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
7 opeq1 4873 . . . . . . 7 (𝑥 = 𝑚 → ⟨𝑥, 𝐾⟩ = ⟨𝑚, 𝐾⟩)
87breq1d 5153 . . . . . 6 (𝑥 = 𝑚 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑓))
98orbi1d 917 . . . . 5 (𝑥 = 𝑚 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
109rexralbidv 3223 . . . 4 (𝑥 = 𝑚 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1110imbi2d 340 . . 3 (𝑥 = 𝑚 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
12 opeq1 4873 . . . . . . 7 (𝑥 = (𝑚 + 1) → ⟨𝑥, 𝐾⟩ = ⟨(𝑚 + 1), 𝐾⟩)
1312breq1d 5153 . . . . . 6 (𝑥 = (𝑚 + 1) → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓))
1413orbi1d 917 . . . . 5 (𝑥 = (𝑚 + 1) → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1514rexralbidv 3223 . . . 4 (𝑥 = (𝑚 + 1) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1615imbi2d 340 . . 3 (𝑥 = (𝑚 + 1) → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
17 opeq1 4873 . . . . . . 7 (𝑥 = 𝑀 → ⟨𝑥, 𝐾⟩ = ⟨𝑀, 𝐾⟩)
1817breq1d 5153 . . . . . 6 (𝑥 = 𝑀 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑀, 𝐾⟩ PolyAP 𝑓))
1918orbi1d 917 . . . . 5 (𝑥 = 𝑀 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
2019rexralbidv 3223 . . . 4 (𝑥 = 𝑀 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
2120imbi2d 340 . . 3 (𝑥 = 𝑀 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
22 oveq1 7438 . . . . . . . 8 (𝑠 = 𝑅 → (𝑠m (1...𝑛)) = (𝑅m (1...𝑛)))
2322raleqdv 3326 . . . . . . 7 (𝑠 = 𝑅 → (∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓))
2423rexbidv 3179 . . . . . 6 (𝑠 = 𝑅 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓))
25 vdwlem9.s . . . . . 6 (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓)
26 vdw.r . . . . . 6 (𝜑𝑅 ∈ Fin)
2724, 25, 26rspcdva 3623 . . . . 5 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓)
28 oveq2 7439 . . . . . . . 8 (𝑛 = 𝑤 → (1...𝑛) = (1...𝑤))
2928oveq2d 7447 . . . . . . 7 (𝑛 = 𝑤 → (𝑅m (1...𝑛)) = (𝑅m (1...𝑤)))
3029raleqdv 3326 . . . . . 6 (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓))
3130cbvrexvw 3238 . . . . 5 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓)
3227, 31sylib 218 . . . 4 (𝜑 → ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓)
33 breq2 5147 . . . . . . 7 (𝑓 = 𝑔 → (𝐾 MonoAP 𝑓𝐾 MonoAP 𝑔))
3433cbvralvw 3237 . . . . . 6 (∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 ↔ ∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔)
35 2nn 12339 . . . . . . . 8 2 ∈ ℕ
36 simpr 484 . . . . . . . 8 ((𝜑𝑤 ∈ ℕ) → 𝑤 ∈ ℕ)
37 nnmulcl 12290 . . . . . . . 8 ((2 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (2 · 𝑤) ∈ ℕ)
3835, 36, 37sylancr 587 . . . . . . 7 ((𝜑𝑤 ∈ ℕ) → (2 · 𝑤) ∈ ℕ)
3926adantr 480 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℕ) → 𝑅 ∈ Fin)
40 ovex 7464 . . . . . . . . . . 11 (1...(2 · 𝑤)) ∈ V
41 elmapg 8879 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ (1...(2 · 𝑤)) ∈ V) → (𝑓 ∈ (𝑅m (1...(2 · 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅))
4239, 40, 41sylancl 586 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℕ) → (𝑓 ∈ (𝑅m (1...(2 · 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅))
4342biimpa 476 . . . . . . . . 9 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅m (1...(2 · 𝑤)))) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
44 simplr 769 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
45 elfznn 13593 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...𝑤) → 𝑦 ∈ ℕ)
4645adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℕ)
4746nnred 12281 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℝ)
48 simpllr 776 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℕ)
4948nnred 12281 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℝ)
50 elfzle2 13568 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑤) → 𝑦𝑤)
5150adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦𝑤)
5247, 49, 49, 51leadd1dd 11877 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (𝑤 + 𝑤))
5348nncnd 12282 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℂ)
54532timesd 12509 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) = (𝑤 + 𝑤))
5552, 54breqtrrd 5171 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (2 · 𝑤))
5646, 48nnaddcld 12318 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ ℕ)
57 nnuz 12921 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5856, 57eleqtrdi 2851 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (ℤ‘1))
5938ad2antrr 726 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℕ)
6059nnzd 12640 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℤ)
61 elfz5 13556 . . . . . . . . . . . . . . . 16 (((𝑦 + 𝑤) ∈ (ℤ‘1) ∧ (2 · 𝑤) ∈ ℤ) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤)))
6258, 60, 61syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤)))
6355, 62mpbird 257 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (1...(2 · 𝑤)))
6444, 63ffvelcdmd 7105 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑓‘(𝑦 + 𝑤)) ∈ 𝑅)
65 fvoveq1 7454 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑓‘(𝑥 + 𝑤)) = (𝑓‘(𝑦 + 𝑤)))
6665cbvmptv 5255 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) = (𝑦 ∈ (1...𝑤) ↦ (𝑓‘(𝑦 + 𝑤)))
6764, 66fmptd 7134 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅)
68 ovex 7464 . . . . . . . . . . . . . 14 (1...𝑤) ∈ V
69 elmapg 8879 . . . . . . . . . . . . . 14 ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ V) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅))
7039, 68, 69sylancl 586 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℕ) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅))
7170biimpar 477 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)))
7267, 71syldan 591 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)))
73 breq2 5147 . . . . . . . . . . . 12 (𝑔 = (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
7473rspcv 3618 . . . . . . . . . . 11 ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
7572, 74syl 17 . . . . . . . . . 10 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
76 2nn0 12543 . . . . . . . . . . . . 13 2 ∈ ℕ0
77 vdwlem9.k . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (ℤ‘2))
7877ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈ (ℤ‘2))
79 eluznn0 12959 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝐾 ∈ (ℤ‘2)) → 𝐾 ∈ ℕ0)
8076, 78, 79sylancr 587 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈ ℕ0)
8168, 80, 67vdwmc 17016 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ↔ ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐})))
8239ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑅 ∈ Fin)
8378adantr 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...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))
9082, 83, 84, 85, 86, 87, 88, 89, 66vdwlem8 17026 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → ⟨1, 𝐾⟩ PolyAP 𝑓)
9190orcd 874 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
9291expr 456 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9392rexlimdvva 3213 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9493exlimdv 1933 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9581, 94sylbid 240 . . . . . . . . . 10 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9675, 95syld 47 . . . . . . . . 9 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9743, 96syldan 591 . . . . . . . 8 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅m (1...(2 · 𝑤)))) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9897ralrimdva 3154 . . . . . . 7 ((𝜑𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
99 oveq2 7439 . . . . . . . . . 10 (𝑛 = (2 · 𝑤) → (1...𝑛) = (1...(2 · 𝑤)))
10099oveq2d 7447 . . . . . . . . 9 (𝑛 = (2 · 𝑤) → (𝑅m (1...𝑛)) = (𝑅m (1...(2 · 𝑤))))
101100raleqdv 3326 . . . . . . . 8 (𝑛 = (2 · 𝑤) → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
102101rspcev 3622 . . . . . . 7 (((2 · 𝑤) ∈ ℕ ∧ ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
10338, 98, 102syl6an 684 . . . . . 6 ((𝜑𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
10434, 103biimtrid 242 . . . . 5 ((𝜑𝑤 ∈ ℕ) → (∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
105104rexlimdva 3155 . . . 4 (𝜑 → (∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
10632, 105mpd 15 . . 3 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
107 breq2 5147 . . . . . . . . . 10 (𝑓 = 𝑔 → (⟨𝑚, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑔))
108 breq2 5147 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP 𝑔))
109107, 108orbi12d 919 . . . . . . . . 9 (𝑓 = 𝑔 → ((⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
110109cbvralvw 3237 . . . . . . . 8 (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
11129raleqdv 3326 . . . . . . . 8 (𝑛 = 𝑤 → (∀𝑔 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
112110, 111bitrid 283 . . . . . . 7 (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
113112cbvrexvw 3238 . . . . . 6 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
114 oveq2 7439 . . . . . . . . . . . . 13 (𝑛 = 𝑣 → (1...𝑛) = (1...𝑣))
115114oveq2d 7447 . . . . . . . . . . . 12 (𝑛 = 𝑣 → (𝑠m (1...𝑛)) = (𝑠m (1...𝑣)))
116115raleqdv 3326 . . . . . . . . . . 11 (𝑛 = 𝑣 → (∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓))
117116cbvrexvw 3238 . . . . . . . . . 10 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓)
118 oveq1 7438 . . . . . . . . . . . 12 (𝑠 = (𝑅m (1...𝑤)) → (𝑠m (1...𝑣)) = ((𝑅m (1...𝑤)) ↑m (1...𝑣)))
119118raleqdv 3326 . . . . . . . . . . 11 (𝑠 = (𝑅m (1...𝑤)) → (∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))
120119rexbidv 3179 . . . . . . . . . 10 (𝑠 = (𝑅m (1...𝑤)) → (∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))
121117, 120bitrid 283 . . . . . . . . 9 (𝑠 = (𝑅m (1...𝑤)) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))
12225ad2antrr 726 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓)
12326ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → 𝑅 ∈ Fin)
124 fzfi 14013 . . . . . . . . . 10 (1...𝑤) ∈ Fin
125 mapfi 9388 . . . . . . . . . 10 ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ Fin) → (𝑅m (1...𝑤)) ∈ Fin)
126123, 124, 125sylancl 586 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → (𝑅m (1...𝑤)) ∈ Fin)
127121, 122, 126rspcdva 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 · 𝑣) ∈ ℕ)
13135, 130mpan 690 . . . . . . . . . . . 12 (𝑣 ∈ ℕ → (2 · 𝑣) ∈ ℕ)
132 nnmulcl 12290 . . . . . . . . . . . 12 ((𝑤 ∈ ℕ ∧ (2 · 𝑣) ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
133131, 132sylan2 593 . . . . . . . . . . 11 ((𝑤 ∈ ℕ ∧ 𝑣 ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
134128, 129, 133syl2anc 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 · 𝑣))))) → 𝜑)
136135, 26syl 17 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝑅 ∈ Fin)
137135, 77syl 17 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝐾 ∈ (ℤ‘2))
138135, 25syl 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 𝑘))
144142, 143orbi12d 919 . . . . . . . . . . . . . . 15 (𝑔 = 𝑘 → ((⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘)))
145144cbvralvw 3237 . . . . . . . . . . . . . 14 (∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑘 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘))
146141, 145sylib 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 · 𝑣)))⟶𝑅))
152136, 150, 151sylancl 586 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) ↔ :(1...(𝑤 · (2 · 𝑣)))⟶𝑅))
153149, 152mpbid 232 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → :(1...(𝑤 · (2 · 𝑣)))⟶𝑅)
154 fvoveq1 7454 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))))
155154cbvmptv 5255 . . . . . . . . . . . . . . 15 (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))))
156 oveq1 7438 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (𝑥 − 1) = (𝑧 − 1))
157156oveq1d 7446 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → ((𝑥 − 1) + 𝑣) = ((𝑧 − 1) + 𝑣))
158157oveq2d 7447 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝑤 · ((𝑥 − 1) + 𝑣)) = (𝑤 · ((𝑧 − 1) + 𝑣)))
159158oveq2d 7447 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))) = (𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))
160159fveq2d 6910 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))
161160mpteq2dv 5244 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
162155, 161eqtrid 2789 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
163162cbvmptv 5255 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝑣) ↦ (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))))) = (𝑧 ∈ (1...𝑣) ↦ (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
164136, 137, 138, 139, 140, 146, 147, 148, 153, 163vdwlem9 17027 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP ))
1651643expia 1122 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) → (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
166165ralrimiv 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 · 𝑣))))
168167oveq2d 7447 . . . . . . . . . . . . 13 (𝑛 = (𝑤 · (2 · 𝑣)) → (𝑅m (1...𝑛)) = (𝑅m (1...(𝑤 · (2 · 𝑣)))))
169168raleqdv 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 ))
172170, 171orbi12d 919 . . . . . . . . . . . . 13 (𝑓 = → ((⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
173172cbvralvw 3237 . . . . . . . . . . . 12 (∀𝑓 ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP ))
174169, 173bitrdi 287 . . . . . . . . . . 11 (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
175174rspcev 3622 . . . . . . . . . 10 (((𝑤 · (2 · 𝑣)) ∈ ℕ ∧ ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
176134, 166, 175syl2anc 584 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
177176anassrs 467 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
178127, 177rexlimddv 3161 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
179178rexlimdvaa 3156 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
180113, 179biimtrid 242 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
181180expcom 413 . . . 4 (𝑚 ∈ ℕ → (𝜑 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
182181a2d 29 . . 3 (𝑚 ∈ ℕ → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
1836, 11, 16, 21, 106, 182nnind 12284 . 2 (𝑀 ∈ ℕ → (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1841, 183mpcom 38 1 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  wss 3951  {csn 4626  cop 4632   class class class wbr 5143  cmpt 5225  ccnv 5684  cima 5688  wf 6557  cfv 6561  (class class class)co 7431  m cmap 8866  Fincfn 8985  1c1 11156   + caddc 11158   · cmul 11160  cle 11296  cmin 11492  cn 12266  2c2 12321  0cn0 12526  cz 12613  cuz 12878  ...cfz 13547  APcvdwa 17003   MonoAP cvdwm 17004   PolyAP cvdwp 17005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-hash 14370  df-vdwap 17006  df-vdwmc 17007  df-vdwpc 17008
This theorem is referenced by:  vdwlem11  17029
  Copyright terms: Public domain W3C validator