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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvdmsscn.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
Assertion	dvdmsscn	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )

Proof

Step	Hyp	Ref	Expression
1		dvdmsscn.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvdmsscn.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3		restsspw	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ⊆ 𝒫 𝑆
4	3 2	sseldi	⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝑆 )
5		elpwi	⊢ ( 𝑋 ∈ 𝒫 𝑆 → 𝑋 ⊆ 𝑆 )
6	4 5	syl	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
7		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
8	1 7	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
9	6 8	sstrd	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )