# Metamath Proof Explorer

## 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)\phantom{\rule{.4em}{0ex}}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}$