Metamath Proof Explorer

Theorem elcpn

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 elcpn 
|- ( ( S C_ CC /\ N e. NN0 ) -> ( F e. ( ( C^n ` S ) ` N ) <-> ( F e. ( CC ^pm S ) /\ ( ( S Dn F ) ` N ) e. ( dom F -cn-> CC ) ) ) )

Proof

Step Hyp Ref Expression
1 cpnfval 
 |-  ( S C_ CC -> ( C^n ` S ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )
2 1 fveq1d 
 |-  ( S C_ CC -> ( ( C^n ` S ) ` N ) = ( ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) ` N ) )
3 fveq2 
 |-  ( n = N -> ( ( S Dn f ) ` n ) = ( ( S Dn f ) ` N ) )
4 3 eleq1d 
 |-  ( n = N -> ( ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) <-> ( ( S Dn f ) ` N ) e. ( dom f -cn-> CC ) ) )
5 4 rabbidv 
 |-  ( n = N -> { 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 ) } )
6 eqid 
 |-  ( 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 ) } )
7 ovex 
 |-  ( CC ^pm S ) e. _V
8 7 rabex 
 |-  { f e. ( CC ^pm S ) | ( ( S Dn f ) ` N ) e. ( dom f -cn-> CC ) } e. _V
9 5 6 8 fvmpt 
 |-  ( N e. NN0 -> ( ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) ` N ) = { f e. ( CC ^pm S ) | ( ( S Dn f ) ` N ) e. ( dom f -cn-> CC ) } )
10 2 9 sylan9eq 
 |-  ( ( S C_ CC /\ N e. NN0 ) -> ( ( C^n ` S ) ` N ) = { f e. ( CC ^pm S ) | ( ( S Dn f ) ` N ) e. ( dom f -cn-> CC ) } )
11 10 eleq2d 
 |-  ( ( S C_ CC /\ N e. NN0 ) -> ( F e. ( ( C^n ` S ) ` N ) <-> F e. { f e. ( CC ^pm S ) | ( ( S Dn f ) ` N ) e. ( dom f -cn-> CC ) } ) )
12 oveq2 
 |-  ( f = F -> ( S Dn f ) = ( S Dn F ) )
13 12 fveq1d 
 |-  ( f = F -> ( ( S Dn f ) ` N ) = ( ( S Dn F ) ` N ) )
14 dmeq 
 |-  ( f = F -> dom f = dom F )
15 14 oveq1d 
 |-  ( f = F -> ( dom f -cn-> CC ) = ( dom F -cn-> CC ) )
16 13 15 eleq12d 
 |-  ( f = F -> ( ( ( S Dn f ) ` N ) e. ( dom f -cn-> CC ) <-> ( ( S Dn F ) ` N ) e. ( dom F -cn-> CC ) ) )
17 16 elrab 
 |-  ( F e. { 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 ) ) )
18 11 17 bitrdi 
 |-  ( ( S C_ CC /\ N e. NN0 ) -> ( F e. ( ( C^n ` S ) ` N ) <-> ( F e. ( CC ^pm S ) /\ ( ( S Dn F ) ` N ) e. ( dom F -cn-> CC ) ) ) )