Detailed syntax breakdown of Definition df-repr
Step | Hyp | Ref
| Expression |
1 | | crepr 32324 |
. 2
class
repr |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | cn0 12114 |
. . 3
class
ℕ0 |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | | vm |
. . . 4
setvar 𝑚 |
6 | | cn 11854 |
. . . . 5
class
ℕ |
7 | 6 | cpw 4527 |
. . . 4
class 𝒫
ℕ |
8 | | cz 12200 |
. . . 4
class
ℤ |
9 | | cc0 10753 |
. . . . . . . 8
class
0 |
10 | 2 | cv 1542 |
. . . . . . . 8
class 𝑠 |
11 | | cfzo 13262 |
. . . . . . . 8
class
..^ |
12 | 9, 10, 11 | co 7231 |
. . . . . . 7
class
(0..^𝑠) |
13 | | va |
. . . . . . . . 9
setvar 𝑎 |
14 | 13 | cv 1542 |
. . . . . . . 8
class 𝑎 |
15 | | vc |
. . . . . . . . 9
setvar 𝑐 |
16 | 15 | cv 1542 |
. . . . . . . 8
class 𝑐 |
17 | 14, 16 | cfv 6397 |
. . . . . . 7
class (𝑐‘𝑎) |
18 | 12, 17, 13 | csu 15273 |
. . . . . 6
class
Σ𝑎 ∈
(0..^𝑠)(𝑐‘𝑎) |
19 | 5 | cv 1542 |
. . . . . 6
class 𝑚 |
20 | 18, 19 | wceq 1543 |
. . . . 5
wff
Σ𝑎 ∈
(0..^𝑠)(𝑐‘𝑎) = 𝑚 |
21 | 4 | cv 1542 |
. . . . . 6
class 𝑏 |
22 | | cmap 8528 |
. . . . . 6
class
↑m |
23 | 21, 12, 22 | co 7231 |
. . . . 5
class (𝑏 ↑m (0..^𝑠)) |
24 | 20, 15, 23 | crab 3066 |
. . . 4
class {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚} |
25 | 4, 5, 7, 8, 24 | cmpo 7233 |
. . 3
class (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}) |
26 | 2, 3, 25 | cmpt 5149 |
. 2
class (𝑠 ∈ ℕ0
↦ (𝑏 ∈ 𝒫
ℕ, 𝑚 ∈ ℤ
↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚})) |
27 | 1, 26 | wceq 1543 |
1
wff repr =
(𝑠 ∈
ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚})) |