# Metamath Proof Explorer

## Theorem numclwwlk1lem2f1

Description: T is a 1-1 function. (Contributed by AV, 26-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 23-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
extwwlkfab.c ${⊢}{C}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)={v}\right\}\right)$
extwwlkfab.f ${⊢}{F}={X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)$
numclwwlk.t ${⊢}{T}=\left({u}\in \left({X}{C}{N}\right)⟼⟨{u}\mathrm{prefix}\left({N}-2\right),{u}\left({N}-1\right)⟩\right)$
Assertion numclwwlk1lem2f1 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to {T}:{X}{C}{N}\underset{1-1}{⟶}{F}×\left({G}\mathrm{NeighbVtx}{X}\right)$

### Proof

Step Hyp Ref Expression
1 extwwlkfab.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 extwwlkfab.c ${⊢}{C}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)={v}\right\}\right)$
3 extwwlkfab.f ${⊢}{F}={X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)$
4 numclwwlk.t ${⊢}{T}=\left({u}\in \left({X}{C}{N}\right)⟼⟨{u}\mathrm{prefix}\left({N}-2\right),{u}\left({N}-1\right)⟩\right)$
5 1 2 3 4 numclwwlk1lem2f ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to {T}:{X}{C}{N}⟶{F}×\left({G}\mathrm{NeighbVtx}{X}\right)$
6 1 2 3 4 numclwwlk1lem2fv ${⊢}{p}\in \left({X}{C}{N}\right)\to {T}\left({p}\right)=⟨{p}\mathrm{prefix}\left({N}-2\right),{p}\left({N}-1\right)⟩$
7 6 ad2antrl ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)\right)\to {T}\left({p}\right)=⟨{p}\mathrm{prefix}\left({N}-2\right),{p}\left({N}-1\right)⟩$
8 1 2 3 4 numclwwlk1lem2fv ${⊢}{a}\in \left({X}{C}{N}\right)\to {T}\left({a}\right)=⟨{a}\mathrm{prefix}\left({N}-2\right),{a}\left({N}-1\right)⟩$
9 8 ad2antll ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)\right)\to {T}\left({a}\right)=⟨{a}\mathrm{prefix}\left({N}-2\right),{a}\left({N}-1\right)⟩$
10 7 9 eqeq12d ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)\right)\to \left({T}\left({p}\right)={T}\left({a}\right)↔⟨{p}\mathrm{prefix}\left({N}-2\right),{p}\left({N}-1\right)⟩=⟨{a}\mathrm{prefix}\left({N}-2\right),{a}\left({N}-1\right)⟩\right)$
11 ovex ${⊢}{p}\mathrm{prefix}\left({N}-2\right)\in \mathrm{V}$
12 fvex ${⊢}{p}\left({N}-1\right)\in \mathrm{V}$
13 11 12 opth ${⊢}⟨{p}\mathrm{prefix}\left({N}-2\right),{p}\left({N}-1\right)⟩=⟨{a}\mathrm{prefix}\left({N}-2\right),{a}\left({N}-1\right)⟩↔\left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)$
14 uzuzle23 ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}\in {ℤ}_{\ge 2}$
15 2 2clwwlkel ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({p}\in \left({X}{C}{N}\right)↔\left({p}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {p}\left({N}-2\right)={X}\right)\right)$
16 isclwwlknon ${⊢}{p}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)↔\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)$
17 16 anbi1i ${⊢}\left({p}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {p}\left({N}-2\right)={X}\right)↔\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)$
18 15 17 syl6bb ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({p}\in \left({X}{C}{N}\right)↔\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\right)$
19 2 2clwwlkel ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({a}\in \left({X}{C}{N}\right)↔\left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)$
20 isclwwlknon ${⊢}{a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)↔\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)$
21 20 anbi1i ${⊢}\left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {a}\left({N}-2\right)={X}\right)↔\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)$
22 19 21 syl6bb ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({a}\in \left({X}{C}{N}\right)↔\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)$
23 18 22 anbi12d ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left(\left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)↔\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\right)$
24 14 23 sylan2 ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)↔\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\right)$
25 24 3adant1 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)↔\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\right)$
26 1 clwwlknbp ${⊢}{p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left({p}\in \mathrm{Word}{V}\wedge \left|{p}\right|={N}\right)$
27 26 adantr ${⊢}\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\to \left({p}\in \mathrm{Word}{V}\wedge \left|{p}\right|={N}\right)$
28 27 adantr ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to \left({p}\in \mathrm{Word}{V}\wedge \left|{p}\right|={N}\right)$
29 simpr ${⊢}\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\to {p}\left(0\right)={X}$
30 29 adantr ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to {p}\left(0\right)={X}$
31 simpr ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to {p}\left({N}-2\right)={X}$
32 29 eqcomd ${⊢}\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\to {X}={p}\left(0\right)$
33 32 adantr ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to {X}={p}\left(0\right)$
34 31 33 eqtrd ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to {p}\left({N}-2\right)={p}\left(0\right)$
35 28 30 34 jca32 ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to \left(\left({p}\in \mathrm{Word}{V}\wedge \left|{p}\right|={N}\right)\wedge \left({p}\left(0\right)={X}\wedge {p}\left({N}-2\right)={p}\left(0\right)\right)\right)$
36 1 clwwlknbp ${⊢}{a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)$
37 36 adantr ${⊢}\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\to \left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)$
38 37 adantr ${⊢}\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\to \left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)$
39 simpr ${⊢}\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\to {a}\left(0\right)={X}$
40 39 adantr ${⊢}\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\to {a}\left(0\right)={X}$
41 simpr ${⊢}\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\to {a}\left({N}-2\right)={X}$
42 39 eqcomd ${⊢}\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\to {X}={a}\left(0\right)$
43 42 adantr ${⊢}\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\to {X}={a}\left(0\right)$
44 41 43 eqtrd ${⊢}\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\to {a}\left({N}-2\right)={a}\left(0\right)$
45 38 40 44 jca32 ${⊢}\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\to \left(\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\wedge \left({a}\left(0\right)={X}\wedge {a}\left({N}-2\right)={a}\left(0\right)\right)\right)$
46 eqtr3 ${⊢}\left(\left|{p}\right|={N}\wedge \left|{a}\right|={N}\right)\to \left|{p}\right|=\left|{a}\right|$
47 46 expcom ${⊢}\left|{a}\right|={N}\to \left(\left|{p}\right|={N}\to \left|{p}\right|=\left|{a}\right|\right)$
48 47 ad2antlr ${⊢}\left(\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\wedge \left({a}\left(0\right)={X}\wedge {a}\left({N}-2\right)={a}\left(0\right)\right)\right)\to \left(\left|{p}\right|={N}\to \left|{p}\right|=\left|{a}\right|\right)$
49 48 com12 ${⊢}\left|{p}\right|={N}\to \left(\left(\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\wedge \left({a}\left(0\right)={X}\wedge {a}\left({N}-2\right)={a}\left(0\right)\right)\right)\to \left|{p}\right|=\left|{a}\right|\right)$
50 49 ad2antlr ${⊢}\left(\left({p}\in \mathrm{Word}{V}\wedge \left|{p}\right|={N}\right)\wedge \left({p}\left(0\right)={X}\wedge {p}\left({N}-2\right)={p}\left(0\right)\right)\right)\to \left(\left(\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\wedge \left({a}\left(0\right)={X}\wedge {a}\left({N}-2\right)={a}\left(0\right)\right)\right)\to \left|{p}\right|=\left|{a}\right|\right)$
51 50 imp ${⊢}\left(\left(\left({p}\in \mathrm{Word}{V}\wedge \left|{p}\right|={N}\right)\wedge \left({p}\left(0\right)={X}\wedge {p}\left({N}-2\right)={p}\left(0\right)\right)\right)\wedge \left(\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\wedge \left({a}\left(0\right)={X}\wedge {a}\left({N}-2\right)={a}\left(0\right)\right)\right)\right)\to \left|{p}\right|=\left|{a}\right|$
52 35 45 51 syl2an ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left|{p}\right|=\left|{a}\right|$
53 52 3ad2ant2 ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to \left|{p}\right|=\left|{a}\right|$
54 27 simprd ${⊢}\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\to \left|{p}\right|={N}$
55 54 adantr ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to \left|{p}\right|={N}$
56 55 eqcomd ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to {N}=\left|{p}\right|$
57 56 adantr ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {N}=\left|{p}\right|$
58 57 oveq1d ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {N}-2=\left|{p}\right|-2$
59 58 oveq2d ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {p}\mathrm{prefix}\left({N}-2\right)={p}\mathrm{prefix}\left(\left|{p}\right|-2\right)$
60 58 oveq2d ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {a}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)$
61 59 60 eqeq12d ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)↔{p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)\right)$
62 61 biimpcd ${⊢}{p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\to \left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)\right)$
63 62 adantr ${⊢}\left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\to \left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)\right)$
64 63 impcom ${⊢}\left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to {p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)$
65 55 oveq1d ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to \left|{p}\right|-2={N}-2$
66 65 fveq2d ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to {p}\left(\left|{p}\right|-2\right)={p}\left({N}-2\right)$
67 66 31 eqtrd ${⊢}\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\to {p}\left(\left|{p}\right|-2\right)={X}$
68 67 adantr ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {p}\left(\left|{p}\right|-2\right)={X}$
69 41 eqcomd ${⊢}\left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\to {X}={a}\left({N}-2\right)$
70 69 adantl ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {X}={a}\left({N}-2\right)$
71 58 fveq2d ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {a}\left({N}-2\right)={a}\left(\left|{p}\right|-2\right)$
72 70 71 eqtrd ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {X}={a}\left(\left|{p}\right|-2\right)$
73 68 72 eqtrd ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {p}\left(\left|{p}\right|-2\right)={a}\left(\left|{p}\right|-2\right)$
74 73 adantr ${⊢}\left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to {p}\left(\left|{p}\right|-2\right)={a}\left(\left|{p}\right|-2\right)$
75 lsw ${⊢}{p}\in \mathrm{Word}{V}\to \mathrm{lastS}\left({p}\right)={p}\left(\left|{p}\right|-1\right)$
76 fvoveq1 ${⊢}\left|{p}\right|={N}\to {p}\left(\left|{p}\right|-1\right)={p}\left({N}-1\right)$
77 75 76 sylan9eq ${⊢}\left({p}\in \mathrm{Word}{V}\wedge \left|{p}\right|={N}\right)\to \mathrm{lastS}\left({p}\right)={p}\left({N}-1\right)$
78 26 77 syl ${⊢}{p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \mathrm{lastS}\left({p}\right)={p}\left({N}-1\right)$
79 78 eqcomd ${⊢}{p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to {p}\left({N}-1\right)=\mathrm{lastS}\left({p}\right)$
80 79 ad3antrrr ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {p}\left({N}-1\right)=\mathrm{lastS}\left({p}\right)$
81 lsw ${⊢}{a}\in \mathrm{Word}{V}\to \mathrm{lastS}\left({a}\right)={a}\left(\left|{a}\right|-1\right)$
82 81 adantr ${⊢}\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\to \mathrm{lastS}\left({a}\right)={a}\left(\left|{a}\right|-1\right)$
83 oveq1 ${⊢}{N}=\left|{a}\right|\to {N}-1=\left|{a}\right|-1$
84 83 eqcoms ${⊢}\left|{a}\right|={N}\to {N}-1=\left|{a}\right|-1$
85 84 fveq2d ${⊢}\left|{a}\right|={N}\to {a}\left({N}-1\right)={a}\left(\left|{a}\right|-1\right)$
86 85 eqeq2d ${⊢}\left|{a}\right|={N}\to \left(\mathrm{lastS}\left({a}\right)={a}\left({N}-1\right)↔\mathrm{lastS}\left({a}\right)={a}\left(\left|{a}\right|-1\right)\right)$
87 86 adantl ${⊢}\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\to \left(\mathrm{lastS}\left({a}\right)={a}\left({N}-1\right)↔\mathrm{lastS}\left({a}\right)={a}\left(\left|{a}\right|-1\right)\right)$
88 82 87 mpbird ${⊢}\left({a}\in \mathrm{Word}{V}\wedge \left|{a}\right|={N}\right)\to \mathrm{lastS}\left({a}\right)={a}\left({N}-1\right)$
89 36 88 syl ${⊢}{a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \mathrm{lastS}\left({a}\right)={a}\left({N}-1\right)$
90 89 eqcomd ${⊢}{a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to {a}\left({N}-1\right)=\mathrm{lastS}\left({a}\right)$
91 90 adantr ${⊢}\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\to {a}\left({N}-1\right)=\mathrm{lastS}\left({a}\right)$
92 91 ad2antrl ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {a}\left({N}-1\right)=\mathrm{lastS}\left({a}\right)$
93 80 92 eqeq12d ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left({p}\left({N}-1\right)={a}\left({N}-1\right)↔\mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)\right)$
94 93 biimpd ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left({p}\left({N}-1\right)={a}\left({N}-1\right)\to \mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)\right)$
95 94 adantld ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left(\left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\to \mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)\right)$
96 95 imp ${⊢}\left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to \mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)$
97 64 74 96 3jca ${⊢}\left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to \left({p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)\wedge {p}\left(\left|{p}\right|-2\right)={a}\left(\left|{p}\right|-2\right)\wedge \mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)\right)$
98 97 3adant1 ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to \left({p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)\wedge {p}\left(\left|{p}\right|-2\right)={a}\left(\left|{p}\right|-2\right)\wedge \mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)\right)$
99 1 clwwlknwrd ${⊢}{p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to {p}\in \mathrm{Word}{V}$
100 99 ad3antrrr ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {p}\in \mathrm{Word}{V}$
101 100 3ad2ant2 ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to {p}\in \mathrm{Word}{V}$
102 1 clwwlknwrd ${⊢}{a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to {a}\in \mathrm{Word}{V}$
103 102 adantr ${⊢}\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\to {a}\in \mathrm{Word}{V}$
104 103 ad2antrl ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to {a}\in \mathrm{Word}{V}$
105 104 3ad2ant2 ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to {a}\in \mathrm{Word}{V}$
106 clwwlknlen ${⊢}{p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left|{p}\right|={N}$
107 eluz2b1 ${⊢}{N}\in {ℤ}_{\ge 2}↔\left({N}\in ℤ\wedge 1<{N}\right)$
108 breq2 ${⊢}{N}=\left|{p}\right|\to \left(1<{N}↔1<\left|{p}\right|\right)$
109 108 eqcoms ${⊢}\left|{p}\right|={N}\to \left(1<{N}↔1<\left|{p}\right|\right)$
110 109 biimpcd ${⊢}1<{N}\to \left(\left|{p}\right|={N}\to 1<\left|{p}\right|\right)$
111 107 110 simplbiim ${⊢}{N}\in {ℤ}_{\ge 2}\to \left(\left|{p}\right|={N}\to 1<\left|{p}\right|\right)$
112 14 106 111 syl2imc ${⊢}{p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left({N}\in {ℤ}_{\ge 3}\to 1<\left|{p}\right|\right)$
113 112 ad3antrrr ${⊢}\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left({N}\in {ℤ}_{\ge 3}\to 1<\left|{p}\right|\right)$
114 113 impcom ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\right)\to 1<\left|{p}\right|$
115 114 3adant3 ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to 1<\left|{p}\right|$
116 2swrd2eqwrdeq ${⊢}\left({p}\in \mathrm{Word}{V}\wedge {a}\in \mathrm{Word}{V}\wedge 1<\left|{p}\right|\right)\to \left({p}={a}↔\left(\left|{p}\right|=\left|{a}\right|\wedge \left({p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)\wedge {p}\left(\left|{p}\right|-2\right)={a}\left(\left|{p}\right|-2\right)\wedge \mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)\right)\right)\right)$
117 101 105 115 116 syl3anc ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to \left({p}={a}↔\left(\left|{p}\right|=\left|{a}\right|\wedge \left({p}\mathrm{prefix}\left(\left|{p}\right|-2\right)={a}\mathrm{prefix}\left(\left|{p}\right|-2\right)\wedge {p}\left(\left|{p}\right|-2\right)={a}\left(\left|{p}\right|-2\right)\wedge \mathrm{lastS}\left({p}\right)=\mathrm{lastS}\left({a}\right)\right)\right)\right)$
118 53 98 117 mpbir2and ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\wedge \left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\right)\to {p}={a}$
119 118 3exp ${⊢}{N}\in {ℤ}_{\ge 3}\to \left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left(\left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\to {p}={a}\right)\right)$
120 119 3ad2ant3 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left(\left(\left({p}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {p}\left(0\right)={X}\right)\wedge {p}\left({N}-2\right)={X}\right)\wedge \left(\left({a}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\wedge {a}\left({N}-2\right)={X}\right)\right)\to \left(\left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\to {p}={a}\right)\right)$
121 25 120 sylbid ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)\to \left(\left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\to {p}={a}\right)\right)$
122 121 imp ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)\right)\to \left(\left({p}\mathrm{prefix}\left({N}-2\right)={a}\mathrm{prefix}\left({N}-2\right)\wedge {p}\left({N}-1\right)={a}\left({N}-1\right)\right)\to {p}={a}\right)$
123 13 122 syl5bi ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)\right)\to \left(⟨{p}\mathrm{prefix}\left({N}-2\right),{p}\left({N}-1\right)⟩=⟨{a}\mathrm{prefix}\left({N}-2\right),{a}\left({N}-1\right)⟩\to {p}={a}\right)$
124 10 123 sylbid ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({p}\in \left({X}{C}{N}\right)\wedge {a}\in \left({X}{C}{N}\right)\right)\right)\to \left({T}\left({p}\right)={T}\left({a}\right)\to {p}={a}\right)$
125 124 ralrimivva ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \forall {p}\in \left({X}{C}{N}\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in \left({X}{C}{N}\right)\phantom{\rule{.4em}{0ex}}\left({T}\left({p}\right)={T}\left({a}\right)\to {p}={a}\right)$
126 dff13 ${⊢}{T}:{X}{C}{N}\underset{1-1}{⟶}{F}×\left({G}\mathrm{NeighbVtx}{X}\right)↔\left({T}:{X}{C}{N}⟶{F}×\left({G}\mathrm{NeighbVtx}{X}\right)\wedge \forall {p}\in \left({X}{C}{N}\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in \left({X}{C}{N}\right)\phantom{\rule{.4em}{0ex}}\left({T}\left({p}\right)={T}\left({a}\right)\to {p}={a}\right)\right)$
127 5 125 126 sylanbrc ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to {T}:{X}{C}{N}\underset{1-1}{⟶}{F}×\left({G}\mathrm{NeighbVtx}{X}\right)$