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

Definition df-cpn 19625
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 19621 . 2  class  C ^n
2 vs . . 3  set  s
3 cc 8923 . . . 4  class  CC
43cpw 3744 . . 3  class  ~P CC
5 vx . . . 4  set  x
6 cn0 10155 . . . 4  class  NN0
75cv 1648 . . . . . . 7  class  x
82cv 1648 . . . . . . . 8  class  s
9 vf . . . . . . . . 9  set  f
109cv 1648 . . . . . . . 8  class  f
11 cdvn 19620 . . . . . . . 8  class  D n
128, 10, 11co 6022 . . . . . . 7  class  ( s  D n f )
137, 12cfv 5396 . . . . . 6  class  ( ( s  D n f ) `  x )
1410cdm 4820 . . . . . . 7  class  dom  f
15 ccncf 18779 . . . . . . 7  class  -cn->
1614, 3, 15co 6022 . . . . . 6  class  ( dom  f -cn-> CC )
1713, 16wcel 1717 . . . . 5  wff  ( ( s  D n f ) `  x )  e.  ( dom  f -cn->
CC )
18 cpm 6957 . . . . . 6  class  ^pm
193, 8, 18co 6022 . . . . 5  class  ( CC 
^pm  s )
2017, 9, 19crab 2655 . . . 4  class  { f  e.  ( CC  ^pm  s )  |  ( ( s  D n
f ) `  x
)  e.  ( dom  f -cn-> CC ) }
215, 6, 20cmpt 4209 . . 3  class  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  D n
f ) `  x
)  e.  ( dom  f -cn-> CC ) } )
222, 4, 21cmpt 4209 . 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 1649 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  19687
  Copyright terms: Public domain W3C validator