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

Theorem vdwmc2 16532
Description: Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdwmc.1 𝑋 ∈ V
vdwmc.2 (𝜑𝐾 ∈ ℕ0)
vdwmc.3 (𝜑𝐹:𝑋𝑅)
vdwmc2.4 (𝜑𝐴𝑋)
Assertion
Ref Expression
vdwmc2 (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐})))
Distinct variable groups:   𝑎,𝑐,𝑑,𝑚,𝐹   𝐾,𝑎,𝑐,𝑑,𝑚   𝜑,𝑐   𝑅,𝑎,𝑐,𝑑   𝜑,𝑎,𝑑
Allowed substitution hints:   𝜑(𝑚)   𝐴(𝑚,𝑎,𝑐,𝑑)   𝑅(𝑚)   𝑋(𝑚,𝑎,𝑐,𝑑)

Proof of Theorem vdwmc2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 vdwmc.1 . . 3 𝑋 ∈ V
2 vdwmc.2 . . 3 (𝜑𝐾 ∈ ℕ0)
3 vdwmc.3 . . 3 (𝜑𝐹:𝑋𝑅)
41, 2, 3vdwmc 16531 . 2 (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})))
5 vdwapid1 16528 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑))
65ne0d 4250 . . . . . . . . . . 11 ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) ≠ ∅)
763expb 1122 . . . . . . . . . 10 ((𝐾 ∈ ℕ ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (𝑎(AP‘𝐾)𝑑) ≠ ∅)
87adantll 714 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (𝑎(AP‘𝐾)𝑑) ≠ ∅)
9 ssn0 4315 . . . . . . . . . 10 (((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ∧ (𝑎(AP‘𝐾)𝑑) ≠ ∅) → (𝐹 “ {𝑐}) ≠ ∅)
109expcom 417 . . . . . . . . 9 ((𝑎(AP‘𝐾)𝑑) ≠ ∅ → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) → (𝐹 “ {𝑐}) ≠ ∅))
118, 10syl 17 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) → (𝐹 “ {𝑐}) ≠ ∅))
12 disjsn 4627 . . . . . . . . . 10 ((𝑅 ∩ {𝑐}) = ∅ ↔ ¬ 𝑐𝑅)
133adantr 484 . . . . . . . . . . . 12 ((𝜑𝐾 ∈ ℕ) → 𝐹:𝑋𝑅)
14 fimacnvdisj 6597 . . . . . . . . . . . . 13 ((𝐹:𝑋𝑅 ∧ (𝑅 ∩ {𝑐}) = ∅) → (𝐹 “ {𝑐}) = ∅)
1514ex 416 . . . . . . . . . . . 12 (𝐹:𝑋𝑅 → ((𝑅 ∩ {𝑐}) = ∅ → (𝐹 “ {𝑐}) = ∅))
1613, 15syl 17 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ℕ) → ((𝑅 ∩ {𝑐}) = ∅ → (𝐹 “ {𝑐}) = ∅))
1716adantr 484 . . . . . . . . . 10 (((𝜑𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑅 ∩ {𝑐}) = ∅ → (𝐹 “ {𝑐}) = ∅))
1812, 17syl5bir 246 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (¬ 𝑐𝑅 → (𝐹 “ {𝑐}) = ∅))
1918necon1ad 2957 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝐹 “ {𝑐}) ≠ ∅ → 𝑐𝑅))
2011, 19syld 47 . . . . . . 7 (((𝜑𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) → 𝑐𝑅))
2120rexlimdvva 3213 . . . . . 6 ((𝜑𝐾 ∈ ℕ) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) → 𝑐𝑅))
2221pm4.71rd 566 . . . . 5 ((𝜑𝐾 ∈ ℕ) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ (𝑐𝑅 ∧ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))))
2322exbidv 1929 . . . 4 ((𝜑𝐾 ∈ ℕ) → (∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑐(𝑐𝑅 ∧ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))))
24 df-rex 3067 . . . 4 (∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑐(𝑐𝑅 ∧ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})))
2523, 24bitr4di 292 . . 3 ((𝜑𝐾 ∈ ℕ) → (∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})))
26 vdwmc2.4 . . . . . . . 8 (𝜑𝐴𝑋)
273, 26ffvelrnd 6905 . . . . . . 7 (𝜑 → (𝐹𝐴) ∈ 𝑅)
2827ne0d 4250 . . . . . 6 (𝜑𝑅 ≠ ∅)
29 1nn 11841 . . . . . . . . 9 1 ∈ ℕ
3029ne0ii 4252 . . . . . . . 8 ℕ ≠ ∅
31 simpllr 776 . . . . . . . . . . . . . . 15 ((((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → 𝐾 = 0)
3231fveq2d 6721 . . . . . . . . . . . . . 14 ((((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (AP‘𝐾) = (AP‘0))
3332oveqd 7230 . . . . . . . . . . . . 13 ((((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) = (𝑎(AP‘0)𝑑))
34 vdwap0 16529 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘0)𝑑) = ∅)
3534adantll 714 . . . . . . . . . . . . 13 ((((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘0)𝑑) = ∅)
3633, 35eqtrd 2777 . . . . . . . . . . . 12 ((((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) = ∅)
37 0ss 4311 . . . . . . . . . . . 12 ∅ ⊆ (𝐹 “ {𝑐})
3836, 37eqsstrdi 3955 . . . . . . . . . . 11 ((((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
3938ralrimiva 3105 . . . . . . . . . 10 (((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) → ∀𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
40 r19.2z 4406 . . . . . . . . . 10 ((ℕ ≠ ∅ ∧ ∀𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})) → ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
4130, 39, 40sylancr 590 . . . . . . . . 9 (((𝜑𝐾 = 0) ∧ 𝑎 ∈ ℕ) → ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
4241ralrimiva 3105 . . . . . . . 8 ((𝜑𝐾 = 0) → ∀𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
43 r19.2z 4406 . . . . . . . 8 ((ℕ ≠ ∅ ∧ ∀𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
4430, 42, 43sylancr 590 . . . . . . 7 ((𝜑𝐾 = 0) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
4544ralrimivw 3106 . . . . . 6 ((𝜑𝐾 = 0) → ∀𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
46 r19.2z 4406 . . . . . 6 ((𝑅 ≠ ∅ ∧ ∀𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})) → ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
4728, 45, 46syl2an2r 685 . . . . 5 ((𝜑𝐾 = 0) → ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
48 rexex 3162 . . . . 5 (∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) → ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
4947, 48syl 17 . . . 4 ((𝜑𝐾 = 0) → ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}))
5049, 472thd 268 . . 3 ((𝜑𝐾 = 0) → (∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})))
51 elnn0 12092 . . . 4 (𝐾 ∈ ℕ0 ↔ (𝐾 ∈ ℕ ∨ 𝐾 = 0))
522, 51sylib 221 . . 3 (𝜑 → (𝐾 ∈ ℕ ∨ 𝐾 = 0))
5325, 50, 52mpjaodan 959 . 2 (𝜑 → (∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐})))
54 vdwapval 16526 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → (𝑥 ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑))))
55543expb 1122 . . . . . . . 8 ((𝐾 ∈ ℕ0 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (𝑥 ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑))))
562, 55sylan 583 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (𝑥 ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑))))
5756imbi1d 345 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑥 ∈ (𝑎(AP‘𝐾)𝑑) → 𝑥 ∈ (𝐹 “ {𝑐})) ↔ (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐}))))
5857albidv 1928 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (∀𝑥(𝑥 ∈ (𝑎(AP‘𝐾)𝑑) → 𝑥 ∈ (𝐹 “ {𝑐})) ↔ ∀𝑥(∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐}))))
59 dfss2 3886 . . . . 5 ((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∀𝑥(𝑥 ∈ (𝑎(AP‘𝐾)𝑑) → 𝑥 ∈ (𝐹 “ {𝑐})))
60 ralcom4 3157 . . . . . 6 (∀𝑚 ∈ (0...(𝐾 − 1))∀𝑥(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})) ↔ ∀𝑥𝑚 ∈ (0...(𝐾 − 1))(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})))
61 ovex 7246 . . . . . . . 8 (𝑎 + (𝑚 · 𝑑)) ∈ V
62 eleq1 2825 . . . . . . . 8 (𝑥 = (𝑎 + (𝑚 · 𝑑)) → (𝑥 ∈ (𝐹 “ {𝑐}) ↔ (𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐})))
6361, 62ceqsalv 3443 . . . . . . 7 (∀𝑥(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})) ↔ (𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐}))
6463ralbii 3088 . . . . . 6 (∀𝑚 ∈ (0...(𝐾 − 1))∀𝑥(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})) ↔ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐}))
65 r19.23v 3198 . . . . . . 7 (∀𝑚 ∈ (0...(𝐾 − 1))(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})) ↔ (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})))
6665albii 1827 . . . . . 6 (∀𝑥𝑚 ∈ (0...(𝐾 − 1))(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})) ↔ ∀𝑥(∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})))
6760, 64, 663bitr3i 304 . . . . 5 (∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐}) ↔ ∀𝑥(∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (𝐹 “ {𝑐})))
6858, 59, 673bitr4g 317 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐})))
69682rexbidva 3218 . . 3 (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐})))
7069rexbidv 3216 . 2 (𝜑 → (∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐})))
714, 53, 703bitrd 308 1 (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐𝑅𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (𝐹 “ {𝑐})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3a 1089  wal 1541   = wceq 1543  wex 1787  wcel 2110  wne 2940  wral 3061  wrex 3062  Vcvv 3408  cin 3865  wss 3866  c0 4237  {csn 4541   class class class wbr 5053  ccnv 5550  cima 5554  wf 6376  cfv 6380  (class class class)co 7213  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734  cmin 11062  cn 11830  0cn0 12090  ...cfz 13095  APcvdwa 16518   MonoAP cvdwm 16519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-fz 13096  df-vdwap 16521  df-vdwmc 16522
This theorem is referenced by:  vdw  16547
  Copyright terms: Public domain W3C validator