This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )