# Metamath Proof Explorer

## Theorem elwwlks2

Description: A walk of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 21-Feb-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 14-Mar-2022)

Ref Expression
Hypothesis elwwlks2.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
Assertion elwwlks2 ${⊢}{G}\in \mathrm{UPGraph}\to \left({W}\in \left(2\mathrm{WWalksN}{G}\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}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 elwwlks2.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 1 wwlksnwwlksnon ${⊢}{W}\in \left(2\mathrm{WWalksN}{G}\right)↔\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)$
3 2 a1i ${⊢}{G}\in \mathrm{UPGraph}\to \left({W}\in \left(2\mathrm{WWalksN}{G}\right)↔\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)$
4 1 elwwlks2on ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\wedge {c}\in {V}\right)\to \left({W}\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\right)$
5 4 3expb ${⊢}\left({G}\in \mathrm{UPGraph}\wedge \left({a}\in {V}\wedge {c}\in {V}\right)\right)\to \left({W}\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\right)$
6 5 2rexbidva ${⊢}{G}\in \mathrm{UPGraph}\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{W}\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)↔\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\right)$
7 rexcom ${⊢}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)$
8 s3cli ${⊢}⟨“{a}{b}{c}”⟩\in \mathrm{Word}\mathrm{V}$
9 8 a1i ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to ⟨“{a}{b}{c}”⟩\in \mathrm{Word}\mathrm{V}$
10 simplr ${⊢}\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to {W}=⟨“{a}{b}{c}”⟩$
11 simpr ${⊢}\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to {p}=⟨“{a}{b}{c}”⟩$
12 10 11 eqtr4d ${⊢}\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to {W}={p}$
13 12 breq2d ${⊢}\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left({f}\mathrm{Walks}\left({G}\right){W}↔{f}\mathrm{Walks}\left({G}\right){p}\right)$
14 13 biimpd ${⊢}\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left({f}\mathrm{Walks}\left({G}\right){W}\to {f}\mathrm{Walks}\left({G}\right){p}\right)$
15 14 com12 ${⊢}{f}\mathrm{Walks}\left({G}\right){W}\to \left(\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to {f}\mathrm{Walks}\left({G}\right){p}\right)$
16 15 adantr ${⊢}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\to \left(\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to {f}\mathrm{Walks}\left({G}\right){p}\right)$
17 16 impcom ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\to {f}\mathrm{Walks}\left({G}\right){p}$
18 simprr ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\to \left|{f}\right|=2$
19 vex ${⊢}{a}\in \mathrm{V}$
20 s3fv0 ${⊢}{a}\in \mathrm{V}\to ⟨“{a}{b}{c}”⟩\left(0\right)={a}$
21 20 eqcomd ${⊢}{a}\in \mathrm{V}\to {a}=⟨“{a}{b}{c}”⟩\left(0\right)$
22 19 21 mp1i ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {a}=⟨“{a}{b}{c}”⟩\left(0\right)$
23 fveq1 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {p}\left(0\right)=⟨“{a}{b}{c}”⟩\left(0\right)$
24 22 23 eqtr4d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {a}={p}\left(0\right)$
25 vex ${⊢}{b}\in \mathrm{V}$
26 s3fv1 ${⊢}{b}\in \mathrm{V}\to ⟨“{a}{b}{c}”⟩\left(1\right)={b}$
27 26 eqcomd ${⊢}{b}\in \mathrm{V}\to {b}=⟨“{a}{b}{c}”⟩\left(1\right)$
28 25 27 mp1i ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {b}=⟨“{a}{b}{c}”⟩\left(1\right)$
29 fveq1 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {p}\left(1\right)=⟨“{a}{b}{c}”⟩\left(1\right)$
30 28 29 eqtr4d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {b}={p}\left(1\right)$
31 vex ${⊢}{c}\in \mathrm{V}$
32 s3fv2 ${⊢}{c}\in \mathrm{V}\to ⟨“{a}{b}{c}”⟩\left(2\right)={c}$
33 32 eqcomd ${⊢}{c}\in \mathrm{V}\to {c}=⟨“{a}{b}{c}”⟩\left(2\right)$
34 31 33 mp1i ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {c}=⟨“{a}{b}{c}”⟩\left(2\right)$
35 fveq1 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {p}\left(2\right)=⟨“{a}{b}{c}”⟩\left(2\right)$
36 34 35 eqtr4d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {c}={p}\left(2\right)$
37 24 30 36 3jca ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)$
38 37 adantl ${⊢}\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)$
39 38 adantr ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\to \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)$
40 17 18 39 3jca ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)$
41 40 ex ${⊢}\left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left(\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)$
42 9 41 spcimedv ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left(\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\to \exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)$
43 wlklenvp1 ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left|{p}\right|=\left|{f}\right|+1$
44 simpl ${⊢}\left(\left|{p}\right|=\left|{f}\right|+1\wedge \left|{f}\right|=2\right)\to \left|{p}\right|=\left|{f}\right|+1$
45 oveq1 ${⊢}\left|{f}\right|=2\to \left|{f}\right|+1=2+1$
46 45 adantl ${⊢}\left(\left|{p}\right|=\left|{f}\right|+1\wedge \left|{f}\right|=2\right)\to \left|{f}\right|+1=2+1$
47 44 46 eqtrd ${⊢}\left(\left|{p}\right|=\left|{f}\right|+1\wedge \left|{f}\right|=2\right)\to \left|{p}\right|=2+1$
48 47 adantl ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left|{p}\right|=\left|{f}\right|+1\wedge \left|{f}\right|=2\right)\right)\to \left|{p}\right|=2+1$
49 2p1e3 ${⊢}2+1=3$
50 48 49 syl6eq ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left|{p}\right|=\left|{f}\right|+1\wedge \left|{f}\right|=2\right)\right)\to \left|{p}\right|=3$
51 50 exp32 ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left(\left|{p}\right|=\left|{f}\right|+1\to \left(\left|{f}\right|=2\to \left|{p}\right|=3\right)\right)$
52 43 51 mpd ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left(\left|{f}\right|=2\to \left|{p}\right|=3\right)$
53 52 adantr ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\to \left(\left|{f}\right|=2\to \left|{p}\right|=3\right)$
54 53 imp ${⊢}\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\to \left|{p}\right|=3$
55 eqcom ${⊢}{a}={p}\left(0\right)↔{p}\left(0\right)={a}$
56 55 biimpi ${⊢}{a}={p}\left(0\right)\to {p}\left(0\right)={a}$
57 eqcom ${⊢}{b}={p}\left(1\right)↔{p}\left(1\right)={b}$
58 57 biimpi ${⊢}{b}={p}\left(1\right)\to {p}\left(1\right)={b}$
59 eqcom ${⊢}{c}={p}\left(2\right)↔{p}\left(2\right)={c}$
60 59 biimpi ${⊢}{c}={p}\left(2\right)\to {p}\left(2\right)={c}$
61 56 58 60 3anim123i ${⊢}\left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\to \left({p}\left(0\right)={a}\wedge {p}\left(1\right)={b}\wedge {p}\left(2\right)={c}\right)$
62 54 61 anim12i ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left(\left|{p}\right|=3\wedge \left({p}\left(0\right)={a}\wedge {p}\left(1\right)={b}\wedge {p}\left(2\right)={c}\right)\right)$
63 1 wlkpwrd ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to {p}\in \mathrm{Word}{V}$
64 simpr ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\to {a}\in {V}$
65 64 anim1i ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to \left({a}\in {V}\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)$
66 3anass ${⊢}\left({a}\in {V}\wedge {b}\in {V}\wedge {c}\in {V}\right)↔\left({a}\in {V}\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)$
67 65 66 sylibr ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to \left({a}\in {V}\wedge {b}\in {V}\wedge {c}\in {V}\right)$
68 67 adantr ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left({a}\in {V}\wedge {b}\in {V}\wedge {c}\in {V}\right)$
69 63 68 anim12i ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\to \left({p}\in \mathrm{Word}{V}\wedge \left({a}\in {V}\wedge {b}\in {V}\wedge {c}\in {V}\right)\right)$
70 69 ad2antrr ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left({p}\in \mathrm{Word}{V}\wedge \left({a}\in {V}\wedge {b}\in {V}\wedge {c}\in {V}\right)\right)$
71 eqwrds3 ${⊢}\left({p}\in \mathrm{Word}{V}\wedge \left({a}\in {V}\wedge {b}\in {V}\wedge {c}\in {V}\right)\right)\to \left({p}=⟨“{a}{b}{c}”⟩↔\left(\left|{p}\right|=3\wedge \left({p}\left(0\right)={a}\wedge {p}\left(1\right)={b}\wedge {p}\left(2\right)={c}\right)\right)\right)$
72 70 71 syl ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left({p}=⟨“{a}{b}{c}”⟩↔\left(\left|{p}\right|=3\wedge \left({p}\left(0\right)={a}\wedge {p}\left(1\right)={b}\wedge {p}\left(2\right)={c}\right)\right)\right)$
73 62 72 mpbird ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to {p}=⟨“{a}{b}{c}”⟩$
74 simprr ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\to {W}=⟨“{a}{b}{c}”⟩$
75 74 ad2antrr ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to {W}=⟨“{a}{b}{c}”⟩$
76 73 75 eqtr4d ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to {p}={W}$
77 76 breq2d ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}↔{f}\mathrm{Walks}\left({G}\right){W}\right)$
78 77 biimpd ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\to {f}\mathrm{Walks}\left({G}\right){W}\right)$
79 simplr ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left|{f}\right|=2$
80 78 79 jctird ${⊢}\left(\left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\right)\wedge \left|{f}\right|=2\right)\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\to \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)$
81 80 exp41 ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left(\left|{f}\right|=2\to \left(\left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\to \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\right)\right)\right)$
82 81 com25 ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left({f}\mathrm{Walks}\left({G}\right){p}\to \left(\left|{f}\right|=2\to \left(\left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\to \left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\right)\right)\right)$
83 82 pm2.43i ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left(\left|{f}\right|=2\to \left(\left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\to \left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)\right)\right)$
84 83 3imp ${⊢}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left(\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)$
85 84 com12 ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left(\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)$
86 85 exlimdv ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left(\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)$
87 42 86 impbid ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left(\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)↔\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)$
88 87 exbidv ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {W}=⟨“{a}{b}{c}”⟩\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)$
89 88 pm5.32da ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to \left(\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)↔\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)\right)$
90 89 2rexbidva ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\to \left(\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)\right)$
91 7 90 syl5bb ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\to \left(\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)\right)$
92 91 rexbidva ${⊢}{G}\in \mathrm{UPGraph}\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){W}\wedge \left|{f}\right|=2\right)\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}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)\right)$
93 3 6 92 3bitrd ${⊢}{G}\in \mathrm{UPGraph}\to \left({W}\in \left(2\mathrm{WWalksN}{G}\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}}\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Walks}\left({G}\right){p}\wedge \left|{f}\right|=2\wedge \left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)\right)\right)\right)$