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 = ( Vtx ` G )
Assertion	midwwlks2s3	|- ( W e. ( 2 WWalksN G ) -> E. b e. V ( W ` 1 ) = b )

Proof

Step	Hyp	Ref	Expression
1		elwwlks2s3.v	|- V = ( Vtx ` G )
2	1	elwwlks2s3	|- ( W e. ( 2 WWalksN G ) -> E. a e. V E. b e. V E. c e. V W = <" a b c "> )
3		fveq1	|- ( W = <" a b c "> -> ( W ` 1 ) = ( <" a b c "> ` 1 ) )
4		s3fv1	|- ( b e. V -> ( <" a b c "> ` 1 ) = b )
5	3 4	sylan9eqr	|- ( ( b e. V /\ W = <" a b c "> ) -> ( W ` 1 ) = b )
6	5	ex	|- ( b e. V -> ( W = <" a b c "> -> ( W ` 1 ) = b ) )
7	6	adantl	|- ( ( a e. V /\ b e. V ) -> ( W = <" a b c "> -> ( W ` 1 ) = b ) )
8	7	rexlimdvw	|- ( ( a e. V /\ b e. V ) -> ( E. c e. V W = <" a b c "> -> ( W ` 1 ) = b ) )
9	8	reximdva	|- ( a e. V -> ( E. b e. V E. c e. V W = <" a b c "> -> E. b e. V ( W ` 1 ) = b ) )
10	9	rexlimiv	|- ( E. a e. V E. b e. V E. c e. V W = <" a b c "> -> E. b e. V ( W ` 1 ) = b )
11	2 10	syl	|- ( W e. ( 2 WWalksN G ) -> E. b e. V ( W ` 1 ) = b )