Detailed syntax breakdown of Definition df-clwwlkn
Step | Hyp | Ref
| Expression |
1 | | cclwwlkn 26277 |
. 2
class
ClWWalksN |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | ve |
. . 3
setvar 𝑒 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | vn |
. . . 4
setvar 𝑛 |
6 | | cn0 11169 |
. . . 4
class
ℕ0 |
7 | | vw |
. . . . . . . 8
setvar 𝑤 |
8 | 7 | cv 1474 |
. . . . . . 7
class 𝑤 |
9 | | chash 12979 |
. . . . . . 7
class
# |
10 | 8, 9 | cfv 5804 |
. . . . . 6
class
(#‘𝑤) |
11 | 5 | cv 1474 |
. . . . . 6
class 𝑛 |
12 | 10, 11 | wceq 1475 |
. . . . 5
wff
(#‘𝑤) = 𝑛 |
13 | 2 | cv 1474 |
. . . . . 6
class 𝑣 |
14 | 3 | cv 1474 |
. . . . . 6
class 𝑒 |
15 | | cclwwlk 26276 |
. . . . . 6
class
ClWWalks |
16 | 13, 14, 15 | co 6549 |
. . . . 5
class (𝑣 ClWWalks 𝑒) |
17 | 12, 7, 16 | crab 2900 |
. . . 4
class {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛} |
18 | 5, 6, 17 | cmpt 4643 |
. . 3
class (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛}) |
19 | 2, 3, 4, 4, 18 | cmpt2 6551 |
. 2
class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛})) |
20 | 1, 19 | wceq 1475 |
1
wff ClWWalksN
= (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛})) |