Theorem midwwlks2s3

Description: There is a vertex between the endpoints of a walk of length 2 between two vertices as length 3 string. (Contributed by AV, 10-Jan-2022)

	Ref	Expression
Hypothesis	elwwlks2s3.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	midwwlks2s3	$$⊢W\in \left(2\mathrm{WWalksN}G\right)\to \exists b\in VW\left(1\right)=b$$

Proof

Step	Hyp	Ref	Expression
1		elwwlks2s3.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	elwwlks2s3	$$⊢W\in \left(2\mathrm{WWalksN}G\right)\to \exists a\in V\exists b\in V\exists c\in VW=⟨“abc”⟩$$
3		fveq1	$$⊢W=⟨“abc”⟩\to W\left(1\right)=⟨“abc”⟩\left(1\right)$$
4		s3fv1	$$⊢b\in V\to ⟨“abc”⟩\left(1\right)=b$$
5	3 4	sylan9eqr	$$⊢\left(b\in V\wedge W=⟨“abc”⟩\right)\to W\left(1\right)=b$$
6	5	ex	$$⊢b\in V\to \left(W=⟨“abc”⟩\to W\left(1\right)=b\right)$$
7	6	adantl	$$⊢\left(a\in V\wedge b\in V\right)\to \left(W=⟨“abc”⟩\to W\left(1\right)=b\right)$$
8	7	rexlimdvw	$$⊢\left(a\in V\wedge b\in V\right)\to \left(\exists c\in VW=⟨“abc”⟩\to W\left(1\right)=b\right)$$
9	8	reximdva	$$⊢a\in V\to \left(\exists b\in V\exists c\in VW=⟨“abc”⟩\to \exists b\in VW\left(1\right)=b\right)$$
10	9	rexlimiv	$$⊢\exists a\in V\exists b\in V\exists c\in VW=⟨“abc”⟩\to \exists b\in VW\left(1\right)=b$$
11	2 10	syl	$$⊢W\in \left(2\mathrm{WWalksN}G\right)\to \exists b\in VW\left(1\right)=b$$