This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Paths and simple paths spthsfval
Description: The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens , 21-Oct-2017) (Revised by AV , 9-Jan-2021)
(Revised by AV , 29-Oct-2021)
Ref
Expression
Assertion
spthsfval ⊢ ( SPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) }
Proof
Step
Hyp
Ref
Expression
1
biidd ⊢ ( 𝑔 = 𝐺 → ( Fun ◡ 𝑝 ↔ Fun ◡ 𝑝 ) )
2
df-spths ⊢ SPaths = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ Fun ◡ 𝑝 ) } )
3
1 2
fvmptopab ⊢ ( SPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) }