Theorem wlkvtxedg

Description: The vertices of a walk are connected by edges. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021)

	Ref	Expression
Hypothesis	wlkvtxedg.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	wlkvtxedg	$$⊢F\mathrm{Walks}\left(G\right)P\to \forall k\in \left(0..^\left|F\right|\right)\exists e\in E\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq e$$

Proof

Step	Hyp	Ref	Expression
1		wlkvtxedg.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
2		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
3	2	wlkvtxiedg	$$⊢F\mathrm{Walks}\left(G\right)P\to \forall k\in \left(0..^\left|F\right|\right)\exists e\in \mathrm{ran}\mathrm{iEdg}\left(G\right)\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq e$$
4		edgval	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
5	1 4	eqtr2i	$$⊢\mathrm{ran}\mathrm{iEdg}\left(G\right)=E$$
6	5	rexeqi	$$⊢\exists e\in \mathrm{ran}\mathrm{iEdg}\left(G\right)\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq e\leftrightarrow \exists e\in E\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq e$$
7	6	ralbii	$$⊢\forall k\in \left(0..^\left|F\right|\right)\exists e\in \mathrm{ran}\mathrm{iEdg}\left(G\right)\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq e\leftrightarrow \forall k\in \left(0..^\left|F\right|\right)\exists e\in E\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq e$$
8	3 7	sylib	$$⊢F\mathrm{Walks}\left(G\right)P\to \forall k\in \left(0..^\left|F\right|\right)\exists e\in E\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq e$$