Definition df-cpn 23439

Description: Define the set of 𝑛-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.)

Assertion

Ref	Expression
df-cpn	⊢ Cn = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}))

Distinct variable group:   𝑓,𝑠,𝑥

Detailed syntax breakdown of Definition df-cpn

Step	Hyp	Ref	Expression
1		ccpn 23435	. 2 class Cn
2		vs	. . 3 setvar 𝑠
3		cc 9813	. . . 4 class ℂ
4	3	cpw 4108	. . 3 class 𝒫 ℂ
5		vx	. . . 4 setvar 𝑥
6		cn0 11169	. . . 4 class ℕ0
7	5	cv 1474	. . . . . . 7 class 𝑥
8	2	cv 1474	. . . . . . . 8 class 𝑠
9		vf	. . . . . . . . 9 setvar 𝑓
10	9	cv 1474	. . . . . . . 8 class 𝑓
11		cdvn 23434	. . . . . . . 8 class D𝑛
12	8, 10, 11	co 6549	. . . . . . 7 class (𝑠 D𝑛 𝑓)
13	7, 12	cfv 5804	. . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑥)
14	10	cdm 5038	. . . . . . 7 class dom 𝑓
15		ccncf 22487	. . . . . . 7 class –cn→
16	14, 3, 15	co 6549	. . . . . 6 class (dom 𝑓–cn→ℂ)
17	13, 16	wcel 1977	. . . . 5 wff ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)
18		cpm 7745	. . . . . 6 class ↑pm
19	3, 8, 18	co 6549	. . . . 5 class (ℂ ↑pm 𝑠)
20	17, 9, 19	crab 2900	. . . 4 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}
21	5, 6, 20	cmpt 4643	. . 3 class (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})
22	2, 4, 21	cmpt 4643	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}))
23	1, 22	wceq 1475	1 wff Cn = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}))

This definition is referenced by:  cpnfval  23501