Metamath Proof Explorer

Theorem elwwlks2s3

Description: A walk of length 2 as word is a length 3 string. (Contributed by AV, 18-May-2021)

Ref Expression
Hypothesis elwwlks2s3.v 
|- V = ( Vtx ` G )
Assertion elwwlks2s3 
|- ( W e. ( 2 WWalksN G ) -> E. a e. V E. b e. V E. c e. V W = <" a b c "> )

Proof

Step Hyp Ref Expression
1 elwwlks2s3.v 
 |-  V = ( Vtx ` G )
2 wwlknbp1 
 |-  ( W e. ( 2 WWalksN G ) -> ( 2 e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( 2 + 1 ) ) )
3 1 wrdeqi 
 |-  Word V = Word ( Vtx ` G )
4 3 eleq2i 
 |-  ( W e. Word V <-> W e. Word ( Vtx ` G ) )
5 df-3 
 |-  3 = ( 2 + 1 )
6 5 eqeq2i 
 |-  ( ( # ` W ) = 3 <-> ( # ` W ) = ( 2 + 1 ) )
7 4 6 anbi12i 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( 2 + 1 ) ) )
8 wrdl3s3 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> E. a e. V E. b e. V E. c e. V W = <" a b c "> )
9 7 8 sylbb1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( 2 + 1 ) ) -> E. a e. V E. b e. V E. c e. V W = <" a b c "> )
10 9 3adant1 
 |-  ( ( 2 e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( 2 + 1 ) ) -> E. a e. V E. b e. V E. c e. V W = <" a b c "> )
11 2 10 syl 
 |-  ( W e. ( 2 WWalksN G ) -> E. a e. V E. b e. V E. c e. V W = <" a b c "> )