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=\left(s\in 𝒫ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\left(s{D}^{n}f\right)\left(x\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccpn	$$class{C}^n$$
1		vs	$$setvars$$
2		cc	$$classℂ$$
3	2	cpw	$$class𝒫ℂ$$
4		vx	$$setvarx$$
5		cn0	$$class{\mathbb{N}}_0$$
6		vf	$$setvarf$$
7		cpm	$$class{\uparrow }_{𝑝𝑚}$$
8	1	cv	$$setvars$$
9	2 8 7	co	$$class\left(ℂ{\uparrow }_{𝑝𝑚}s\right)$$
10		cdvn	$$class{D}^n$$
11	6	cv	$$setvarf$$
12	8 11 10	co	$$class\left(s{D}^{n}f\right)$$
13	4	cv	$$setvarx$$
14	13 12	cfv	$$class\left(s{D}^{n}f\right)\left(x\right)$$
15	11	cdm	$$class\mathrm{dom}f$$
16		ccncf	$$class\underset{cn}{⟶}$$
17	15 2 16	co	$$class\left(\mathrm{dom}f\underset{cn}{⟶}ℂ\right)$$
18	14 17	wcel	$$wff\left(s{D}^{n}f\right)\left(x\right):\mathrm{dom}f\underset{cn}{⟶}ℂ$$
19	18 6 9	crab	$$class\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\left(s{D}^{n}f\right)\left(x\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}$$
20	4 5 19	cmpt	$$class\left(x\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\left(s{D}^{n}f\right)\left(x\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)$$
21	1 3 20	cmpt	$$class\left(s\in 𝒫ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\left(s{D}^{n}f\right)\left(x\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)\right)$$
22	0 21	wceq	$$wff{C}^n=\left(s\in 𝒫ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\left(s{D}^{n}f\right)\left(x\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)\right)$$