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

Theorem vdwlem10 16318
 Description: Lemma for vdw 16322. 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 4795 . . . . . . 7 (𝑥 = 1 → ⟨𝑥, 𝐾⟩ = ⟨1, 𝐾⟩)
32breq1d 5067 . . . . . 6 (𝑥 = 1 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨1, 𝐾⟩ PolyAP 𝑓))
43orbi1d 913 . . . . 5 (𝑥 = 1 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
54rexralbidv 3299 . . . 4 (𝑥 = 1 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
65imbi2d 343 . . 3 (𝑥 = 1 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
7 opeq1 4795 . . . . . . 7 (𝑥 = 𝑚 → ⟨𝑥, 𝐾⟩ = ⟨𝑚, 𝐾⟩)
87breq1d 5067 . . . . . 6 (𝑥 = 𝑚 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑓))
98orbi1d 913 . . . . 5 (𝑥 = 𝑚 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
109rexralbidv 3299 . . . 4 (𝑥 = 𝑚 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1110imbi2d 343 . . 3 (𝑥 = 𝑚 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
12 opeq1 4795 . . . . . . 7 (𝑥 = (𝑚 + 1) → ⟨𝑥, 𝐾⟩ = ⟨(𝑚 + 1), 𝐾⟩)
1312breq1d 5067 . . . . . 6 (𝑥 = (𝑚 + 1) → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓))
1413orbi1d 913 . . . . 5 (𝑥 = (𝑚 + 1) → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1514rexralbidv 3299 . . . 4 (𝑥 = (𝑚 + 1) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
1615imbi2d 343 . . 3 (𝑥 = (𝑚 + 1) → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
17 opeq1 4795 . . . . . . 7 (𝑥 = 𝑀 → ⟨𝑥, 𝐾⟩ = ⟨𝑀, 𝐾⟩)
1817breq1d 5067 . . . . . 6 (𝑥 = 𝑀 → (⟨𝑥, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑀, 𝐾⟩ PolyAP 𝑓))
1918orbi1d 913 . . . . 5 (𝑥 = 𝑀 → ((⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
2019rexralbidv 3299 . . . 4 (𝑥 = 𝑀 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
2120imbi2d 343 . . 3 (𝑥 = 𝑀 → ((𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑥, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) ↔ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))))
22 oveq1 7155 . . . . . . . 8 (𝑠 = 𝑅 → (𝑠m (1...𝑛)) = (𝑅m (1...𝑛)))
2322raleqdv 3414 . . . . . . 7 (𝑠 = 𝑅 → (∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓))
2423rexbidv 3295 . . . . . 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 7156 . . . . . . . 8 (𝑛 = 𝑤 → (1...𝑛) = (1...𝑤))
2928oveq2d 7164 . . . . . . 7 (𝑛 = 𝑤 → (𝑅m (1...𝑛)) = (𝑅m (1...𝑤)))
3029raleqdv 3414 . . . . . 6 (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓))
3130cbvrexvw 3449 . . . . 5 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓)
3227, 31sylib 220 . . . 4 (𝜑 → ∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓)
33 breq2 5061 . . . . . . 7 (𝑓 = 𝑔 → (𝐾 MonoAP 𝑓𝐾 MonoAP 𝑔))
3433cbvralvw 3448 . . . . . 6 (∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 ↔ ∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔)
35 2nn 11702 . . . . . . . 8 2 ∈ ℕ
36 simpr 487 . . . . . . . 8 ((𝜑𝑤 ∈ ℕ) → 𝑤 ∈ ℕ)
37 nnmulcl 11653 . . . . . . . 8 ((2 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (2 · 𝑤) ∈ ℕ)
3835, 36, 37sylancr 589 . . . . . . 7 ((𝜑𝑤 ∈ ℕ) → (2 · 𝑤) ∈ ℕ)
3926adantr 483 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℕ) → 𝑅 ∈ Fin)
40 ovex 7181 . . . . . . . . . . 11 (1...(2 · 𝑤)) ∈ V
41 elmapg 8411 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ (1...(2 · 𝑤)) ∈ V) → (𝑓 ∈ (𝑅m (1...(2 · 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅))
4239, 40, 41sylancl 588 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℕ) → (𝑓 ∈ (𝑅m (1...(2 · 𝑤))) ↔ 𝑓:(1...(2 · 𝑤))⟶𝑅))
4342biimpa 479 . . . . . . . . 9 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅m (1...(2 · 𝑤)))) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
44 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
45 elfznn 12928 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...𝑤) → 𝑦 ∈ ℕ)
4645adantl 484 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℕ)
4746nnred 11645 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦 ∈ ℝ)
48 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℕ)
4948nnred 11645 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℝ)
50 elfzle2 12903 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑤) → 𝑦𝑤)
5150adantl 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑦𝑤)
5247, 49, 49, 51leadd1dd 11246 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (𝑤 + 𝑤))
5348nncnd 11646 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → 𝑤 ∈ ℂ)
54532timesd 11872 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) = (𝑤 + 𝑤))
5552, 54breqtrrd 5085 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ≤ (2 · 𝑤))
5646, 48nnaddcld 11681 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ ℕ)
57 nnuz 12273 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5856, 57eleqtrdi 2921 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (ℤ‘1))
5938ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℕ)
6059nnzd 12078 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (2 · 𝑤) ∈ ℤ)
61 elfz5 12892 . . . . . . . . . . . . . . . 16 (((𝑦 + 𝑤) ∈ (ℤ‘1) ∧ (2 · 𝑤) ∈ ℤ) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤)))
6258, 60, 61syl2anc 586 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → ((𝑦 + 𝑤) ∈ (1...(2 · 𝑤)) ↔ (𝑦 + 𝑤) ≤ (2 · 𝑤)))
6355, 62mpbird 259 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑦 + 𝑤) ∈ (1...(2 · 𝑤)))
6444, 63ffvelrnd 6845 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ 𝑦 ∈ (1...𝑤)) → (𝑓‘(𝑦 + 𝑤)) ∈ 𝑅)
65 fvoveq1 7171 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑓‘(𝑥 + 𝑤)) = (𝑓‘(𝑦 + 𝑤)))
6665cbvmptv 5160 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) = (𝑦 ∈ (1...𝑤) ↦ (𝑓‘(𝑦 + 𝑤)))
6764, 66fmptd 6871 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅)
68 ovex 7181 . . . . . . . . . . . . . 14 (1...𝑤) ∈ V
69 elmapg 8411 . . . . . . . . . . . . . 14 ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ V) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅))
7039, 68, 69sylancl 588 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℕ) → ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) ↔ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅))
7170biimpar 480 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))):(1...𝑤)⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)))
7267, 71syldan 593 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)))
73 breq2 5061 . . . . . . . . . . . 12 (𝑔 = (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
7473rspcv 3616 . . . . . . . . . . 11 ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ∈ (𝑅m (1...𝑤)) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
7572, 74syl 17 . . . . . . . . . 10 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤)))))
76 2nn0 11906 . . . . . . . . . . . . 13 2 ∈ ℕ0
77 vdwlem9.k . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (ℤ‘2))
7877ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈ (ℤ‘2))
79 eluznn0 12309 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝐾 ∈ (ℤ‘2)) → 𝐾 ∈ ℕ0)
8076, 78, 79sylancr 589 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → 𝐾 ∈ ℕ0)
8168, 80, 67vdwmc 16306 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) ↔ ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐})))
8239ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑅 ∈ Fin)
8378adantr 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝐾 ∈ (ℤ‘2))
84 simpllr 774 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑤 ∈ ℕ)
85 simplr 767 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑓:(1...(2 · 𝑤))⟶𝑅)
86 vex 3496 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
87 simprll 777 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑎 ∈ ℕ)
88 simprlr 778 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → 𝑑 ∈ ℕ)
89 simprr 771 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))
9082, 83, 84, 85, 86, 87, 88, 89, 66vdwlem8 16316 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → ⟨1, 𝐾⟩ PolyAP 𝑓)
9190orcd 869 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}))) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
9291expr 459 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9392rexlimdvva 3292 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9493exlimdv 1928 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ ((𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) “ {𝑐}) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9581, 94sylbid 242 . . . . . . . . . 10 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (𝐾 MonoAP (𝑥 ∈ (1...𝑤) ↦ (𝑓‘(𝑥 + 𝑤))) → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9675, 95syld 47 . . . . . . . . 9 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓:(1...(2 · 𝑤))⟶𝑅) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9743, 96syldan 593 . . . . . . . 8 (((𝜑𝑤 ∈ ℕ) ∧ 𝑓 ∈ (𝑅m (1...(2 · 𝑤)))) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → (⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
9897ralrimdva 3187 . . . . . . 7 ((𝜑𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
99 oveq2 7156 . . . . . . . . . 10 (𝑛 = (2 · 𝑤) → (1...𝑛) = (1...(2 · 𝑤)))
10099oveq2d 7164 . . . . . . . . 9 (𝑛 = (2 · 𝑤) → (𝑅m (1...𝑛)) = (𝑅m (1...(2 · 𝑤))))
101100raleqdv 3414 . . . . . . . 8 (𝑛 = (2 · 𝑤) → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
102101rspcev 3621 . . . . . . 7 (((2 · 𝑤) ∈ ℕ ∧ ∀𝑓 ∈ (𝑅m (1...(2 · 𝑤)))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
10338, 98, 102syl6an 682 . . . . . 6 ((𝜑𝑤 ∈ ℕ) → (∀𝑔 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑔 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
10434, 103syl5bi 244 . . . . 5 ((𝜑𝑤 ∈ ℕ) → (∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
105104rexlimdva 3282 . . . 4 (𝜑 → (∃𝑤 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑤))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
10632, 105mpd 15 . . 3 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨1, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
107 breq2 5061 . . . . . . . . . 10 (𝑓 = 𝑔 → (⟨𝑚, 𝐾⟩ PolyAP 𝑓 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑔))
108 breq2 5061 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP 𝑔))
109107, 108orbi12d 915 . . . . . . . . 9 (𝑓 = 𝑔 → ((⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
110109cbvralvw 3448 . . . . . . . 8 (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
11129raleqdv 3414 . . . . . . . 8 (𝑛 = 𝑤 → (∀𝑔 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
112110, 111syl5bb 285 . . . . . . 7 (𝑛 = 𝑤 → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
113112cbvrexvw 3449 . . . . . 6 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
114 oveq2 7156 . . . . . . . . . . . . 13 (𝑛 = 𝑣 → (1...𝑛) = (1...𝑣))
115114oveq2d 7164 . . . . . . . . . . . 12 (𝑛 = 𝑣 → (𝑠m (1...𝑛)) = (𝑠m (1...𝑣)))
116115raleqdv 3414 . . . . . . . . . . 11 (𝑛 = 𝑣 → (∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓))
117116cbvrexvw 3449 . . . . . . . . . 10 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓)
118 oveq1 7155 . . . . . . . . . . . 12 (𝑠 = (𝑅m (1...𝑤)) → (𝑠m (1...𝑣)) = ((𝑅m (1...𝑤)) ↑m (1...𝑣)))
119118raleqdv 3414 . . . . . . . . . . 11 (𝑠 = (𝑅m (1...𝑤)) → (∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))
120119rexbidv 3295 . . . . . . . . . 10 (𝑠 = (𝑅m (1...𝑤)) → (∃𝑣 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑣))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))
121117, 120syl5bb 285 . . . . . . . . 9 (𝑠 = (𝑅m (1...𝑤)) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑣 ∈ ℕ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))
12225ad2antrr 724 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓)
12326ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → 𝑅 ∈ Fin)
124 fzfi 13332 . . . . . . . . . 10 (1...𝑤) ∈ Fin
125 mapfi 8812 . . . . . . . . . 10 ((𝑅 ∈ Fin ∧ (1...𝑤) ∈ Fin) → (𝑅m (1...𝑤)) ∈ Fin)
126123, 124, 125sylancl 588 . . . . . . . . 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 777 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → 𝑤 ∈ ℕ)
129 simprrl 779 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → 𝑣 ∈ ℕ)
130 nnmulcl 11653 . . . . . . . . . . . . 13 ((2 ∈ ℕ ∧ 𝑣 ∈ ℕ) → (2 · 𝑣) ∈ ℕ)
13135, 130mpan 688 . . . . . . . . . . . 12 (𝑣 ∈ ℕ → (2 · 𝑣) ∈ ℕ)
132 nnmulcl 11653 . . . . . . . . . . . 12 ((𝑤 ∈ ℕ ∧ (2 · 𝑣) ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
133131, 132sylan2 594 . . . . . . . . . . 11 ((𝑤 ∈ ℕ ∧ 𝑣 ∈ ℕ) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
134128, 129, 133syl2anc 586 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → (𝑤 · (2 · 𝑣)) ∈ ℕ)
135 simp1l 1192 . . . . . . . . . . . . . 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 1193 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝑚 ∈ ℕ)
140 simp2ll 1235 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝑤 ∈ ℕ)
141 simp2lr 1236 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
142 breq2 5061 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑘 → (⟨𝑚, 𝐾⟩ PolyAP 𝑔 ↔ ⟨𝑚, 𝐾⟩ PolyAP 𝑘))
143 breq2 5061 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑘 → ((𝐾 + 1) MonoAP 𝑔 ↔ (𝐾 + 1) MonoAP 𝑘))
144142, 143orbi12d 915 . . . . . . . . . . . . . . 15 (𝑔 = 𝑘 → ((⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ (⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘)))
145144cbvralvw 3448 . . . . . . . . . . . . . 14 (∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) ↔ ∀𝑘 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘))
146141, 145sylib 220 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑘 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑘 ∨ (𝐾 + 1) MonoAP 𝑘))
147 simp2rl 1237 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → 𝑣 ∈ ℕ)
148 simp2rr 1238 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)
149 simp3 1133 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))))
150 ovex 7181 . . . . . . . . . . . . . . 15 (1...(𝑤 · (2 · 𝑣))) ∈ V
151 elmapg 8411 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Fin ∧ (1...(𝑤 · (2 · 𝑣))) ∈ V) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) ↔ :(1...(𝑤 · (2 · 𝑣)))⟶𝑅))
152136, 150, 151sylancl 588 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) ↔ :(1...(𝑤 · (2 · 𝑣)))⟶𝑅))
153149, 152mpbid 234 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → :(1...(𝑤 · (2 · 𝑣)))⟶𝑅)
154 fvoveq1 7171 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))))
155154cbvmptv 5160 . . . . . . . . . . . . . . 15 (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))))
156 oveq1 7155 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (𝑥 − 1) = (𝑧 − 1))
157156oveq1d 7163 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → ((𝑥 − 1) + 𝑣) = ((𝑧 − 1) + 𝑣))
158157oveq2d 7164 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝑤 · ((𝑥 − 1) + 𝑣)) = (𝑤 · ((𝑧 − 1) + 𝑣)))
159158oveq2d 7164 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))) = (𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))
160159fveq2d 6667 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣)))) = (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣)))))
161160mpteq2dv 5153 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
162155, 161syl5eq 2866 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣))))) = (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
163162cbvmptv 5160 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝑣) ↦ (𝑦 ∈ (1...𝑤) ↦ (‘(𝑦 + (𝑤 · ((𝑥 − 1) + 𝑣)))))) = (𝑧 ∈ (1...𝑣) ↦ (𝑢 ∈ (1...𝑤) ↦ (‘(𝑢 + (𝑤 · ((𝑧 − 1) + 𝑣))))))
164136, 137, 138, 139, 140, 146, 147, 148, 153, 163vdwlem9 16317 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) ∧ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))) → (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP ))
1651643expia 1116 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ( ∈ (𝑅m (1...(𝑤 · (2 · 𝑣)))) → (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
166165ralrimiv 3179 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP ))
167 oveq2 7156 . . . . . . . . . . . . . 14 (𝑛 = (𝑤 · (2 · 𝑣)) → (1...𝑛) = (1...(𝑤 · (2 · 𝑣))))
168167oveq2d 7164 . . . . . . . . . . . . 13 (𝑛 = (𝑤 · (2 · 𝑣)) → (𝑅m (1...𝑛)) = (𝑅m (1...(𝑤 · (2 · 𝑣)))))
169168raleqdv 3414 . . . . . . . . . . . 12 (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀𝑓 ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
170 breq2 5061 . . . . . . . . . . . . . 14 (𝑓 = → (⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ↔ ⟨(𝑚 + 1), 𝐾⟩ PolyAP ))
171 breq2 5061 . . . . . . . . . . . . . 14 (𝑓 = → ((𝐾 + 1) MonoAP 𝑓 ↔ (𝐾 + 1) MonoAP ))
172170, 171orbi12d 915 . . . . . . . . . . . . 13 (𝑓 = → ((⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ (⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
173172cbvralvw 3448 . . . . . . . . . . . 12 (∀𝑓 ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP ))
174169, 173syl6bb 289 . . . . . . . . . . 11 (𝑛 = (𝑤 · (2 · 𝑣)) → (∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) ↔ ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )))
175174rspcev 3621 . . . . . . . . . 10 (((𝑤 · (2 · 𝑣)) ∈ ℕ ∧ ∀ ∈ (𝑅m (1...(𝑤 · (2 · 𝑣))))(⟨(𝑚 + 1), 𝐾⟩ PolyAP ∨ (𝐾 + 1) MonoAP )) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
176134, 166, 175syl2anc 586 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
177176anassrs 470 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) ∧ (𝑣 ∈ ℕ ∧ ∀𝑓 ∈ ((𝑅m (1...𝑤)) ↑m (1...𝑣))𝐾 MonoAP 𝑓)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
178127, 177rexlimddv 3289 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ (𝑤 ∈ ℕ ∧ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
179178rexlimdvaa 3283 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (∃𝑤 ∈ ℕ ∀𝑔 ∈ (𝑅m (1...𝑤))(⟨𝑚, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
180113, 179syl5bi 244 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨𝑚, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅m (1...𝑛))(⟨(𝑚 + 1), 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓)))
181180expcom 416 . . . 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 11648 . 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 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1082   = wceq 1531  ∃wex 1774   ∈ wcel 2108  ∀wral 3136  ∃wrex 3137  Vcvv 3493   ⊆ wss 3934  {csn 4559  ⟨cop 4565   class class class wbr 5057   ↦ cmpt 5137  ◡ccnv 5547   “ cima 5551  ⟶wf 6344  ‘cfv 6348  (class class class)co 7148   ↑m cmap 8398  Fincfn 8501  1c1 10530   + caddc 10532   · cmul 10534   ≤ cle 10668   − cmin 10862  ℕcn 11630  2c2 11684  ℕ0cn0 11889  ℤcz 11973  ℤ≥cuz 12235  ...cfz 12884  APcvdwa 16293   MonoAP cvdwm 16294   PolyAP cvdwp 16295 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 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-dju 9322  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12885  df-hash 13683  df-vdwap 16296  df-vdwmc 16297  df-vdwpc 16298 This theorem is referenced by:  vdwlem11  16319
 Copyright terms: Public domain W3C validator