Metamath Proof Explorer

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 
|- ( 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 )