Detailed syntax breakdown of Definition df-pthon
Step | Hyp | Ref
| Expression |
1 | | cpthon 26032 |
. 2
class
PathOn |
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 | 5 | cv 1474 |
. . . . . . . 8
class 𝑎 |
13 | 6 | cv 1474 |
. . . . . . . 8
class 𝑏 |
14 | 3 | cv 1474 |
. . . . . . . . 9
class 𝑒 |
15 | | cwlkon 26030 |
. . . . . . . . 9
class
WalkOn |
16 | 7, 14, 15 | co 6549 |
. . . . . . . 8
class (𝑣 WalkOn 𝑒) |
17 | 12, 13, 16 | co 6549 |
. . . . . . 7
class (𝑎(𝑣 WalkOn 𝑒)𝑏) |
18 | 9, 11, 17 | wbr 4583 |
. . . . . 6
wff 𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 |
19 | | cpath 26028 |
. . . . . . . 8
class
Paths |
20 | 7, 14, 19 | co 6549 |
. . . . . . 7
class (𝑣 Paths 𝑒) |
21 | 9, 11, 20 | wbr 4583 |
. . . . . 6
wff 𝑓(𝑣 Paths 𝑒)𝑝 |
22 | 18, 21 | wa 383 |
. . . . 5
wff (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Paths 𝑒)𝑝) |
23 | 22, 8, 10 | copab 4642 |
. . . 4
class
{〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Paths 𝑒)𝑝)} |
24 | 5, 6, 7, 7, 23 | cmpt2 6551 |
. . 3
class (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Paths 𝑒)𝑝)}) |
25 | 2, 3, 4, 4, 24 | cmpt2 6551 |
. 2
class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Paths 𝑒)𝑝)})) |
26 | 1, 25 | wceq 1475 |
1
wff PathOn =
(𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Paths 𝑒)𝑝)})) |