vdwlem9 - Metamath Proof Explorer

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

Theorem vdwlem9 15531

Description: Lemma for vdw 15536. (Contributed by Mario Carneiro, 12-Sep-2014.)

**Hypotheses**
Ref	Expression
vdw.r	⊢ (𝜑 → 𝑅 ∈ Fin)
vdwlem9.k	⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
vdwlem9.s	⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑_𝑚 (1...𝑛))𝐾 MonoAP 𝑓)
vdwlem9.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
vdwlem9.w	⊢ (𝜑 → 𝑊 ∈ ℕ)
vdwlem9.g	⊢ (𝜑 → ∀𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
vdwlem9.v	⊢ (𝜑 → 𝑉 ∈ ℕ)
vdwlem9.a	⊢ (𝜑 → ∀𝑓 ∈ ((𝑅 ↑_𝑚 (1...𝑊)) ↑_𝑚 (1...𝑉))𝐾 MonoAP 𝑓)
vdwlem9.h	⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
vdwlem9.f	⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))

**Assertion**
Ref	Expression
vdwlem9	⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))

Distinct variable groups: 𝑔,𝑛,𝑥,𝑦,𝜑 𝑥,𝑓,𝑦,𝑉 𝑓,𝑊,𝑥,𝑦 𝑓,𝑔,𝐹,𝑥,𝑦 𝑓,𝑛,𝑠,𝐾,𝑔,𝑥,𝑦 𝑓,𝑀,𝑔,𝑛,𝑥,𝑦 𝑅,𝑓,𝑔,𝑛,𝑠,𝑥,𝑦 𝑔,𝐻,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑓,𝑠) 𝐹(𝑛,𝑠) 𝐻(𝑓,𝑛,𝑠) 𝑀(𝑠) 𝑉(𝑔,𝑛,𝑠) 𝑊(𝑔,𝑛,𝑠)

