Definition df-cpn 24938

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

Assertion

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

Distinct variable group:   𝑓,𝑠,𝑥

Detailed syntax breakdown of Definition df-cpn

Step	Hyp	Ref	Expression
1		ccpn 24934	. 2 class 𝓑C𝑛
2		vs	. . 3 setvar 𝑠
3		cc 10800	. . . 4 class ℂ
4	3	cpw 4530	. . 3 class 𝒫 ℂ
5		vx	. . . 4 setvar 𝑥
6		cn0 12163	. . . 4 class ℕ0
7	5	cv 1538	. . . . . . 7 class 𝑥
8	2	cv 1538	. . . . . . . 8 class 𝑠
9		vf	. . . . . . . . 9 setvar 𝑓
10	9	cv 1538	. . . . . . . 8 class 𝑓
11		cdvn 24933	. . . . . . . 8 class D𝑛
12	8, 10, 11	co 7255	. . . . . . 7 class (𝑠 D𝑛 𝑓)
13	7, 12	cfv 6418	. . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑥)
14	10	cdm 5580	. . . . . . 7 class dom 𝑓
15		ccncf 23945	. . . . . . 7 class –cn→
16	14, 3, 15	co 7255	. . . . . 6 class (dom 𝑓–cn→ℂ)
17	13, 16	wcel 2108	. . . . 5 wff ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)
18		cpm 8574	. . . . . 6 class ↑pm
19	3, 8, 18	co 7255	. . . . 5 class (ℂ ↑pm 𝑠)
20	17, 9, 19	crab 3067	. . . 4 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}
21	5, 6, 20	cmpt 5153	. . 3 class (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})
22	2, 4, 21	cmpt 5153	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}))
23	1, 22	wceq 1539	1 wff 𝓑C𝑛 = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}))

This definition is referenced by:  cpnfval  25001