Theorem wlkp

Description: The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021)

	Ref	Expression
Hypothesis	wlkp.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	wlkp	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶V$$

Proof

Step	Hyp	Ref	Expression
1		wlkp.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
3	1 2	wlkprop	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(F\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left(G\right)\wedge P:\left(0\dots \left|F\right|\right)⟶V\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)$$
4	3	simp2d	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶V$$