Definition df-cpn 23633

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

Step	Hyp	Ref	Expression
1		ccpn 23629	. 2 class C^n
2		vs	. . 3 setvar s
3		cc 9934	. . . 4 class CC
4	3	cpw 4158	. . 3 class ~P CC
5		vx	. . . 4 setvar x
6		cn0 11292	. . . 4 class NN0
7	5	cv 1482	. . . . . . 7 class x
8	2	cv 1482	. . . . . . . 8 class s
9		vf	. . . . . . . . 9 setvar f
10	9	cv 1482	. . . . . . . 8 class f
11		cdvn 23628	. . . . . . . 8 class Dn
12	8, 10, 11	co 6650	. . . . . . 7 class ( s Dn f )
13	7, 12	cfv 5888	. . . . . 6 class ( ( s Dn f ) ` x )
14	10	cdm 5114	. . . . . . 7 class dom f
15		ccncf 22679	. . . . . . 7 class -cn->
16	14, 3, 15	co 6650	. . . . . 6 class ( dom f -cn-> CC )
17	13, 16	wcel 1990	. . . . 5 wff ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC )
18		cpm 7858	. . . . . 6 class ^pm
19	3, 8, 18	co 6650	. . . . 5 class ( CC ^pm s )
20	17, 9, 19	crab 2916	. . . 4 class { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) }
21	5, 6, 20	cmpt 4729	. . 3 class ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } )
22	2, 4, 21	cmpt 4729	. 2 class ( s e. ~P CC |-> ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } ) )
23	1, 22	wceq 1483	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 ) } ) )

This definition is referenced by:  cpnfval  23695