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	|- ( ph -> S e. { RR , CC } )
	dvdmsscn.x	|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
Assertion	dvdmsscn	|- ( ph -> X C_ CC )

Proof

Step	Hyp	Ref	Expression
1		dvdmsscn.s	|- ( ph -> S e. { RR , CC } )
2		dvdmsscn.x	|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3		restsspw	|- ( ( TopOpen ` CCfld ) |`t S ) C_ ~P S
4	3 2	sseldi	|- ( ph -> X e. ~P S )
5		elpwi	|- ( X e. ~P S -> X C_ S )
6	4 5	syl	|- ( ph -> X C_ S )
7		recnprss	|- ( S e. { RR , CC } -> S C_ CC )
8	1 7	syl	|- ( ph -> S C_ CC )
9	6 8	sstrd	|- ( ph -> X C_ CC )