Theorem wlkpvtx

Description: A walk connects vertices. (Contributed by AV, 22-Feb-2021)

	Ref	Expression
Hypothesis	wlkpvtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	wlkpvtx	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(N\in \left(0\dots \left|F\right|\right)\to P\left(N\right)\in V\right)$$

Proof

Step	Hyp	Ref	Expression
1		wlkpvtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	wlkp	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶V$$
3		ffvelcdm	$$⊢\left(P:\left(0\dots \left|F\right|\right)⟶V\wedge N\in \left(0\dots \left|F\right|\right)\right)\to P\left(N\right)\in V$$
4	3	ex	$$⊢P:\left(0\dots \left|F\right|\right)⟶V\to \left(N\in \left(0\dots \left|F\right|\right)\to P\left(N\right)\in V\right)$$
5	2 4	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(N\in \left(0\dots \left|F\right|\right)\to P\left(N\right)\in V\right)$$