Metamath Proof Explorer


Theorem 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 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 wksv f p | f Walks G p V
3 trliswlk f Trails G p f Walks G p
4 3 ssopab2i f p | f Trails G p f p | f Walks G p
5 2 4 ssexi f p | f Trails G p V
6 5 a1i f p | f Trails G p V
7 df-spths SPaths = g V f p | f Trails g p Fun p -1
8 1 6 7 fvmptopab SPaths G = f p | f Trails G p Fun p -1
9 8 mptru SPaths G = f p | f Trails G p Fun p -1