Detailed syntax breakdown of Definition df-cpn
Step | Hyp | Ref
| Expression |
1 | | ccpn 24629 |
. 2
class
𝓑C𝑛 |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | cc 10625 |
. . . 4
class
ℂ |
4 | 3 | cpw 4498 |
. . 3
class 𝒫
ℂ |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | | cn0 11988 |
. . . 4
class
ℕ0 |
7 | 5 | cv 1541 |
. . . . . . 7
class 𝑥 |
8 | 2 | cv 1541 |
. . . . . . . 8
class 𝑠 |
9 | | vf |
. . . . . . . . 9
setvar 𝑓 |
10 | 9 | cv 1541 |
. . . . . . . 8
class 𝑓 |
11 | | cdvn 24628 |
. . . . . . . 8
class
D𝑛 |
12 | 8, 10, 11 | co 7182 |
. . . . . . 7
class (𝑠 D𝑛 𝑓) |
13 | 7, 12 | cfv 6349 |
. . . . . 6
class ((𝑠 D𝑛 𝑓)‘𝑥) |
14 | 10 | cdm 5535 |
. . . . . . 7
class dom 𝑓 |
15 | | ccncf 23640 |
. . . . . . 7
class
–cn→ |
16 | 14, 3, 15 | co 7182 |
. . . . . 6
class (dom
𝑓–cn→ℂ) |
17 | 13, 16 | wcel 2114 |
. . . . 5
wff ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ) |
18 | | cpm 8450 |
. . . . . 6
class
↑pm |
19 | 3, 8, 18 | co 7182 |
. . . . 5
class (ℂ
↑pm 𝑠) |
20 | 17, 9, 19 | crab 3058 |
. . . 4
class {𝑓 ∈ (ℂ
↑pm 𝑠)
∣ ((𝑠
D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)} |
21 | 5, 6, 20 | cmpt 5120 |
. . 3
class (𝑥 ∈ ℕ0
↦ {𝑓 ∈ (ℂ
↑pm 𝑠)
∣ ((𝑠
D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}) |
22 | 2, 4, 21 | cmpt 5120 |
. 2
class (𝑠 ∈ 𝒫 ℂ
↦ (𝑥 ∈
ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})) |
23 | 1, 22 | wceq 1542 |
1
wff
𝓑C𝑛 = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0
↦ {𝑓 ∈ (ℂ
↑pm 𝑠)
∣ ((𝑠
D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})) |