Step |
Hyp |
Ref |
Expression |
1 |
|
biidd |
⊢ ( ( ⊤ ∧ 𝑔 = 𝐺 ) → ( Fun ◡ 𝑝 ↔ Fun ◡ 𝑝 ) ) |
2 |
|
wksv |
⊢ { 〈 𝑓 , 𝑝 〉 ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V |
3 |
|
trliswlk |
⊢ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) |
4 |
3
|
ssopab2i |
⊢ { 〈 𝑓 , 𝑝 〉 ∣ 𝑓 ( Trails ‘ 𝐺 ) 𝑝 } ⊆ { 〈 𝑓 , 𝑝 〉 ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } |
5 |
2 4
|
ssexi |
⊢ { 〈 𝑓 , 𝑝 〉 ∣ 𝑓 ( Trails ‘ 𝐺 ) 𝑝 } ∈ V |
6 |
5
|
a1i |
⊢ ( ⊤ → { 〈 𝑓 , 𝑝 〉 ∣ 𝑓 ( Trails ‘ 𝐺 ) 𝑝 } ∈ V ) |
7 |
|
df-spths |
⊢ SPaths = ( 𝑔 ∈ V ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ Fun ◡ 𝑝 ) } ) |
8 |
1 6 7
|
fvmptopab |
⊢ ( ⊤ → ( SPaths ‘ 𝐺 ) = { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } ) |
9 |
8
|
mptru |
⊢ ( SPaths ‘ 𝐺 ) = { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } |