Metamath Proof Explorer

Theorem dvbsss

Description: The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Assertion dvbsss 
|- dom ( S _D F ) C_ S

Proof

Step Hyp Ref Expression
1 df-dv 
 |-  _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) )
2 1 reldmmpo 
 |-  Rel dom _D
3 df-rel 
 |-  ( Rel dom _D <-> dom _D C_ ( _V X. _V ) )
4 2 3 mpbi 
 |-  dom _D C_ ( _V X. _V )
5 4 sseli 
 |-  ( <. S , F >. e. dom _D -> <. S , F >. e. ( _V X. _V ) )
6 opelxp1 
 |-  ( <. S , F >. e. ( _V X. _V ) -> S e. _V )
7 5 6 syl 
 |-  ( <. S , F >. e. dom _D -> S e. _V )
8 opeq1 
 |-  ( s = S -> <. s , F >. = <. S , F >. )
9 8 eleq1d 
 |-  ( s = S -> ( <. s , F >. e. dom _D <-> <. S , F >. e. dom _D ) )
10 eleq1 
 |-  ( s = S -> ( s e. ~P CC <-> S e. ~P CC ) )
11 oveq2 
 |-  ( s = S -> ( CC ^pm s ) = ( CC ^pm S ) )
12 11 eleq2d 
 |-  ( s = S -> ( F e. ( CC ^pm s ) <-> F e. ( CC ^pm S ) ) )
13 10 12 anbi12d 
 |-  ( s = S -> ( ( s e. ~P CC /\ F e. ( CC ^pm s ) ) <-> ( S e. ~P CC /\ F e. ( CC ^pm S ) ) ) )
14 9 13 imbi12d 
 |-  ( s = S -> ( ( <. s , F >. e. dom _D -> ( s e. ~P CC /\ F e. ( CC ^pm s ) ) ) <-> ( <. S , F >. e. dom _D -> ( S e. ~P CC /\ F e. ( CC ^pm S ) ) ) ) )
15 1 dmmpossx 
 |-  dom _D C_ U_ s e. ~P CC ( { s } X. ( CC ^pm s ) )
16 15 sseli 
 |-  ( <. s , F >. e. dom _D -> <. s , F >. e. U_ s e. ~P CC ( { s } X. ( CC ^pm s ) ) )
17 opeliunxp 
 |-  ( <. s , F >. e. U_ s e. ~P CC ( { s } X. ( CC ^pm s ) ) <-> ( s e. ~P CC /\ F e. ( CC ^pm s ) ) )
18 16 17 sylib 
 |-  ( <. s , F >. e. dom _D -> ( s e. ~P CC /\ F e. ( CC ^pm s ) ) )
19 14 18 vtoclg 
 |-  ( S e. _V -> ( <. S , F >. e. dom _D -> ( S e. ~P CC /\ F e. ( CC ^pm S ) ) ) )
20 7 19 mpcom 
 |-  ( <. S , F >. e. dom _D -> ( S e. ~P CC /\ F e. ( CC ^pm S ) ) )
21 20 simpld 
 |-  ( <. S , F >. e. dom _D -> S e. ~P CC )
22 21 elpwid 
 |-  ( <. S , F >. e. dom _D -> S C_ CC )
23 20 simprd 
 |-  ( <. S , F >. e. dom _D -> F e. ( CC ^pm S ) )
24 cnex 
 |-  CC e. _V
25 elpm2g 
 |-  ( ( CC e. _V /\ S e. ~P CC ) -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
26 24 21 25 sylancr 
 |-  ( <. S , F >. e. dom _D -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
27 23 26 mpbid 
 |-  ( <. S , F >. e. dom _D -> ( F : dom F --> CC /\ dom F C_ S ) )
28 27 simpld 
 |-  ( <. S , F >. e. dom _D -> F : dom F --> CC )
29 27 simprd 
 |-  ( <. S , F >. e. dom _D -> dom F C_ S )
30 22 28 29 dvbss 
 |-  ( <. S , F >. e. dom _D -> dom ( S _D F ) C_ dom F )
31 30 29 sstrd 
 |-  ( <. S , F >. e. dom _D -> dom ( S _D F ) C_ S )
32 df-ov 
 |-  ( S _D F ) = ( _D ` <. S , F >. )
33 ndmfv 
 |-  ( -. <. S , F >. e. dom _D -> ( _D ` <. S , F >. ) = (/) )
34 32 33 syl5eq 
 |-  ( -. <. S , F >. e. dom _D -> ( S _D F ) = (/) )
35 34 dmeqd 
 |-  ( -. <. S , F >. e. dom _D -> dom ( S _D F ) = dom (/) )
36 dm0 
 |-  dom (/) = (/)
37 35 36 eqtrdi 
 |-  ( -. <. S , F >. e. dom _D -> dom ( S _D F ) = (/) )
38 0ss 
 |-  (/) C_ S
39 37 38 eqsstrdi 
 |-  ( -. <. S , F >. e. dom _D -> dom ( S _D F ) C_ S )
40 31 39 pm2.61i 
 |-  dom ( S _D F ) C_ S