Detailed syntax breakdown of Definition df-wlkon
Step | Hyp | Ref
| Expression |
1 | | cwlkon 26030 |
. 2
class
WalkOn |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | ve |
. . 3
setvar 𝑒 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | va |
. . . 4
setvar 𝑎 |
6 | | vb |
. . . 4
setvar 𝑏 |
7 | 2 | cv 1474 |
. . . 4
class 𝑣 |
8 | | vf |
. . . . . . . 8
setvar 𝑓 |
9 | 8 | cv 1474 |
. . . . . . 7
class 𝑓 |
10 | | vp |
. . . . . . . 8
setvar 𝑝 |
11 | 10 | cv 1474 |
. . . . . . 7
class 𝑝 |
12 | 3 | cv 1474 |
. . . . . . . 8
class 𝑒 |
13 | | cwalk 26026 |
. . . . . . . 8
class
Walks |
14 | 7, 12, 13 | co 6549 |
. . . . . . 7
class (𝑣 Walks 𝑒) |
15 | 9, 11, 14 | wbr 4583 |
. . . . . 6
wff 𝑓(𝑣 Walks 𝑒)𝑝 |
16 | | cc0 9815 |
. . . . . . . 8
class
0 |
17 | 16, 11 | cfv 5804 |
. . . . . . 7
class (𝑝‘0) |
18 | 5 | cv 1474 |
. . . . . . 7
class 𝑎 |
19 | 17, 18 | wceq 1475 |
. . . . . 6
wff (𝑝‘0) = 𝑎 |
20 | | chash 12979 |
. . . . . . . . 9
class
# |
21 | 9, 20 | cfv 5804 |
. . . . . . . 8
class
(#‘𝑓) |
22 | 21, 11 | cfv 5804 |
. . . . . . 7
class (𝑝‘(#‘𝑓)) |
23 | 6 | cv 1474 |
. . . . . . 7
class 𝑏 |
24 | 22, 23 | wceq 1475 |
. . . . . 6
wff (𝑝‘(#‘𝑓)) = 𝑏 |
25 | 15, 19, 24 | w3a 1031 |
. . . . 5
wff (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏) |
26 | 25, 8, 10 | copab 4642 |
. . . 4
class
{〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)} |
27 | 5, 6, 7, 7, 26 | cmpt2 6551 |
. . 3
class (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}) |
28 | 2, 3, 4, 4, 27 | cmpt2 6551 |
. 2
class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) |
29 | 1, 28 | wceq 1475 |
1
wff WalkOn =
(𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) |