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)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)$$