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	$$⊢\mathrm{Rel}\mathrm{Walks}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-wlks	$$⊢\mathrm{Walks}=\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left(g\right)\wedge p:\left(0\dots \left|f\right|\right)⟶\mathrm{Vtx}\left(g\right)\wedge \forall k\in \left(0..^\left|f\right|\right)if-\left(p\left(k\right)=p\left(k+1\right),\mathrm{iEdg}\left(g\right)\left(f\left(k\right)\right)=\left\{p\left(k\right)\right\},\left\{p\left(k\right),p\left(k+1\right)\right\}\subseteq \mathrm{iEdg}\left(g\right)\left(f\left(k\right)\right)\right)\right)\right\}\right)$$
2	1	relmptopab	$$⊢\mathrm{Rel}\mathrm{Walks}\left(G\right)$$