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 "> )