# Metamath Proof Explorer

## Theorem wlkv

Description: The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 3-Feb-2021)

Ref Expression
Assertion wlkv ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\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}\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)\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)\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)$