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){\upharpoonright }_{𝑡}S=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}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){\upharpoonright }_{𝑡}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){\upharpoonright }_{𝑡}S\in \mathrm{Top}$$
12	7 10 11	sylancr	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}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){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
15	13 1 14	sylancr	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
16		toponuni	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)\to S=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
17	15 16	syl	$$⊢\phi \to S=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
18	3 17	sseqtrd	$$⊢\phi \to A\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
19		eqid	$$⊢\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
20	19	ntrss2	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{Top}\wedge A\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\right)\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(A\right)\subseteq A$$
21	12 18 20	syl2anc	$$⊢\phi \to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(A\right)\subseteq A$$
22	6 21	sstrd	$$⊢\phi \to \mathrm{dom}{F}_S^{\prime }\subseteq A$$