# Metamath Proof Explorer

## Theorem dvbssntr

Description: The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses dvcl.s ${⊢}{\phi }\to {S}\subseteq ℂ$
dvcl.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
dvcl.a ${⊢}{\phi }\to {A}\subseteq {S}$
dvbssntr.j ${⊢}{J}={K}{↾}_{𝑡}{S}$
dvbssntr.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion dvbssntr ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq \mathrm{int}\left({J}\right)\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 dvcl.s ${⊢}{\phi }\to {S}\subseteq ℂ$
2 dvcl.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
3 dvcl.a ${⊢}{\phi }\to {A}\subseteq {S}$
4 dvbssntr.j ${⊢}{J}={K}{↾}_{𝑡}{S}$
5 dvbssntr.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
6 4 5 dvfval ${⊢}\left({S}\subseteq ℂ\wedge {F}:{A}⟶ℂ\wedge {A}\subseteq {S}\right)\to \left({S}\mathrm{D}{F}=\bigcup _{{x}\in \mathrm{int}\left({J}\right)\left({A}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)\wedge {S}\mathrm{D}{F}\subseteq \mathrm{int}\left({J}\right)\left({A}\right)×ℂ\right)$
7 1 2 3 6 syl3anc ${⊢}{\phi }\to \left({S}\mathrm{D}{F}=\bigcup _{{x}\in \mathrm{int}\left({J}\right)\left({A}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)\wedge {S}\mathrm{D}{F}\subseteq \mathrm{int}\left({J}\right)\left({A}\right)×ℂ\right)$
8 dmss ${⊢}{S}\mathrm{D}{F}\subseteq \mathrm{int}\left({J}\right)\left({A}\right)×ℂ\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq \mathrm{dom}\left(\mathrm{int}\left({J}\right)\left({A}\right)×ℂ\right)$
9 7 8 simpl2im ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq \mathrm{dom}\left(\mathrm{int}\left({J}\right)\left({A}\right)×ℂ\right)$
10 dmxpss ${⊢}\mathrm{dom}\left(\mathrm{int}\left({J}\right)\left({A}\right)×ℂ\right)\subseteq \mathrm{int}\left({J}\right)\left({A}\right)$
11 9 10 sstrdi ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq \mathrm{int}\left({J}\right)\left({A}\right)$