# Metamath Proof Explorer

## Theorem wlkprop

Description: Properties of a walk. (Contributed by AV, 5-Nov-2021)

Ref Expression
Hypotheses wksfval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
wksfval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
Assertion wlkprop ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\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),{I}\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq {I}\left({F}\left({k}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 wksfval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 wksfval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 1 2 wksfval ${⊢}{G}\in \mathrm{V}\to \mathrm{Walks}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\in \mathrm{Word}\mathrm{dom}{I}\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),{I}\left({f}\left({k}\right)\right)=\left\{{p}\left({k}\right)\right\},\left\{{p}\left({k}\right),{p}\left({k}+1\right)\right\}\subseteq {I}\left({f}\left({k}\right)\right)\right)\right)\right\}$
4 3 brfvopab ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$
5 1 2 iswlk ${⊢}\left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\to \left({F}\mathrm{Walks}\left({G}\right){P}↔\left({F}\in \mathrm{Word}\mathrm{dom}{I}\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),{I}\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
6 5 biimpd ${⊢}\left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\to \left({F}\mathrm{Walks}\left({G}\right){P}\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\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),{I}\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
7 4 6 mpcom ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\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),{I}\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq {I}\left({F}\left({k}\right)\right)\right)\right)$