Detailed syntax breakdown of Definition df-clwwlk
| Step | Hyp | Ref
| Expression |
| 1 | | cclwwlk 30000 |
. 2
class
ClWWalks |
| 2 | | vg |
. . 3
setvar 𝑔 |
| 3 | | cvv 3480 |
. . 3
class
V |
| 4 | | vw |
. . . . . . 7
setvar 𝑤 |
| 5 | 4 | cv 1539 |
. . . . . 6
class 𝑤 |
| 6 | | c0 4333 |
. . . . . 6
class
∅ |
| 7 | 5, 6 | wne 2940 |
. . . . 5
wff 𝑤 ≠ ∅ |
| 8 | | vi |
. . . . . . . . . 10
setvar 𝑖 |
| 9 | 8 | cv 1539 |
. . . . . . . . 9
class 𝑖 |
| 10 | 9, 5 | cfv 6561 |
. . . . . . . 8
class (𝑤‘𝑖) |
| 11 | | c1 11156 |
. . . . . . . . . 10
class
1 |
| 12 | | caddc 11158 |
. . . . . . . . . 10
class
+ |
| 13 | 9, 11, 12 | co 7431 |
. . . . . . . . 9
class (𝑖 + 1) |
| 14 | 13, 5 | cfv 6561 |
. . . . . . . 8
class (𝑤‘(𝑖 + 1)) |
| 15 | 10, 14 | cpr 4628 |
. . . . . . 7
class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} |
| 16 | 2 | cv 1539 |
. . . . . . . 8
class 𝑔 |
| 17 | | cedg 29064 |
. . . . . . . 8
class
Edg |
| 18 | 16, 17 | cfv 6561 |
. . . . . . 7
class
(Edg‘𝑔) |
| 19 | 15, 18 | wcel 2108 |
. . . . . 6
wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) |
| 20 | | cc0 11155 |
. . . . . . 7
class
0 |
| 21 | | chash 14369 |
. . . . . . . . 9
class
♯ |
| 22 | 5, 21 | cfv 6561 |
. . . . . . . 8
class
(♯‘𝑤) |
| 23 | | cmin 11492 |
. . . . . . . 8
class
− |
| 24 | 22, 11, 23 | co 7431 |
. . . . . . 7
class
((♯‘𝑤)
− 1) |
| 25 | | cfzo 13694 |
. . . . . . 7
class
..^ |
| 26 | 20, 24, 25 | co 7431 |
. . . . . 6
class
(0..^((♯‘𝑤) − 1)) |
| 27 | 19, 8, 26 | wral 3061 |
. . . . 5
wff
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) |
| 28 | | clsw 14600 |
. . . . . . . 8
class
lastS |
| 29 | 5, 28 | cfv 6561 |
. . . . . . 7
class
(lastS‘𝑤) |
| 30 | 20, 5 | cfv 6561 |
. . . . . . 7
class (𝑤‘0) |
| 31 | 29, 30 | cpr 4628 |
. . . . . 6
class
{(lastS‘𝑤),
(𝑤‘0)} |
| 32 | 31, 18 | wcel 2108 |
. . . . 5
wff
{(lastS‘𝑤),
(𝑤‘0)} ∈
(Edg‘𝑔) |
| 33 | 7, 27, 32 | w3a 1087 |
. . . 4
wff (𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)) |
| 34 | | cvtx 29013 |
. . . . . 6
class
Vtx |
| 35 | 16, 34 | cfv 6561 |
. . . . 5
class
(Vtx‘𝑔) |
| 36 | 35 | cword 14552 |
. . . 4
class Word
(Vtx‘𝑔) |
| 37 | 33, 4, 36 | crab 3436 |
. . 3
class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))} |
| 38 | 2, 3, 37 | cmpt 5225 |
. 2
class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}) |
| 39 | 1, 38 | wceq 1540 |
1
wff ClWWalks =
(𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}) |