Metamath Proof Explorer


Theorem relwlk

Description: The set ( WalksG ) of all walks on G is a set of pairs by our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018) (Revised by AV, 19-Feb-2021)

Ref Expression
Assertion relwlk Rel Walks G

Proof

Step Hyp Ref Expression
1 df-wlks Walks = g V f p | f Word dom iEdg g p : 0 f Vtx g k 0 ..^ f if- p k = p k + 1 iEdg g f k = p k p k p k + 1 iEdg g f k
2 1 relmptopab Rel Walks G