MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cpn Unicode version

Definition df-cpn 19219
Description: Define the set of  n-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.)
Assertion
Ref Expression
df-cpn  |-  C ^n  =  ( s  e. 
~P CC  |->  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  D n
f ) `  x
)  e.  ( dom  f -cn-> CC ) } ) )
Distinct variable group:    f, s, x

Detailed syntax breakdown of Definition df-cpn
StepHypRef Expression
1 ccpn 19215 . 2  class  C ^n
2 vs . . 3  set  s
3 cc 8735 . . . 4  class  CC
43cpw 3625 . . 3  class  ~P CC
5 vx . . . 4  set  x
6 cn0 9965 . . . 4  class  NN0
75cv 1622 . . . . . . 7  class  x
82cv 1622 . . . . . . . 8  class  s
9 vf . . . . . . . . 9  set  f
109cv 1622 . . . . . . . 8  class  f
11 cdvn 19214 . . . . . . . 8  class  D n
128, 10, 11co 5858 . . . . . . 7  class  ( s  D n f )
137, 12cfv 5255 . . . . . 6  class  ( ( s  D n f ) `  x )
1410cdm 4689 . . . . . . 7  class  dom  f
15 ccncf 18380 . . . . . . 7  class  -cn->
1614, 3, 15co 5858 . . . . . 6  class  ( dom  f -cn-> CC )
1713, 16wcel 1684 . . . . 5  wff  ( ( s  D n f ) `  x )  e.  ( dom  f -cn->
CC )
18 cpm 6773 . . . . . 6  class  ^pm
193, 8, 18co 5858 . . . . 5  class  ( CC 
^pm  s )
2017, 9, 19crab 2547 . . . 4  class  { f  e.  ( CC  ^pm  s )  |  ( ( s  D n
f ) `  x
)  e.  ( dom  f -cn-> CC ) }
215, 6, 20cmpt 4077 . . 3  class  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  D n
f ) `  x
)  e.  ( dom  f -cn-> CC ) } )
222, 4, 21cmpt 4077 . 2  class  ( s  e.  ~P CC  |->  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  D n
f ) `  x
)  e.  ( dom  f -cn-> CC ) } ) )
231, 22wceq 1623 1  wff  C ^n  =  ( s  e. 
~P CC  |->  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  D n
f ) `  x
)  e.  ( dom  f -cn-> CC ) } ) )
Colors of variables: wff set class
This definition is referenced by:  cpnfval  19281
  Copyright terms: Public domain W3C validator