Theorem dvdmsscn

Description: X is a subset of CC . This statement is very often used when computing derivatives. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvdmsscn.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvdmsscn.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
Assertion	dvdmsscn	$$⊢\phi \to X\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		dvdmsscn.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvdmsscn.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		restsspw	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\subseteq 𝒫S$$
4	3 2	sseldi	$$⊢\phi \to X\in 𝒫S$$
5		elpwi	$$⊢X\in 𝒫S\to X\subseteq S$$
6	4 5	syl	$$⊢\phi \to X\subseteq S$$
7		recnprss	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$
8	1 7	syl	$$⊢\phi \to S\subseteq ℂ$$
9	6 8	sstrd	$$⊢\phi \to X\subseteq ℂ$$