Metamath Proof Explorer

Definition df-cpn

Description: Define the set of n -times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014)

Ref Expression
Assertion df-cpn 
|- C^n = ( s e. ~P CC |-> ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccpn 
 |-  C^n
1 vs 
 |-  s
2 cc 
 |-  CC
3 2 cpw 
 |-  ~P CC
4 vx 
 |-  x
5 cn0 
 |-  NN0
6 vf 
 |-  f
7 cpm 
 |-  ^pm
8 1 cv 
 |-  s
9 2 8 7 co 
 |-  ( CC ^pm s )
10 cdvn 
 |-  Dn
11 6 cv 
 |-  f
12 8 11 10 co 
 |-  ( s Dn f )
13 4 cv 
 |-  x
14 13 12 cfv 
 |-  ( ( s Dn f ) ` x )
15 11 cdm 
 |-  dom f
16 ccncf 
 |-  -cn->
17 15 2 16 co 
 |-  ( dom f -cn-> CC )
18 14 17 wcel 
 |-  ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC )
19 18 6 9 crab 
 |-  { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) }
20 4 5 19 cmpt 
 |-  ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } )
21 1 3 20 cmpt 
 |-  ( s e. ~P CC |-> ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } ) )
22 0 21 wceq 
 |-  C^n = ( s e. ~P CC |-> ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } ) )