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

Definition df-cpn 24633
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
StepHypRef Expression
1 ccpn 24629 . 2 class 𝓑C𝑛
2 vs . . 3 setvar 𝑠
3 cc 10625 . . . 4 class
43cpw 4498 . . 3 class 𝒫 ℂ
5 vx . . . 4 setvar 𝑥
6 cn0 11988 . . . 4 class 0
75cv 1541 . . . . . . 7 class 𝑥
82cv 1541 . . . . . . . 8 class 𝑠
9 vf . . . . . . . . 9 setvar 𝑓
109cv 1541 . . . . . . . 8 class 𝑓
11 cdvn 24628 . . . . . . . 8 class D𝑛
128, 10, 11co 7182 . . . . . . 7 class (𝑠 D𝑛 𝑓)
137, 12cfv 6349 . . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑥)
1410cdm 5535 . . . . . . 7 class dom 𝑓
15 ccncf 23640 . . . . . . 7 class cn
1614, 3, 15co 7182 . . . . . 6 class (dom 𝑓cn→ℂ)
1713, 16wcel 2114 . . . . 5 wff ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓cn→ℂ)
18 cpm 8450 . . . . . 6 class pm
193, 8, 18co 7182 . . . . 5 class (ℂ ↑pm 𝑠)
2017, 9, 19crab 3058 . . . 4 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓cn→ℂ)}
215, 6, 20cmpt 5120 . . 3 class (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓cn→ℂ)})
222, 4, 21cmpt 5120 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓cn→ℂ)}))
231, 22wceq 1542 1 wff 𝓑C𝑛 = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓cn→ℂ)}))
Colors of variables: wff setvar class
This definition is referenced by:  cpnfval  24696
  Copyright terms: Public domain W3C validator