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 )`
` |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ A C_ U. ( ( TopOpen ` CCfld ) |`t S ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) C_ A )`
` |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) C_ A )`
` |-  ( ph -> dom ( S _D F ) C_ A )`