# Metamath Proof Explorer

## Theorem elwspths2spth

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

Ref Expression
Hypothesis elwwlks2.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
Assertion elwspths2spth ${⊢}{G}\in \mathrm{UPGraph}\to \left({W}\in \left(2\mathrm{WSPathsN}{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{SPaths}\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 wspthsnwspthsnon ${⊢}{W}\in \left(2\mathrm{WSPathsN}{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{WSPathsNOn}{G}\right){c}\right)$
3 2 a1i ${⊢}{G}\in \mathrm{UPGraph}\to \left({W}\in \left(2\mathrm{WSPathsN}{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{WSPathsNOn}{G}\right){c}\right)\right)$
4 1 elwspths2on ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\wedge {c}\in {V}\right)\to \left({W}\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\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{WSPathsNOn}{G}\right){c}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\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{WSPathsNOn}{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 ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\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 ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\right)\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\left({W}=⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\right)\right)$
8 wspthnon ${⊢}⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\right)↔\left(⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\right)$
9 ancom ${⊢}\left(⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\right)↔\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)$
10 19.41v ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)↔\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)$
11 9 10 bitr4i ${⊢}\left(⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)$
12 simpr ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\to {a}\in {V}$
13 simpr ${⊢}\left({b}\in {V}\wedge {c}\in {V}\right)\to {c}\in {V}$
14 12 13 anim12i ${⊢}\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 {c}\in {V}\right)$
15 vex ${⊢}{f}\in \mathrm{V}$
16 s3cli ${⊢}⟨“{a}{b}{c}”⟩\in \mathrm{Word}\mathrm{V}$
17 15 16 pm3.2i ${⊢}\left({f}\in \mathrm{V}\wedge ⟨“{a}{b}{c}”⟩\in \mathrm{Word}\mathrm{V}\right)$
18 1 isspthonpth ${⊢}\left(\left({a}\in {V}\wedge {c}\in {V}\right)\wedge \left({f}\in \mathrm{V}\wedge ⟨“{a}{b}{c}”⟩\in \mathrm{Word}\mathrm{V}\right)\right)\to \left({f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩↔\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\right)$
19 14 17 18 sylancl ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to \left({f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩↔\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\right)$
20 wwlknon ${⊢}⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)↔\left(⟨“{a}{b}{c}”⟩\in \left(2\mathrm{WWalksN}{G}\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)$
21 2nn0 ${⊢}2\in {ℕ}_{0}$
22 iswwlksn ${⊢}2\in {ℕ}_{0}\to \left(⟨“{a}{b}{c}”⟩\in \left(2\mathrm{WWalksN}{G}\right)↔\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\right)$
23 21 22 mp1i ${⊢}\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}{b}{c}”⟩\in \left(2\mathrm{WWalksN}{G}\right)↔\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\right)$
24 23 3anbi1d ${⊢}\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(⟨“{a}{b}{c}”⟩\in \left(2\mathrm{WWalksN}{G}\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)↔\left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)$
25 20 24 syl5bb ${⊢}\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}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)↔\left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)$
26 19 25 anbi12d ${⊢}\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({f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)↔\left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)$
27 26 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(\left({f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)↔\left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)$
28 16 a1i ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to ⟨“{a}{b}{c}”⟩\in \mathrm{Word}\mathrm{V}$
29 simprl1 ${⊢}\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 {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)\to {f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩$
30 spthiswlk ${⊢}{f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\to {f}\mathrm{Walks}\left({G}\right)⟨“{a}{b}{c}”⟩$
31 wlklenvm1 ${⊢}{f}\mathrm{Walks}\left({G}\right)⟨“{a}{b}{c}”⟩\to \left|{f}\right|=\left|⟨“{a}{b}{c}”⟩\right|-1$
32 simpl ${⊢}\left(\left|{f}\right|=\left|⟨“{a}{b}{c}”⟩\right|-1\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\to \left|{f}\right|=\left|⟨“{a}{b}{c}”⟩\right|-1$
33 oveq1 ${⊢}\left|⟨“{a}{b}{c}”⟩\right|=2+1\to \left|⟨“{a}{b}{c}”⟩\right|-1=2+1-1$
34 2cn ${⊢}2\in ℂ$
35 pncan1 ${⊢}2\in ℂ\to 2+1-1=2$
36 34 35 ax-mp ${⊢}2+1-1=2$
37 33 36 syl6eq ${⊢}\left|⟨“{a}{b}{c}”⟩\right|=2+1\to \left|⟨“{a}{b}{c}”⟩\right|-1=2$
38 37 adantl ${⊢}\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\to \left|⟨“{a}{b}{c}”⟩\right|-1=2$
39 38 3ad2ant1 ${⊢}\left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\to \left|⟨“{a}{b}{c}”⟩\right|-1=2$
40 39 adantl ${⊢}\left(\left|{f}\right|=\left|⟨“{a}{b}{c}”⟩\right|-1\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\to \left|⟨“{a}{b}{c}”⟩\right|-1=2$
41 32 40 eqtrd ${⊢}\left(\left|{f}\right|=\left|⟨“{a}{b}{c}”⟩\right|-1\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\to \left|{f}\right|=2$
42 41 ex ${⊢}\left|{f}\right|=\left|⟨“{a}{b}{c}”⟩\right|-1\to \left(\left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\to \left|{f}\right|=2\right)$
43 30 31 42 3syl ${⊢}{f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\to \left(\left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\to \left|{f}\right|=2\right)$
44 43 3ad2ant1 ${⊢}\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\to \left(\left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\to \left|{f}\right|=2\right)$
45 44 imp ${⊢}\left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\to \left|{f}\right|=2$
46 45 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 {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)\to \left|{f}\right|=2$
47 s3fv0 ${⊢}{a}\in \mathrm{V}\to ⟨“{a}{b}{c}”⟩\left(0\right)={a}$
48 47 elv ${⊢}⟨“{a}{b}{c}”⟩\left(0\right)={a}$
49 48 eqcomi ${⊢}{a}=⟨“{a}{b}{c}”⟩\left(0\right)$
50 s3fv1 ${⊢}{b}\in \mathrm{V}\to ⟨“{a}{b}{c}”⟩\left(1\right)={b}$
51 50 elv ${⊢}⟨“{a}{b}{c}”⟩\left(1\right)={b}$
52 51 eqcomi ${⊢}{b}=⟨“{a}{b}{c}”⟩\left(1\right)$
53 s3fv2 ${⊢}{c}\in \mathrm{V}\to ⟨“{a}{b}{c}”⟩\left(2\right)={c}$
54 53 elv ${⊢}⟨“{a}{b}{c}”⟩\left(2\right)={c}$
55 54 eqcomi ${⊢}{c}=⟨“{a}{b}{c}”⟩\left(2\right)$
56 49 52 55 3pm3.2i ${⊢}\left({a}=⟨“{a}{b}{c}”⟩\left(0\right)\wedge {b}=⟨“{a}{b}{c}”⟩\left(1\right)\wedge {c}=⟨“{a}{b}{c}”⟩\left(2\right)\right)$
57 56 a1i ${⊢}\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 {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)\to \left({a}=⟨“{a}{b}{c}”⟩\left(0\right)\wedge {b}=⟨“{a}{b}{c}”⟩\left(1\right)\wedge {c}=⟨“{a}{b}{c}”⟩\left(2\right)\right)$
58 29 46 57 3jca ${⊢}\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 {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)\to \left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge \left|{f}\right|=2\wedge \left({a}=⟨“{a}{b}{c}”⟩\left(0\right)\wedge {b}=⟨“{a}{b}{c}”⟩\left(1\right)\wedge {c}=⟨“{a}{b}{c}”⟩\left(2\right)\right)\right)$
59 breq2 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left({f}\mathrm{SPaths}\left({G}\right){p}↔{f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\right)$
60 fveq1 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {p}\left(0\right)=⟨“{a}{b}{c}”⟩\left(0\right)$
61 60 eqeq2d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left({a}={p}\left(0\right)↔{a}=⟨“{a}{b}{c}”⟩\left(0\right)\right)$
62 fveq1 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {p}\left(1\right)=⟨“{a}{b}{c}”⟩\left(1\right)$
63 62 eqeq2d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left({b}={p}\left(1\right)↔{b}=⟨“{a}{b}{c}”⟩\left(1\right)\right)$
64 fveq1 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to {p}\left(2\right)=⟨“{a}{b}{c}”⟩\left(2\right)$
65 64 eqeq2d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left({c}={p}\left(2\right)↔{c}=⟨“{a}{b}{c}”⟩\left(2\right)\right)$
66 61 63 65 3anbi123d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left(\left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)↔\left({a}=⟨“{a}{b}{c}”⟩\left(0\right)\wedge {b}=⟨“{a}{b}{c}”⟩\left(1\right)\wedge {c}=⟨“{a}{b}{c}”⟩\left(2\right)\right)\right)$
67 59 66 3anbi13d ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left(\left({f}\mathrm{SPaths}\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)↔\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge \left|{f}\right|=2\wedge \left({a}=⟨“{a}{b}{c}”⟩\left(0\right)\wedge {b}=⟨“{a}{b}{c}”⟩\left(1\right)\wedge {c}=⟨“{a}{b}{c}”⟩\left(2\right)\right)\right)\right)$
68 67 ad2antlr ${⊢}\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 {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)\to \left(\left({f}\mathrm{SPaths}\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)↔\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge \left|{f}\right|=2\wedge \left({a}=⟨“{a}{b}{c}”⟩\left(0\right)\wedge {b}=⟨“{a}{b}{c}”⟩\left(1\right)\wedge {c}=⟨“{a}{b}{c}”⟩\left(2\right)\right)\right)\right)$
69 58 68 mpbird ${⊢}\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 {p}=⟨“{a}{b}{c}”⟩\right)\wedge \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)\to \left({f}\mathrm{SPaths}\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)$
70 69 ex ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left(\left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\to \left({f}\mathrm{SPaths}\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)$
71 28 70 spcimedv ${⊢}\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(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\to \exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
72 spthiswlk ${⊢}{f}\mathrm{SPaths}\left({G}\right){p}\to {f}\mathrm{Walks}\left({G}\right){p}$
73 wlklenvp1 ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left|{p}\right|=\left|{f}\right|+1$
74 oveq1 ${⊢}\left|{f}\right|=2\to \left|{f}\right|+1=2+1$
75 2p1e3 ${⊢}2+1=3$
76 74 75 syl6eq ${⊢}\left|{f}\right|=2\to \left|{f}\right|+1=3$
77 76 eqeq2d ${⊢}\left|{f}\right|=2\to \left(\left|{p}\right|=\left|{f}\right|+1↔\left|{p}\right|=3\right)$
78 77 biimpcd ${⊢}\left|{p}\right|=\left|{f}\right|+1\to \left(\left|{f}\right|=2\to \left|{p}\right|=3\right)$
79 72 73 78 3syl ${⊢}{f}\mathrm{SPaths}\left({G}\right){p}\to \left(\left|{f}\right|=2\to \left|{p}\right|=3\right)$
80 79 imp ${⊢}\left({f}\mathrm{SPaths}\left({G}\right){p}\wedge \left|{f}\right|=2\right)\to \left|{p}\right|=3$
81 80 3adant3 ${⊢}\left({f}\mathrm{SPaths}\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|{p}\right|=3$
82 81 adantl ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\to \left|{p}\right|=3$
83 eqcom ${⊢}{a}={p}\left(0\right)↔{p}\left(0\right)={a}$
84 eqcom ${⊢}{b}={p}\left(1\right)↔{p}\left(1\right)={b}$
85 eqcom ${⊢}{c}={p}\left(2\right)↔{p}\left(2\right)={c}$
86 83 84 85 3anbi123i ${⊢}\left({a}={p}\left(0\right)\wedge {b}={p}\left(1\right)\wedge {c}={p}\left(2\right)\right)↔\left({p}\left(0\right)={a}\wedge {p}\left(1\right)={b}\wedge {p}\left(2\right)={c}\right)$
87 86 biimpi ${⊢}\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)$
88 87 3ad2ant3 ${⊢}\left({f}\mathrm{SPaths}\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({p}\left(0\right)={a}\wedge {p}\left(1\right)={b}\wedge {p}\left(2\right)={c}\right)$
89 88 adantl ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\to \left({p}\left(0\right)={a}\wedge {p}\left(1\right)={b}\wedge {p}\left(2\right)={c}\right)$
90 82 89 jca ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\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)$
91 1 wlkpwrd ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to {p}\in \mathrm{Word}{V}$
92 72 91 syl ${⊢}{f}\mathrm{SPaths}\left({G}\right){p}\to {p}\in \mathrm{Word}{V}$
93 92 3ad2ant1 ${⊢}\left({f}\mathrm{SPaths}\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 {p}\in \mathrm{Word}{V}$
94 12 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)$
95 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)$
96 94 95 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)$
97 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)$
98 93 96 97 syl2anr ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\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)$
99 90 98 mpbird ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\to {p}=⟨“{a}{b}{c}”⟩$
100 59 biimpcd ${⊢}{f}\mathrm{SPaths}\left({G}\right){p}\to \left({p}=⟨“{a}{b}{c}”⟩\to {f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\right)$
101 100 3ad2ant1 ${⊢}\left({f}\mathrm{SPaths}\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({p}=⟨“{a}{b}{c}”⟩\to {f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\right)$
102 101 adantl ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\to \left({p}=⟨“{a}{b}{c}”⟩\to {f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\right)$
103 102 imp ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to {f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩$
104 48 a1i ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to ⟨“{a}{b}{c}”⟩\left(0\right)={a}$
105 fveq2 ${⊢}\left|{f}\right|=2\to ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)=⟨“{a}{b}{c}”⟩\left(2\right)$
106 105 54 syl6eq ${⊢}\left|{f}\right|=2\to ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}$
107 106 3ad2ant2 ${⊢}\left({f}\mathrm{SPaths}\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 ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}$
108 107 ad2antlr ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}$
109 103 104 108 3jca ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)$
110 wlkiswwlks1 ${⊢}{G}\in \mathrm{UPGraph}\to \left({f}\mathrm{Walks}\left({G}\right){p}\to {p}\in \mathrm{WWalks}\left({G}\right)\right)$
111 110 adantr ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\to {p}\in \mathrm{WWalks}\left({G}\right)\right)$
112 111 adantr ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to \left({f}\mathrm{Walks}\left({G}\right){p}\to {p}\in \mathrm{WWalks}\left({G}\right)\right)$
113 72 112 syl5com ${⊢}{f}\mathrm{SPaths}\left({G}\right){p}\to \left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to {p}\in \mathrm{WWalks}\left({G}\right)\right)$
114 113 3ad2ant1 ${⊢}\left({f}\mathrm{SPaths}\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({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to {p}\in \mathrm{WWalks}\left({G}\right)\right)$
115 114 impcom ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\to {p}\in \mathrm{WWalks}\left({G}\right)$
116 115 adantr ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to {p}\in \mathrm{WWalks}\left({G}\right)$
117 eleq1 ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left({p}\in \mathrm{WWalks}\left({G}\right)↔⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\right)$
118 117 bicomd ${⊢}{p}=⟨“{a}{b}{c}”⟩\to \left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)↔{p}\in \mathrm{WWalks}\left({G}\right)\right)$
119 118 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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)↔{p}\in \mathrm{WWalks}\left({G}\right)\right)$
120 116 119 mpbird ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to ⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)$
121 s3len ${⊢}\left|⟨“{a}{b}{c}”⟩\right|=3$
122 df-3 ${⊢}3=2+1$
123 121 122 eqtri ${⊢}\left|⟨“{a}{b}{c}”⟩\right|=2+1$
124 120 123 jctir ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)$
125 54 a1i ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to ⟨“{a}{b}{c}”⟩\left(2\right)={c}$
126 124 104 125 3jca ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)$
127 109 126 jca ${⊢}\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 \left({f}\mathrm{SPaths}\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)\wedge {p}=⟨“{a}{b}{c}”⟩\right)\to \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)$
128 99 127 mpdan ${⊢}\left(\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\wedge \left({f}\mathrm{SPaths}\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)\to \left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)$
129 128 ex ${⊢}\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({f}\mathrm{SPaths}\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({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)$
130 129 exlimdv ${⊢}\left(\left({G}\in \mathrm{UPGraph}\wedge {a}\in {V}\right)\wedge \left({b}\in {V}\wedge {c}\in {V}\right)\right)\to \left(\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)\right)$
131 71 130 impbid ${⊢}\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(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)↔\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
132 131 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(\left(\left({f}\mathrm{SPaths}\left({G}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(\left|{f}\right|\right)={c}\right)\wedge \left(\left(⟨“{a}{b}{c}”⟩\in \mathrm{WWalks}\left({G}\right)\wedge \left|⟨“{a}{b}{c}”⟩\right|=2+1\right)\wedge ⟨“{a}{b}{c}”⟩\left(0\right)={a}\wedge ⟨“{a}{b}{c}”⟩\left(2\right)={c}\right)\right)↔\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
133 27 132 bitrd ${⊢}\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}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)↔\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
134 133 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}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\wedge ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
135 11 134 syl5bb ${⊢}\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(⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WWalksNOn}{G}\right){c}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}\left({a}\mathrm{SPathsOn}\left({G}\right){c}\right)⟨“{a}{b}{c}”⟩\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
136 8 135 syl5bb ${⊢}\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}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
137 136 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 ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\right)\right)↔\left({W}=⟨“{a}{b}{c}”⟩\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{SPaths}\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)$
138 137 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 ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\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{SPaths}\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)$
139 7 138 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 ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\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{SPaths}\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)$
140 139 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 ⟨“{a}{b}{c}”⟩\in \left({a}\left(2\mathrm{WSPathsNOn}{G}\right){c}\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{SPaths}\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)$
141 3 6 140 3bitrd ${⊢}{G}\in \mathrm{UPGraph}\to \left({W}\in \left(2\mathrm{WSPathsN}{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{SPaths}\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)$