Detailed syntax breakdown of Definition df-clwwlk
Step | Hyp | Ref
| Expression |
1 | | cclwwlk 26276 |
. 2
class
ClWWalks |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | ve |
. . 3
setvar 𝑒 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | vi |
. . . . . . . . . 10
setvar 𝑖 |
6 | 5 | cv 1474 |
. . . . . . . . 9
class 𝑖 |
7 | | vw |
. . . . . . . . . 10
setvar 𝑤 |
8 | 7 | cv 1474 |
. . . . . . . . 9
class 𝑤 |
9 | 6, 8 | cfv 5804 |
. . . . . . . 8
class (𝑤‘𝑖) |
10 | | c1 9816 |
. . . . . . . . . 10
class
1 |
11 | | caddc 9818 |
. . . . . . . . . 10
class
+ |
12 | 6, 10, 11 | co 6549 |
. . . . . . . . 9
class (𝑖 + 1) |
13 | 12, 8 | cfv 5804 |
. . . . . . . 8
class (𝑤‘(𝑖 + 1)) |
14 | 9, 13 | cpr 4127 |
. . . . . . 7
class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} |
15 | 3 | cv 1474 |
. . . . . . . 8
class 𝑒 |
16 | 15 | crn 5039 |
. . . . . . 7
class ran 𝑒 |
17 | 14, 16 | wcel 1977 |
. . . . . 6
wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 |
18 | | cc0 9815 |
. . . . . . 7
class
0 |
19 | | chash 12979 |
. . . . . . . . 9
class
# |
20 | 8, 19 | cfv 5804 |
. . . . . . . 8
class
(#‘𝑤) |
21 | | cmin 10145 |
. . . . . . . 8
class
− |
22 | 20, 10, 21 | co 6549 |
. . . . . . 7
class
((#‘𝑤) −
1) |
23 | | cfzo 12334 |
. . . . . . 7
class
..^ |
24 | 18, 22, 23 | co 6549 |
. . . . . 6
class
(0..^((#‘𝑤)
− 1)) |
25 | 17, 5, 24 | wral 2896 |
. . . . 5
wff
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 |
26 | | clsw 13147 |
. . . . . . . 8
class
lastS |
27 | 8, 26 | cfv 5804 |
. . . . . . 7
class ( lastS
‘𝑤) |
28 | 18, 8 | cfv 5804 |
. . . . . . 7
class (𝑤‘0) |
29 | 27, 28 | cpr 4127 |
. . . . . 6
class {( lastS
‘𝑤), (𝑤‘0)} |
30 | 29, 16 | wcel 1977 |
. . . . 5
wff {( lastS
‘𝑤), (𝑤‘0)} ∈ ran 𝑒 |
31 | 25, 30 | wa 383 |
. . . 4
wff
(∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒) |
32 | 2 | cv 1474 |
. . . . 5
class 𝑣 |
33 | 32 | cword 13146 |
. . . 4
class Word
𝑣 |
34 | 31, 7, 33 | crab 2900 |
. . 3
class {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)} |
35 | 2, 3, 4, 4, 34 | cmpt2 6551 |
. 2
class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)}) |
36 | 1, 35 | wceq 1475 |
1
wff ClWWalks =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)}) |