Database
GRAPH THEORY
Walks, paths and cycles
Trails
trlsfval
Metamath Proof Explorer
Description: The set of trails (in an undirected graph). (Contributed by Alexander
van der Vekens , 20-Oct-2017) (Revised by AV , 28-Dec-2020) (Revised by AV , 29-Oct-2021)
Ref
Expression
Assertion
trlsfval
⊢ Trails ⁡ G = f p | f Walks ⁡ G p ∧ Fun ⁡ f -1
Proof
Step
Hyp
Ref
Expression
1
biidd
⊢ g = G → Fun ⁡ f -1 ↔ Fun ⁡ f -1
2
df-trls
⊢ Trails = g ∈ V ⟼ f p | f Walks ⁡ g p ∧ Fun ⁡ f -1
3
1 2
fvmptopab
⊢ Trails ⁡ G = f p | f Walks ⁡ G p ∧ Fun ⁡ f -1