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

Theorem vdwlem10 16958
Description: Lemma for vdw 16962. 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 4874 . . . . . . 7 (𝑥 = 1 → ⟨𝑥, 𝐾⟩ = ⟨1, 𝐾⟩)
32breq1d 5158 . . . . . 6 (𝑥 = 1 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨1, 𝐾⟩ PolyAP 𝑓))
43orbi1d 915 . . . . 5 (𝑥 = 1 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
54rexralbidv 3217 . . . 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 4874 . . . . . . 7 (𝑥 = 𝑚 → ⟨𝑥, 𝐾⟩ = ⟨𝑚, 𝐾⟩)
87breq1d 5158 . . . . . 6 (𝑥 = 𝑚 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑓))
98orbi1d 915 . . . . 5 (𝑥 = 𝑚 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
109rexralbidv 3217 . . . 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 4874 . . . . . . 7 (𝑥 = (𝑚 + 1) → ⟨𝑥, 𝐾⟩ = ⟨(𝑚 + 1), 𝐾⟩)
1312breq1d 5158 . . . . . 6 (𝑥 = (𝑚 + 1) → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓))
1413orbi1d 915 . . . . 5 (𝑥 = (𝑚 + 1) → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1514rexralbidv 3217 . . . 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 4874 . . . . . . 7 (𝑥 = 𝑀 → ⟨𝑥, 𝐾⟩ = ⟨𝑀, 𝐾⟩)
1817breq1d 5158 . . . . . 6 (𝑥 = 𝑀 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑀, 𝐾⟩ PolyAP 𝑓))
1918orbi1d 915 . . . . 5 (𝑥 = 𝑀 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
2019rexralbidv 3217 . . . 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 7427 . . . . . . . 8 (𝑠 = 𝑅 → (𝑠m (1...𝑛)) = (𝑅m (1...𝑛)))
2322raleqdv 3322 . . . . . . 7 (𝑠 = 𝑅 → (∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓))
2423rexbidv 3175 . . . . . 6 (𝑠 = 𝑅 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓))
25 vdwlem9.s . . . . . 6 (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓)
26 vdw.r . . . . . 6 (𝜑𝑅 ∈ Fin)
2724, 25, 26rspcdva 3610 . . . . 5 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓)
28 oveq2 7428 . . . . . . . 8 (𝑛 = 𝑤 → (1...𝑛) = (1...𝑤))
2928oveq2d 7436 . . . . . . 7 (𝑛 = 𝑤 → (𝑅m (1...𝑛)) = (𝑅m (1...𝑤)))
3029raleqdv 3322 . . . . . 6 (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓))
3130cbvrexvw 3232 . . . . 5 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓)
3227, 31sylib 217 . . . 4 (𝜑 → ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓)
33 breq2 5152 . . . . . . 7 (𝑓 = 𝑔 → (𝐾 MonoAP 𝑓𝐾 MonoAP 𝑔))
3433cbvralvw 3231 . . . . . 6 (∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 ↔ ∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔)
35 2nn 12315 . . . . . . . 8 2 ∈ ℕ
36 simpr 484 . . . . . . . 8 ((𝜑𝑤 ∈ ℕ) → 𝑤 ∈ ℕ)
37 nnmulcl 12266 . . . . . . . 8 ((2 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (2 · 𝑤) ∈ ℕ)
3835, 36, 37sylancr 586 . . . . . . 7 ((𝜑𝑤 ∈ ℕ) → (2 · 𝑤) ∈ ℕ)
3926adantr 480 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℕ) → 𝑅 ∈ Fin)
40 ovex 7453 . . . . . . . . . . 11 (1...(2 · 𝑤)) ∈ V
41 elmapg 8857 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ (1...(2 · 𝑤)) ∈ V) → (𝑓 ∈ (𝑅m (1...(2 · 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅))
4239, 40, 41sylancl 585 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℕ) → (𝑓 ∈ (𝑅m (1...(2 · 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅))
4342biimpa 476 . . . . . . . . 9 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅m (1...(2 · 𝑤)))) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
44 simplr 768 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
45 elfznn 13562 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...𝑤) → 𝑦 ∈ ℕ)
4645adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℕ)
4746nnred 12257 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℝ)
48 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℕ)
4948nnred 12257 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℝ)
50 elfzle2 13537 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑤) → 𝑦𝑤)
5150adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦𝑤)
5247, 49, 49, 51leadd1dd 11858 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (𝑤 + 𝑤))
5348nncnd 12258 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℂ)
54532timesd 12485 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) = (𝑤 + 𝑤))
5552, 54breqtrrd 5176 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (2 · 𝑤))
5646, 48nnaddcld 12294 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ ℕ)
57 nnuz 12895 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5856, 57eleqtrdi 2839 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (ℤ‘1))
5938ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℕ)
6059nnzd 12615 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℤ)
61 elfz5 13525 . . . . . . . . . . . . . . . 16 (((𝑦 + 𝑤) ∈ (ℤ‘1) ∧ (2 · 𝑤) ∈ ℤ) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤)))
6258, 60, 61syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤)))
6355, 62mpbird 257 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (1...(2 · 𝑤)))
6444, 63ffvelcdmd 7095 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑓‘(𝑦 + 𝑤)) ∈ 𝑅)
65 fvoveq1 7443 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑓‘(𝑥 + 𝑤)) = (𝑓‘(𝑦 + 𝑤)))
6665cbvmptv 5261 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) = (𝑦 ∈ (1...𝑤) ↦ (𝑓‘(𝑦 + 𝑤)))
6764, 66fmptd 7124 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅)
68 ovex 7453 . . . . . . . . . . . . . 14 (1...𝑤) ∈ V
69 elmapg 8857 . . . . . . . . . . . . . 14 ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ V) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅))
7039, 68, 69sylancl 585 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℕ) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅))
7170biimpar 477 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)))
7267, 71syldan 590 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)))
73 breq2 5152 . . . . . . . . . . . 12 (𝑔 = (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
7473rspcv 3605 . . . . . . . . . . 11 ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
7572, 74syl 17 . . . . . . . . . 10 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
76 2nn0 12519 . . . . . . . . . . . . 13 2 ∈ ℕ0
77 vdwlem9.k . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (ℤ‘2))
7877ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈ (ℤ‘2))
79 eluznn0 12931 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝐾 ∈ (ℤ‘2)) → 𝐾 ∈ ℕ0)
8076, 78, 79sylancr 586 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈ ℕ0)
8168, 80, 67vdwmc 16946 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ↔ ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐})))
8239ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑅 ∈ Fin)
8378adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝐾 ∈ (ℤ‘2))
84 simpllr 775 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑤 ∈ ℕ)
85 simplr 768 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
86 vex 3475 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
87 simprll 778 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑎 ∈ ℕ)
88 simprlr 779 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑑 ∈ ℕ)
89 simprr 772 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))
9082, 83, 84, 85, 86, 87, 88, 89, 66vdwlem8 16956 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → ⟨1, 𝐾⟩ PolyAP 𝑓)
9190orcd 872 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
9291expr 456 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9392rexlimdvva 3208 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9493exlimdv 1929 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9581, 94sylbid 239 . . . . . . . . . 10 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9675, 95syld 47 . . . . . . . . 9 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9743, 96syldan 590 . . . . . . . 8 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅m (1...(2 · 𝑤)))) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9897ralrimdva 3151 . . . . . . 7 ((𝜑𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
99 oveq2 7428 . . . . . . . . . 10 (𝑛 = (2 · 𝑤) → (1...𝑛) = (1...(2 · 𝑤)))
10099oveq2d 7436 . . . . . . . . 9 (𝑛 = (2 · 𝑤) → (𝑅m (1...𝑛)) = (𝑅m (1...(2 · 𝑤))))
101100raleqdv 3322 . . . . . . . 8 (𝑛 = (2 · 𝑤) → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
102101rspcev 3609 . . . . . . 7 (((2 · 𝑤) ∈ ℕ ∧ ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
10338, 98, 102syl6an 683 . . . . . 6 ((𝜑𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
10434, 103biimtrid 241 . . . . 5 ((𝜑𝑤 ∈ ℕ) → (∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
105104rexlimdva 3152 . . . 4 (𝜑 → (∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
10632, 105mpd 15 . . 3 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
107 breq2 5152 . . . . . . . . . 10 (𝑓 = 𝑔 → (⟨𝑚, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑔))
108 breq2 5152 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP 𝑔))
109107, 108orbi12d 917 . . . . . . . . 9 (𝑓 = 𝑔 → ((⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
110109cbvralvw 3231 . . . . . . . 8 (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
11129raleqdv 3322 . . . . . . . 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 3232 . . . . . 6 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
114 oveq2 7428 . . . . . . . . . . . . 13 (𝑛 = 𝑣 → (1...𝑛) = (1...𝑣))
115114oveq2d 7436 . . . . . . . . . . . 12 (𝑛 = 𝑣 → (𝑠m (1...𝑛)) = (𝑠m (1...𝑣)))
116115raleqdv 3322 . . . . . . . . . . 11 (𝑛 = 𝑣 → (∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓))
117116cbvrexvw 3232 . . . . . . . . . 10 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓)
118 oveq1 7427 . . . . . . . . . . . 12 (𝑠 = (𝑅m (1...𝑤)) → (𝑠m (1...𝑣)) = ((𝑅m (1...𝑤)) ↑m (1...𝑣)))
119118raleqdv 3322 . . . . . . . . . . 11 (𝑠 = (𝑅m (1...𝑤)) → (∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))
120119rexbidv 3175 . . . . . . . . . 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 725 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓)
12326ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → 𝑅 ∈ Fin)
124 fzfi 13969 . . . . . . . . . 10 (1...𝑤) ∈ Fin
125 mapfi 9372 . . . . . . . . . 10 ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ Fin) → (𝑅m (1...𝑤)) ∈ Fin)
126123, 124, 125sylancl 585 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → (𝑅m (1...𝑤)) ∈ Fin)
127121, 122, 126rspcdva 3610 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)
128 simprll 778 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → 𝑤 ∈ ℕ)
129 simprrl 780 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → 𝑣 ∈ ℕ)
130 nnmulcl 12266 . . . . . . . . . . . . 13 ((2 ∈ ℕ ∧ 𝑣 ∈ ℕ) → (2 · 𝑣) ∈ ℕ)
13135, 130mpan 689 . . . . . . . . . . . 12 (𝑣 ∈ ℕ → (2 · 𝑣) ∈ ℕ)
132 nnmulcl 12266 . . . . . . . . . . . 12 ((𝑤 ∈ ℕ ∧ (2 · 𝑣) ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
133131, 132sylan2 592 . . . . . . . . . . 11 ((𝑤 ∈ ℕ ∧ 𝑣 ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
134128, 129, 133syl2anc 583 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
135 simp1l 1195 . . . . . . . . . . . . . 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 1196 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝑚 ∈ ℕ)
140 simp2ll 1238 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝑤 ∈ ℕ)
141 simp2lr 1239 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
142 breq2 5152 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑘 → (⟨𝑚, 𝐾⟩ PolyAP 𝑔 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑘))
143 breq2 5152 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑘 → ((𝐾 + 1) MonoAP 𝑔 ↔ (𝐾 + 1) MonoAP 𝑘))
144142, 143orbi12d 917 . . . . . . . . . . . . . . 15 (𝑔 = 𝑘 → ((⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘)))
145144cbvralvw 3231 . . . . . . . . . . . . . 14 (∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑘 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘))
146141, 145sylib 217 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑘 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘))
147 simp2rl 1240 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝑣 ∈ ℕ)
148 simp2rr 1241 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)
149 simp3 1136 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))))
150 ovex 7453 . . . . . . . . . . . . . . 15 (1...(𝑤 · (2 · 𝑣))) ∈ V
151 elmapg 8857 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Fin ∧ (1...(𝑤 · (2 · 𝑣))) ∈ V) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) ↔ :(1...(𝑤 · (2 · 𝑣)))⟶𝑅))
152136, 150, 151sylancl 585 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) ↔ :(1...(𝑤 · (2 · 𝑣)))⟶𝑅))
153149, 152mpbid 231 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → :(1...(𝑤 · (2 · 𝑣)))⟶𝑅)
154 fvoveq1 7443 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))))
155154cbvmptv 5261 . . . . . . . . . . . . . . 15 (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))))
156 oveq1 7427 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (𝑥 − 1) = (𝑧 − 1))
157156oveq1d 7435 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → ((𝑥 − 1) + 𝑣) = ((𝑧 − 1) + 𝑣))
158157oveq2d 7436 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝑤 · ((𝑥 − 1) + 𝑣)) = (𝑤 · ((𝑧 − 1) + 𝑣)))
159158oveq2d 7436 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))) = (𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))
160159fveq2d 6901 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))
161160mpteq2dv 5250 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
162155, 161eqtrid 2780 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
163162cbvmptv 5261 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝑣) ↦ (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))))) = (𝑧 ∈ (1...𝑣) ↦ (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
164136, 137, 138, 139, 140, 146, 147, 148, 153, 163vdwlem9 16957 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP ))
1651643expia 1119 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) → (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
166165ralrimiv 3142 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP ))
167 oveq2 7428 . . . . . . . . . . . . . 14 (𝑛 = (𝑤 · (2 · 𝑣)) → (1...𝑛) = (1...(𝑤 · (2 · 𝑣))))
168167oveq2d 7436 . . . . . . . . . . . . 13 (𝑛 = (𝑤 · (2 · 𝑣)) → (𝑅m (1...𝑛)) = (𝑅m (1...(𝑤 · (2 · 𝑣)))))
169168raleqdv 3322 . . . . . . . . . . . 12 (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
170 breq2 5152 . . . . . . . . . . . . . 14 (𝑓 = → (⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ↔ ⟨(𝑚 + 1), 𝐾⟩ PolyAP ))
171 breq2 5152 . . . . . . . . . . . . . 14 (𝑓 = → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP ))
172170, 171orbi12d 917 . . . . . . . . . . . . 13 (𝑓 = → ((⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
173172cbvralvw 3231 . . . . . . . . . . . 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 3609 . . . . . . . . . 10 (((𝑤 · (2 · 𝑣)) ∈ ℕ ∧ ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
176134, 166, 175syl2anc 583 . . . . . . . . 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 3158 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
179178rexlimdvaa 3153 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
180113, 179biimtrid 241 . . . . 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 12260 . 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 205  wa 395  wo 846  w3a 1085   = wceq 1534  wex 1774  wcel 2099  wral 3058  wrex 3067  Vcvv 3471  wss 3947  {csn 4629  cop 4635   class class class wbr 5148  cmpt 5231  ccnv 5677  cima 5681  wf 6544  cfv 6548  (class class class)co 7420  m cmap 8844  Fincfn 8963  1c1 11139   + caddc 11141   · cmul 11143  cle 11279  cmin 11474  cn 12242  2c2 12297  0cn0 12502  cz 12588  cuz 12852  ...cfz 13516  APcvdwa 16933   MonoAP cvdwm 16934   PolyAP cvdwp 16935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-1o 8486  df-oadd 8490  df-er 8724  df-map 8846  df-pm 8847  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-dju 9924  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-n0 12503  df-z 12589  df-uz 12853  df-rp 13007  df-fz 13517  df-hash 14322  df-vdwap 16936  df-vdwmc 16937  df-vdwpc 16938
This theorem is referenced by:  vdwlem11  16959
  Copyright terms: Public domain W3C validator