Proof of Theorem vdwlem9 Dummy variables 𝑎 𝑑 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vdwlem9.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ ℕ)
2		vdwlem9.w	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ ℕ)
3		vdw.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Fin)
4		vdwlem9.h	. . . . 5 ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
5		vdwlem9.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
6	1, 2, 3, 4, 5	vdwlem4 15526	. . . 4 ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑_𝑚 (1...𝑊)))
7		ovex 6577	. . . . 5 ⊢ (𝑅 ↑_𝑚 (1...𝑊)) ∈ V
8		ovex 6577	. . . . 5 ⊢ (1...𝑉) ∈ V
9	7, 8	elmap 7772	. . . 4 ⊢ (𝐹 ∈ ((𝑅 ↑_𝑚 (1...𝑊)) ↑_𝑚 (1...𝑉)) ↔ 𝐹:(1...𝑉)⟶(𝑅 ↑_𝑚 (1...𝑊)))
10	6, 9	sylibr 223	. . 3 ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↑_𝑚 (1...𝑊)) ↑_𝑚 (1...𝑉)))
11		vdwlem9.a	. . 3 ⊢ (𝜑 → ∀𝑓 ∈ ((𝑅 ↑_𝑚 (1...𝑊)) ↑_𝑚 (1...𝑉))𝐾 MonoAP 𝑓)
12		breq2 4587	. . . 4 ⊢ (𝑓 = 𝐹 → (𝐾 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝐹))
13	12	rspcv 3278	. . 3 ⊢ (𝐹 ∈ ((𝑅 ↑_𝑚 (1...𝑊)) ↑_𝑚 (1...𝑉)) → (∀𝑓 ∈ ((𝑅 ↑_𝑚 (1...𝑊)) ↑_𝑚 (1...𝑉))𝐾 MonoAP 𝑓 → 𝐾 MonoAP 𝐹))
14	10, 11, 13	sylc 63	. 2 ⊢ (𝜑 → 𝐾 MonoAP 𝐹)
15		vdwlem9.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
16		eluz2nn 11602	. . . . . 6 ⊢ (𝐾 ∈ (ℤ_≥‘2) → 𝐾 ∈ ℕ)
17	15, 16	syl 17	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ)
18	17	nnnn0d 11228	. . . 4 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
19	8, 18, 6	vdwmc 15520	. . 3 ⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑔∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔})))
20		vdwlem9.g	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
21	20	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ∀𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
22		simprr 792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))
23	17	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ)
24		simprll 798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℕ)
25		simprlr 799	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑑 ∈ ℕ)
26		vdwapid1 15517	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑))
27	23, 24, 25, 26	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑))
28	22, 27	sseldd 3569	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑎 ∈ (^◡𝐹 “ {𝑔}))
29		ffn 5958	. . . . . . . . . . . . . 14 ⊢ (𝐹:(1...𝑉)⟶(𝑅 ↑_𝑚 (1...𝑊)) → 𝐹 Fn (1...𝑉))
30	6, 29	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 Fn (1...𝑉))
31	30	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝐹 Fn (1...𝑉))
32		fniniseg 6246	. . . . . . . . . . . 12 ⊢ (𝐹 Fn (1...𝑉) → (𝑎 ∈ (^◡𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔)))
33	31, 32	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 ∈ (^◡𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔)))
34	28, 33	mpbid 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔))
35	34	simprd 478	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) = 𝑔)
36	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝐹:(1...𝑉)⟶(𝑅 ↑_𝑚 (1...𝑊)))
37	34	simpld 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑎 ∈ (1...𝑉))
38	36, 37	ffvelrnd 6268	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) ∈ (𝑅 ↑_𝑚 (1...𝑊)))
39	35, 38	eqeltrrd 2689	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊)))
40		rsp 2913	. . . . . . . 8 ⊢ (∀𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊)) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
41	21, 39, 40	sylc 63	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
42	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℕ)
43	2	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℕ)
44	3	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑅 ∈ Fin)
45	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
46		vdwlem9.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
47	46	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑀 ∈ ℕ)
48		ovex 6577	. . . . . . . . . . . 12 ⊢ (1...𝑊) ∈ V
49		elmapg 7757	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Fin ∧ (1...𝑊) ∈ V) → (𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅))
50	44, 48, 49	sylancl 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑔 ∈ (𝑅 ↑_𝑚 (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅))
51	39, 50	mpbid 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑔:(1...𝑊)⟶𝑅)
52	15	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝐾 ∈ (ℤ_≥‘2))
53	42, 43, 44, 45, 5, 47, 51, 52, 24, 25, 22	vdwlem7 15529	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
54		olc 398	. . . . . . . . . 10 ⊢ ((𝐾 + 1) MonoAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))
55	54	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
56	53, 55	jaod 394	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
57		oveq1 6556	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑎 → (𝑥 − 1) = (𝑎 − 1))
58	57	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → ((𝑥 − 1) + 𝑉) = ((𝑎 − 1) + 𝑉))
59	58	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝑎 − 1) + 𝑉)))
60	59	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))
61	60	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
62	61	mpteq2dv 4673	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
63	48	mptex 6390	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ∈ V
64	62, 5, 63	fvmpt 6191	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (1...𝑉) → (𝐹‘𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
65	37, 64	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
66	65, 35	eqtr3d 2646	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = 𝑔)
67	66	breq2d 4595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ↔ (𝐾 + 1) MonoAP 𝑔))
68	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ₀)
69		peano2nn0 11210	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ₀ → (𝐾 + 1) ∈ ℕ₀)
70	68, 69	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝐾 + 1) ∈ ℕ₀)
71		nnm1nn0 11211	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → (𝑎 − 1) ∈ ℕ₀)
72	24, 71	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℕ₀)
73		nn0nnaddcl 11201	. . . . . . . . . . . . 13 ⊢ (((𝑎 − 1) ∈ ℕ₀ ∧ 𝑉 ∈ ℕ) → ((𝑎 − 1) + 𝑉) ∈ ℕ)
74	72, 42, 73	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℕ)
75	43, 74	nnmulcld 10945	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · ((𝑎 − 1) + 𝑉)) ∈ ℕ)
76	24, 42	nnaddcld 10944	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℕ)
77	43, 76	nnmulcld 10945	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℕ)
78	77	nnzd 11357	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℤ)
79		2nn 11062	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ
80		nnmulcl 10920	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ 𝑉 ∈ ℕ) → (2 · 𝑉) ∈ ℕ)
81	79, 1, 80	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 𝑉) ∈ ℕ)
82	2, 81	nnmulcld 10945	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℕ)
83	82	nnzd 11357	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℤ)
84	83	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ ℤ)
85	24	nnred 10912	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℝ)
86	42	nnred 10912	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℝ)
87		elfzle2 12216	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (1...𝑉) → 𝑎 ≤ 𝑉)
88	37, 87	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑎 ≤ 𝑉)
89	85, 86, 86, 88	leadd1dd 10520	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (𝑉 + 𝑉))
90	42	nncnd 10913	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℂ)
91	90	2timesd 11152	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (2 · 𝑉) = (𝑉 + 𝑉))
92	89, 91	breqtrrd 4611	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (2 · 𝑉))
93	76	nnred 10912	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℝ)
94	81	nnred 10912	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 𝑉) ∈ ℝ)
95	94	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (2 · 𝑉) ∈ ℝ)
96	43	nnred 10912	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℝ)
97	43	nngt0d 10941	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 0 < 𝑊)
98		lemul2 10755	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 + 𝑉) ∈ ℝ ∧ (2 · 𝑉) ∈ ℝ ∧ (𝑊 ∈ ℝ ∧ 0 < 𝑊)) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
99	93, 95, 96, 97, 98	syl112anc 1322	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
100	92, 99	mpbid 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))
101		eluz2 11569	. . . . . . . . . . . . 13 ⊢ ((𝑊 · (2 · 𝑉)) ∈ (ℤ_≥‘(𝑊 · (𝑎 + 𝑉))) ↔ ((𝑊 · (𝑎 + 𝑉)) ∈ ℤ ∧ (𝑊 · (2 · 𝑉)) ∈ ℤ ∧ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
102	78, 84, 100, 101	syl3anbrc 1239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ (ℤ_≥‘(𝑊 · (𝑎 + 𝑉))))
103	43	nncnd 10913	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℂ)
104		1cnd 9935	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 1 ∈ ℂ)
105	72	nn0cnd 11230	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℂ)
106	105, 90	addcld 9938	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℂ)
107	103, 104, 106	adddid 9943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))))
108	104, 105, 90	addassd 9941	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (1 + ((𝑎 − 1) + 𝑉)))
109		ax-1cn 9873	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℂ
110	24	nncnd 10913	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℂ)
111		pncan3 10168	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎)
112	109, 110, 111	sylancr 694	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (1 + (𝑎 − 1)) = 𝑎)
113	112	oveq1d 6564	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (𝑎 + 𝑉))
114	108, 113	eqtr3d 2646	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (1 + ((𝑎 − 1) + 𝑉)) = (𝑎 + 𝑉))
115	114	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = (𝑊 · (𝑎 + 𝑉)))
116	103	mulid1d 9936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · 1) = 𝑊)
117	116	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))
118	107, 115, 117	3eqtr3d 2652	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))
119	118	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (ℤ_≥‘(𝑊 · (𝑎 + 𝑉))) = (ℤ_≥‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
120	102, 119	eleqtrd 2690	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ (ℤ_≥‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
121		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))) = (𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉))))
122	121	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))) = (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
123	122	cbvmptv 4678	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = (𝑧 ∈ (1...𝑊) ↦ (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
124	44, 70, 43, 75, 45, 120, 123	vdwlem2 15524	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) → (𝐾 + 1) MonoAP 𝐻))
125	67, 124	sylbird 249	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (𝐾 + 1) MonoAP 𝐻))
126	125	orim2d 881	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
127	56, 126	syld 46	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → ((⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
128	41, 127	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}))) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))
129	128	expr 641	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
130	129	rexlimdvva 3020	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
131	130	exlimdv 1848	. . 3 ⊢ (𝜑 → (∃𝑔∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (^◡𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
132	19, 131	sylbid 229	. 2 ⊢ (𝜑 → (𝐾 MonoAP 𝐹 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
133	14, 132	mpd 15	1 ⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ⊆ wss 3540 {csn 4125 ⟨cop 4131 class class class wbr 4583 ↦ cmpt 4643 ^◡ccnv 5037 “ cima 5041 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↑_𝑚 cmap 7744 Fincfn 7841 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 APcvdwa 15507 MonoAP cvdwm 15508 PolyAP cvdwp 15509

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-hash 12980 df-vdwap 15510 df-vdwmc 15511 df-vdwpc 15512

This theorem is referenced by: vdwlem10 15532

W3C validator