Metamath Proof Explorer


Theorem relpths

Description: The set ( PathsG ) of all paths on G is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021)

Ref Expression
Assertion relpths Rel Paths G

Proof

Step Hyp Ref Expression
1 df-pths Paths = g V f p | f Trails g p Fun p 1 ..^ f -1 p 0 f p 1 ..^ f =
2 1 relmptopab Rel Paths G