Metamath Proof Explorer


Theorem pthsfval

Description: The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion pthsfval Paths G = f p | f Trails G p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =

Proof

Step Hyp Ref Expression
1 biidd g = G Fun p 1 ..^ f -1 p 0 f p 1 ..^ f = Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
2 df-pths Paths = g V f p | f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
3 3anass f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f = f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
4 3 opabbii f p | f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f = = f p | f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
5 4 mpteq2i g V f p | f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f = = g V f p | f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
6 2 5 eqtri Paths = g V f p | f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
7 1 6 fvmptopab Paths G = f p | f Trails G p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
8 3anass f Trails G p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f = f Trails G p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
9 8 opabbii f p | f Trails G p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f = = f p | f Trails G p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
10 7 9 eqtr4i Paths G = f p | f Trails G p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =