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

Definition df-cpn 22100
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  Dn
f ) `  x
)  e.  ( dom  f -cn-> CC ) } ) )
Distinct variable group:    f, s, x

Detailed syntax breakdown of Definition df-cpn
StepHypRef Expression
1 ccpn 22096 . 2  class  C^n
2 vs . . 3  setvar  s
3 cc 9491 . . . 4  class  CC
43cpw 4010 . . 3  class  ~P CC
5 vx . . . 4  setvar  x
6 cn0 10796 . . . 4  class  NN0
75cv 1378 . . . . . . 7  class  x
82cv 1378 . . . . . . . 8  class  s
9 vf . . . . . . . . 9  setvar  f
109cv 1378 . . . . . . . 8  class  f
11 cdvn 22095 . . . . . . . 8  class  Dn
128, 10, 11co 6285 . . . . . . 7  class  ( s  Dn f )
137, 12cfv 5588 . . . . . 6  class  ( ( s  Dn f ) `  x )
1410cdm 4999 . . . . . . 7  class  dom  f
15 ccncf 21207 . . . . . . 7  class  -cn->
1614, 3, 15co 6285 . . . . . 6  class  ( dom  f -cn-> CC )
1713, 16wcel 1767 . . . . 5  wff  ( ( s  Dn f ) `  x )  e.  ( dom  f -cn->
CC )
18 cpm 7422 . . . . . 6  class  ^pm
193, 8, 18co 6285 . . . . 5  class  ( CC 
^pm  s )
2017, 9, 19crab 2818 . . . 4  class  { f  e.  ( CC  ^pm  s )  |  ( ( s  Dn
f ) `  x
)  e.  ( dom  f -cn-> CC ) }
215, 6, 20cmpt 4505 . . 3  class  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  Dn
f ) `  x
)  e.  ( dom  f -cn-> CC ) } )
222, 4, 21cmpt 4505 . 2  class  ( s  e.  ~P CC  |->  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  Dn
f ) `  x
)  e.  ( dom  f -cn-> CC ) } ) )
231, 22wceq 1379 1  wff  C^n  =  ( s  e. 
~P CC  |->  ( x  e.  NN0  |->  { f  e.  ( CC  ^pm  s )  |  ( ( s  Dn
f ) `  x
)  e.  ( dom  f -cn-> CC ) } ) )
Colors of variables: wff setvar class
This definition is referenced by:  cpnfval  22162
  Copyright terms: Public domain W3C validator