Step |
Hyp |
Ref |
Expression |
0 |
|
ctrlson |
⊢ TrailsOn |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvv |
⊢ V |
3 |
|
va |
⊢ 𝑎 |
4 |
|
cvtx |
⊢ Vtx |
5 |
1
|
cv |
⊢ 𝑔 |
6 |
5 4
|
cfv |
⊢ ( Vtx ‘ 𝑔 ) |
7 |
|
vb |
⊢ 𝑏 |
8 |
|
vf |
⊢ 𝑓 |
9 |
|
vp |
⊢ 𝑝 |
10 |
8
|
cv |
⊢ 𝑓 |
11 |
3
|
cv |
⊢ 𝑎 |
12 |
|
cwlkson |
⊢ WalksOn |
13 |
5 12
|
cfv |
⊢ ( WalksOn ‘ 𝑔 ) |
14 |
7
|
cv |
⊢ 𝑏 |
15 |
11 14 13
|
co |
⊢ ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) |
16 |
9
|
cv |
⊢ 𝑝 |
17 |
10 16 15
|
wbr |
⊢ 𝑓 ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) 𝑝 |
18 |
|
ctrls |
⊢ Trails |
19 |
5 18
|
cfv |
⊢ ( Trails ‘ 𝑔 ) |
20 |
10 16 19
|
wbr |
⊢ 𝑓 ( Trails ‘ 𝑔 ) 𝑝 |
21 |
17 20
|
wa |
⊢ ( 𝑓 ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ) |
22 |
21 8 9
|
copab |
⊢ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ) } |
23 |
3 7 6 6 22
|
cmpo |
⊢ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ) } ) |
24 |
1 2 23
|
cmpt |
⊢ ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ) } ) ) |
25 |
0 24
|
wceq |
⊢ TrailsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ) } ) ) |