# 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}=\mathrm{Vtx}\left({G}\right)$
Assertion elwwlks2s3 ${⊢}{W}\in \left(2\mathrm{WWalksN}{G}\right)\to \exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}=⟨“{a}{b}{c}”⟩$

### Proof

Step Hyp Ref Expression
1 elwwlks2s3.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 wwlknbp1 ${⊢}{W}\in \left(2\mathrm{WWalksN}{G}\right)\to \left(2\in {ℕ}_{0}\wedge {W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|=2+1\right)$
3 1 wrdeqi ${⊢}\mathrm{Word}{V}=\mathrm{Word}\mathrm{Vtx}\left({G}\right)$
4 3 eleq2i ${⊢}{W}\in \mathrm{Word}{V}↔{W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
5 df-3 ${⊢}3=2+1$
6 5 eqeq2i ${⊢}\left|{W}\right|=3↔\left|{W}\right|=2+1$
7 4 6 anbi12i ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=3\right)↔\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|=2+1\right)$
8 wrdl3s3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=3\right)↔\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}=⟨“{a}{b}{c}”⟩$
9 7 8 sylbb1 ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|=2+1\right)\to \exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}=⟨“{a}{b}{c}”⟩$
10 9 3adant1 ${⊢}\left(2\in {ℕ}_{0}\wedge {W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|=2+1\right)\to \exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}=⟨“{a}{b}{c}”⟩$
11 2 10 syl ${⊢}{W}\in \left(2\mathrm{WWalksN}{G}\right)\to \exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}=⟨“{a}{b}{c}”⟩$