Detailed syntax breakdown of Definition df-pthson
Step | Hyp | Ref
| Expression |
1 | | cpthson 28078 |
. 2
class
PathsOn |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | va |
. . . 4
setvar 𝑎 |
5 | | vb |
. . . 4
setvar 𝑏 |
6 | 2 | cv 1541 |
. . . . 5
class 𝑔 |
7 | | cvtx 27364 |
. . . . 5
class
Vtx |
8 | 6, 7 | cfv 6432 |
. . . 4
class
(Vtx‘𝑔) |
9 | | vf |
. . . . . . . 8
setvar 𝑓 |
10 | 9 | cv 1541 |
. . . . . . 7
class 𝑓 |
11 | | vp |
. . . . . . . 8
setvar 𝑝 |
12 | 11 | cv 1541 |
. . . . . . 7
class 𝑝 |
13 | 4 | cv 1541 |
. . . . . . . 8
class 𝑎 |
14 | 5 | cv 1541 |
. . . . . . . 8
class 𝑏 |
15 | | ctrlson 28056 |
. . . . . . . . 9
class
TrailsOn |
16 | 6, 15 | cfv 6432 |
. . . . . . . 8
class
(TrailsOn‘𝑔) |
17 | 13, 14, 16 | co 7271 |
. . . . . . 7
class (𝑎(TrailsOn‘𝑔)𝑏) |
18 | 10, 12, 17 | wbr 5079 |
. . . . . 6
wff 𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 |
19 | | cpths 28076 |
. . . . . . . 8
class
Paths |
20 | 6, 19 | cfv 6432 |
. . . . . . 7
class
(Paths‘𝑔) |
21 | 10, 12, 20 | wbr 5079 |
. . . . . 6
wff 𝑓(Paths‘𝑔)𝑝 |
22 | 18, 21 | wa 396 |
. . . . 5
wff (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝) |
23 | 22, 9, 11 | copab 5141 |
. . . 4
class
{〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)} |
24 | 4, 5, 8, 8, 23 | cmpo 7273 |
. . 3
class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)}) |
25 | 2, 3, 24 | cmpt 5162 |
. 2
class (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)})) |
26 | 1, 25 | wceq 1542 |
1
wff PathsOn =
(𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)})) |