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	\|- ( ph -> S C_ CC )
	dvcl.f	\|- ( ph -> F : A --> CC )
	dvcl.a	\|- ( ph -> A C_ S )
Assertion	dvbss	\|- ( ph -> dom ( S _D F ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		dvcl.s	\|- ( ph -> S C_ CC )
2		dvcl.f	\|- ( ph -> F : A --> CC )
3		dvcl.a	\|- ( ph -> A C_ S )
4		eqid	\|- ( ( TopOpen ` CCfld ) \|`t S ) = ( ( TopOpen ` CCfld ) \|`t S )
5		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
6	1 2 3 4 5	dvbssntr	\|- ( ph -> dom ( S _D F ) C_ ( ( int ` ( ( TopOpen ` CCfld ) \|`t S ) ) ` A ) )
7	5	cnfldtop	\|- ( TopOpen ` CCfld ) e. Top
8		cnex	\|- CC e. _V
9		ssexg	\|- ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
10	1 8 9	sylancl	\|- ( ph -> S e. _V )
11		resttop	\|- ( ( ( TopOpen ` CCfld ) e. Top /\ S e. _V ) -> ( ( TopOpen ` CCfld ) \|`t S ) e. Top )
12	7 10 11	sylancr	\|- ( ph -> ( ( TopOpen ` CCfld ) \|`t S ) e. Top )
13	5	cnfldtopon	\|- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
14		resttopon	\|- ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) \|`t S ) e. ( TopOn ` S ) )
15	13 1 14	sylancr	\|- ( ph -> ( ( TopOpen ` CCfld ) \|`t S ) e. ( TopOn ` S ) )
16		toponuni	\|- ( ( ( TopOpen ` CCfld ) \|`t S ) e. ( TopOn ` S ) -> S = U. ( ( TopOpen ` CCfld ) \|`t S ) )
17	15 16	syl	\|- ( ph -> S = U. ( ( TopOpen ` CCfld ) \|`t S ) )
18	3 17	sseqtrd	\|- ( ph -> A C_ U. ( ( TopOpen ` CCfld ) \|`t S ) )
19		eqid	\|- U. ( ( TopOpen ` CCfld ) \|`t S ) = U. ( ( TopOpen ` CCfld ) \|`t S )
20	19	ntrss2	\|- ( ( ( ( TopOpen ` CCfld ) \|`t S ) e. Top /\ A C_ U. ( ( TopOpen ` CCfld ) \|`t S ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) \|`t S ) ) ` A ) C_ A )
21	12 18 20	syl2anc	\|- ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) \|`t S ) ) ` A ) C_ A )
22	6 21	sstrd	\|- ( ph -> dom ( S _D F ) C_ A )

Metamath Proof Explorer

Theorem dvbss

Proof