Database
GRAPH THEORY
Walks, paths and cycles
Paths and simple paths
spthsfval
Metamath Proof Explorer
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 ⁡ G = f p | f Trails ⁡ G p ∧ Fun ⁡ p -1
Proof
Step
Hyp
Ref
Expression
1
biidd
⊢ g = G → Fun ⁡ p -1 ↔ Fun ⁡ p -1
2
df-spths
⊢ SPaths = g ∈ V ⟼ f p | f Trails ⁡ g p ∧ Fun ⁡ p -1
3
1 2
fvmptopab
⊢ SPaths ⁡ G = f p | f Trails ⁡ G p ∧ Fun ⁡ p -1