Metamath Proof Explorer

Theorem cpnfval

Description: Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion cpnfval 
|- ( S C_ CC -> ( C^n ` S ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 1 elpw2 
 |-  ( S e. ~P CC <-> S C_ CC )
3 oveq2 
 |-  ( s = S -> ( CC ^pm s ) = ( CC ^pm S ) )
4 oveq1 
 |-  ( s = S -> ( s Dn f ) = ( S Dn f ) )
5 4 fveq1d 
 |-  ( s = S -> ( ( s Dn f ) ` n ) = ( ( S Dn f ) ` n ) )
6 5 eleq1d 
 |-  ( s = S -> ( ( ( s Dn f ) ` n ) e. ( dom f -cn-> CC ) <-> ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) ) )
7 3 6 rabeqbidv 
 |-  ( s = S -> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` n ) e. ( dom f -cn-> CC ) } = { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } )
8 7 mpteq2dv 
 |-  ( s = S -> ( n e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )
9 df-cpn 
 |-  C^n = ( s e. ~P CC |-> ( n e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )
10 nn0ex 
 |-  NN0 e. _V
11 10 mptex 
 |-  ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) e. _V
12 8 9 11 fvmpt 
 |-  ( S e. ~P CC -> ( C^n ` S ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )
13 2 12 sylbir 
 |-  ( S C_ CC -> ( C^n ` S ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )