Metamath Proof Explorer

Theorem dvbss

Description: The set of differentiable points is a subset of the domain of the function. (Contributed by Mario Carneiro, 6-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}$
Assertion dvbss ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {A}$

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 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}$
5 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
6 1 2 3 4 5 dvbssntr ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)$
7 5 cnfldtop ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$
8 cnex ${⊢}ℂ\in \mathrm{V}$
9 ssexg ${⊢}\left({S}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to {S}\in \mathrm{V}$
10 1 8 9 sylancl ${⊢}{\phi }\to {S}\in \mathrm{V}$
11 resttop ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge {S}\in \mathrm{V}\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}$
12 7 10 11 sylancr ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}$
13 5 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
14 resttopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge {S}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
15 13 1 14 sylancr ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
16 toponuni ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)\to {S}=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
17 15 16 syl ${⊢}{\phi }\to {S}=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
18 3 17 sseqtrd ${⊢}{\phi }\to {A}\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
19 eqid ${⊢}\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
20 19 ntrss2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}\wedge {A}\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\right)\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)\subseteq {A}$
21 12 18 20 syl2anc ${⊢}{\phi }\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({A}\right)\subseteq {A}$
22 6 21 sstrd ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {A}$