Detailed syntax breakdown of Definition df-wwlkn
Step | Hyp | Ref
| Expression |
1 | | cwwlkn 26206 |
. 2
class
WWalksN |
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 |
. . . . . . 7
class 𝑛 |
12 | | c1 9816 |
. . . . . . 7
class
1 |
13 | | caddc 9818 |
. . . . . . 7
class
+ |
14 | 11, 12, 13 | co 6549 |
. . . . . 6
class (𝑛 + 1) |
15 | 10, 14 | wceq 1475 |
. . . . 5
wff
(#‘𝑤) = (𝑛 + 1) |
16 | 2 | cv 1474 |
. . . . . 6
class 𝑣 |
17 | 3 | cv 1474 |
. . . . . 6
class 𝑒 |
18 | | cwwlk 26205 |
. . . . . 6
class
WWalks |
19 | 16, 17, 18 | co 6549 |
. . . . 5
class (𝑣 WWalks 𝑒) |
20 | 15, 7, 19 | crab 2900 |
. . . 4
class {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)} |
21 | 5, 6, 20 | cmpt 4643 |
. . 3
class (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)}) |
22 | 2, 3, 4, 4, 21 | cmpt2 6551 |
. 2
class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)})) |
23 | 1, 22 | wceq 1475 |
1
wff WWalksN =
(𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)})) |