Detailed syntax breakdown of Definition df-cpn
Step | Hyp | Ref
| Expression |
1 | | ccpn 23629 |
. 2
class
Cn |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | cc 9934 |
. . . 4
class
ℂ |
4 | 3 | cpw 4158 |
. . 3
class 𝒫
ℂ |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | | cn0 11292 |
. . . 4
class
ℕ0 |
7 | 5 | cv 1482 |
. . . . . . 7
class 𝑥 |
8 | 2 | cv 1482 |
. . . . . . . 8
class 𝑠 |
9 | | vf |
. . . . . . . . 9
setvar 𝑓 |
10 | 9 | cv 1482 |
. . . . . . . 8
class 𝑓 |
11 | | cdvn 23628 |
. . . . . . . 8
class
D𝑛 |
12 | 8, 10, 11 | co 6650 |
. . . . . . 7
class (𝑠 D𝑛 𝑓) |
13 | 7, 12 | cfv 5888 |
. . . . . 6
class ((𝑠 D𝑛 𝑓)‘𝑥) |
14 | 10 | cdm 5114 |
. . . . . . 7
class dom 𝑓 |
15 | | ccncf 22679 |
. . . . . . 7
class
–cn→ |
16 | 14, 3, 15 | co 6650 |
. . . . . 6
class (dom
𝑓–cn→ℂ) |
17 | 13, 16 | wcel 1990 |
. . . . 5
wff ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ) |
18 | | cpm 7858 |
. . . . . 6
class
↑pm |
19 | 3, 8, 18 | co 6650 |
. . . . 5
class (ℂ
↑pm 𝑠) |
20 | 17, 9, 19 | crab 2916 |
. . . 4
class {𝑓 ∈ (ℂ
↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)} |
21 | 5, 6, 20 | cmpt 4729 |
. . 3
class (𝑥 ∈ ℕ0
↦ {𝑓 ∈ (ℂ
↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}) |
22 | 2, 4, 21 | cmpt 4729 |
. 2
class (𝑠 ∈ 𝒫 ℂ
↦ (𝑥 ∈
ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm
𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})) |
23 | 1, 22 | wceq 1483 |
1
wff
Cn = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0
↦ {𝑓 ∈ (ℂ
↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)})) |