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