Metamath Proof Explorer

Theorem dvnbss

Description: The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnbss 
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> dom ( ( S Dn F ) ` N ) C_ dom F )

Proof

Step Hyp Ref Expression
1 dvnff 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) : NN0 --> ( CC ^pm dom F ) )
2 1 ffvelrnda 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) e. ( CC ^pm dom F ) )
3 2 3impa 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) e. ( CC ^pm dom F ) )
4 cnex 
 |-  CC e. _V
5 simp2 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> F e. ( CC ^pm S ) )
6 5 dmexd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> dom F e. _V )
7 elpm2g 
 |-  ( ( CC e. _V /\ dom F e. _V ) -> ( ( ( S Dn F ) ` N ) e. ( CC ^pm dom F ) <-> ( ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC /\ dom ( ( S Dn F ) ` N ) C_ dom F ) ) )
8 4 6 7 sylancr 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( ( S Dn F ) ` N ) e. ( CC ^pm dom F ) <-> ( ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC /\ dom ( ( S Dn F ) ` N ) C_ dom F ) ) )
9 3 8 mpbid 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC /\ dom ( ( S Dn F ) ` N ) C_ dom F ) )
10 9 simprd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> dom ( ( S Dn F ) ` N ) C_ dom F )