# Metamath Proof Explorer

## Theorem dvbsss

Description: The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Assertion dvbsss ${⊢}\mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$

### Proof

Step Hyp Ref Expression
1 df-dv ${⊢}\mathrm{D}=\left({s}\in 𝒫ℂ,{f}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)⟼\bigcup _{{x}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{s}\right)\left(\mathrm{dom}{f}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left(\mathrm{dom}{f}\setminus \left\{{x}\right\}\right)⟼\frac{{f}\left({z}\right)-{f}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)\right)$
2 1 reldmmpo ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{D}$
3 df-rel ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{D}↔\mathrm{dom}\mathrm{D}\subseteq \mathrm{V}×\mathrm{V}$
4 2 3 mpbi ${⊢}\mathrm{dom}\mathrm{D}\subseteq \mathrm{V}×\mathrm{V}$
5 4 sseli ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to ⟨{S},{F}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
6 opelxp1 ${⊢}⟨{S},{F}⟩\in \left(\mathrm{V}×\mathrm{V}\right)\to {S}\in \mathrm{V}$
7 5 6 syl ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to {S}\in \mathrm{V}$
8 opeq1 ${⊢}{s}={S}\to ⟨{s},{F}⟩=⟨{S},{F}⟩$
9 8 eleq1d ${⊢}{s}={S}\to \left(⟨{s},{F}⟩\in \mathrm{dom}\mathrm{D}↔⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\right)$
10 eleq1 ${⊢}{s}={S}\to \left({s}\in 𝒫ℂ↔{S}\in 𝒫ℂ\right)$
11 oveq2 ${⊢}{s}={S}\to ℂ{↑}_{𝑝𝑚}{s}=ℂ{↑}_{𝑝𝑚}{S}$
12 11 eleq2d ${⊢}{s}={S}\to \left({F}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)↔{F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)$
13 10 12 anbi12d ${⊢}{s}={S}\to \left(\left({s}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)\right)↔\left({S}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\right)$
14 9 13 imbi12d ${⊢}{s}={S}\to \left(\left(⟨{s},{F}⟩\in \mathrm{dom}\mathrm{D}\to \left({s}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)\right)\right)↔\left(⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \left({S}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\right)\right)$
15 1 dmmpossx ${⊢}\mathrm{dom}\mathrm{D}\subseteq \bigcup _{{s}\in 𝒫ℂ}\left(\left\{{s}\right\}×\left(ℂ{↑}_{𝑝𝑚}{s}\right)\right)$
16 15 sseli ${⊢}⟨{s},{F}⟩\in \mathrm{dom}\mathrm{D}\to ⟨{s},{F}⟩\in \bigcup _{{s}\in 𝒫ℂ}\left(\left\{{s}\right\}×\left(ℂ{↑}_{𝑝𝑚}{s}\right)\right)$
17 opeliunxp ${⊢}⟨{s},{F}⟩\in \bigcup _{{s}\in 𝒫ℂ}\left(\left\{{s}\right\}×\left(ℂ{↑}_{𝑝𝑚}{s}\right)\right)↔\left({s}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)\right)$
18 16 17 sylib ${⊢}⟨{s},{F}⟩\in \mathrm{dom}\mathrm{D}\to \left({s}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)\right)$
19 14 18 vtoclg ${⊢}{S}\in \mathrm{V}\to \left(⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \left({S}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)\right)$
20 7 19 mpcom ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \left({S}\in 𝒫ℂ\wedge {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)\right)$
21 20 simpld ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to {S}\in 𝒫ℂ$
22 21 elpwid ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to {S}\subseteq ℂ$
23 20 simprd ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to {F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)$
24 cnex ${⊢}ℂ\in \mathrm{V}$
25 elpm2g ${⊢}\left(ℂ\in \mathrm{V}\wedge {S}\in 𝒫ℂ\right)\to \left({F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)↔\left({F}:\mathrm{dom}{F}⟶ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)\right)$
26 24 21 25 sylancr ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \left({F}\in \left(ℂ{↑}_{𝑝𝑚}{S}\right)↔\left({F}:\mathrm{dom}{F}⟶ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)\right)$
27 23 26 mpbid ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \left({F}:\mathrm{dom}{F}⟶ℂ\wedge \mathrm{dom}{F}\subseteq {S}\right)$
28 27 simpld ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to {F}:\mathrm{dom}{F}⟶ℂ$
29 27 simprd ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \mathrm{dom}{F}\subseteq {S}$
30 22 28 29 dvbss ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq \mathrm{dom}{F}$
31 30 29 sstrd ${⊢}⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$
32 df-ov ${⊢}{S}\mathrm{D}{F}=\mathrm{D}\left(⟨{S},{F}⟩\right)$
33 ndmfv ${⊢}¬⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \mathrm{D}\left(⟨{S},{F}⟩\right)=\varnothing$
34 32 33 syl5eq ${⊢}¬⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to {S}\mathrm{D}{F}=\varnothing$
35 34 dmeqd ${⊢}¬⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \mathrm{dom}{{F}}_{{S}}^{\prime }=\mathrm{dom}\varnothing$
36 dm0 ${⊢}\mathrm{dom}\varnothing =\varnothing$
37 35 36 syl6eq ${⊢}¬⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \mathrm{dom}{{F}}_{{S}}^{\prime }=\varnothing$
38 0ss ${⊢}\varnothing \subseteq {S}$
39 37 38 eqsstrdi ${⊢}¬⟨{S},{F}⟩\in \mathrm{dom}\mathrm{D}\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$
40 31 39 pm2.61i ${⊢}\mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$