Metamath Proof Explorer

Theorem clwwlknonex2lem2

Description: Lemma 2 for clwwlknonex2 : Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018) (Revised by AV, 27-Jan-2022)

Ref Expression
Hypotheses clwwlknonex2.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
clwwlknonex2.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion clwwlknonex2lem2 ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \forall {i}\in \left(\left(0..^\left|{W}\right|-1\right)\cup \left\{\left|{W}\right|-1,\left|{W}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}$

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 clwwlknonex2.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 simpl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {W}\in \mathrm{Word}{V}$
4 3 adantr ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {W}\in \mathrm{Word}{V}$
5 elfzonn0 ${⊢}{i}\in \left(0..^\left|{W}\right|-1\right)\to {i}\in {ℕ}_{0}$
6 5 adantl ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {i}\in {ℕ}_{0}$
7 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
8 elfzo0 ${⊢}{i}\in \left(0..^\left|{W}\right|-1\right)↔\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|-1\in ℕ\wedge {i}<\left|{W}\right|-1\right)$
9 nn0re ${⊢}{i}\in {ℕ}_{0}\to {i}\in ℝ$
10 9 adantr ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to {i}\in ℝ$
11 nn0re ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left|{W}\right|\in ℝ$
12 peano2rem ${⊢}\left|{W}\right|\in ℝ\to \left|{W}\right|-1\in ℝ$
13 11 12 syl ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left|{W}\right|-1\in ℝ$
14 13 adantl ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left|{W}\right|-1\in ℝ$
15 11 adantl ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left|{W}\right|\in ℝ$
16 10 14 15 3jca ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left({i}\in ℝ\wedge \left|{W}\right|-1\in ℝ\wedge \left|{W}\right|\in ℝ\right)$
17 11 ltm1d ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left|{W}\right|-1<\left|{W}\right|$
18 17 adantl ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left|{W}\right|-1<\left|{W}\right|$
19 lttr ${⊢}\left({i}\in ℝ\wedge \left|{W}\right|-1\in ℝ\wedge \left|{W}\right|\in ℝ\right)\to \left(\left({i}<\left|{W}\right|-1\wedge \left|{W}\right|-1<\left|{W}\right|\right)\to {i}<\left|{W}\right|\right)$
20 19 expcomd ${⊢}\left({i}\in ℝ\wedge \left|{W}\right|-1\in ℝ\wedge \left|{W}\right|\in ℝ\right)\to \left(\left|{W}\right|-1<\left|{W}\right|\to \left({i}<\left|{W}\right|-1\to {i}<\left|{W}\right|\right)\right)$
21 16 18 20 sylc ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left({i}<\left|{W}\right|-1\to {i}<\left|{W}\right|\right)$
22 21 impancom ${⊢}\left({i}\in {ℕ}_{0}\wedge {i}<\left|{W}\right|-1\right)\to \left(\left|{W}\right|\in {ℕ}_{0}\to {i}<\left|{W}\right|\right)$
23 22 3adant2 ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|-1\in ℕ\wedge {i}<\left|{W}\right|-1\right)\to \left(\left|{W}\right|\in {ℕ}_{0}\to {i}<\left|{W}\right|\right)$
24 8 23 sylbi ${⊢}{i}\in \left(0..^\left|{W}\right|-1\right)\to \left(\left|{W}\right|\in {ℕ}_{0}\to {i}<\left|{W}\right|\right)$
25 7 24 syl5com ${⊢}{W}\in \mathrm{Word}{V}\to \left({i}\in \left(0..^\left|{W}\right|-1\right)\to {i}<\left|{W}\right|\right)$
26 25 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left({i}\in \left(0..^\left|{W}\right|-1\right)\to {i}<\left|{W}\right|\right)$
27 26 imp ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {i}<\left|{W}\right|$
28 ccat2s1fvw ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {i}\in {ℕ}_{0}\wedge {i}<\left|{W}\right|\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right)={W}\left({i}\right)$
29 4 6 27 28 syl3anc ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right)={W}\left({i}\right)$
30 29 eqcomd ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {W}\left({i}\right)=\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right)$
31 peano2nn0 ${⊢}{i}\in {ℕ}_{0}\to {i}+1\in {ℕ}_{0}$
32 6 31 syl ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {i}+1\in {ℕ}_{0}$
33 1red ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to 1\in ℝ$
34 10 33 15 ltaddsubd ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left({i}+1<\left|{W}\right|↔{i}<\left|{W}\right|-1\right)$
35 34 biimprd ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to \left({i}<\left|{W}\right|-1\to {i}+1<\left|{W}\right|\right)$
36 35 impancom ${⊢}\left({i}\in {ℕ}_{0}\wedge {i}<\left|{W}\right|-1\right)\to \left(\left|{W}\right|\in {ℕ}_{0}\to {i}+1<\left|{W}\right|\right)$
37 36 3adant2 ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{W}\right|-1\in ℕ\wedge {i}<\left|{W}\right|-1\right)\to \left(\left|{W}\right|\in {ℕ}_{0}\to {i}+1<\left|{W}\right|\right)$
38 8 37 sylbi ${⊢}{i}\in \left(0..^\left|{W}\right|-1\right)\to \left(\left|{W}\right|\in {ℕ}_{0}\to {i}+1<\left|{W}\right|\right)$
39 7 38 mpan9 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {i}+1<\left|{W}\right|$
40 39 adantlr ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {i}+1<\left|{W}\right|$
41 ccat2s1fvw ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {i}+1\in {ℕ}_{0}\wedge {i}+1<\left|{W}\right|\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)={W}\left({i}+1\right)$
42 4 32 40 41 syl3anc ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)={W}\left({i}+1\right)$
43 42 eqcomd ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to {W}\left({i}+1\right)=\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)$
44 30 43 preq12d ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to \left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}=\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}$
45 44 eleq1d ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|-1\right)\right)\to \left(\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}↔\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
46 45 ralbidva ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}↔\forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
47 46 biimpd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
48 47 impancom ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
49 48 3adant3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
50 49 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
51 50 com12 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
52 51 a1dd ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)\right)$
53 52 3adant3 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)\right)$
54 53 imp31 ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}$
55 ax-1 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left({X}\in {V}\wedge {Y}\in {V}\right)\right)$
56 55 3adant3 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left({X}\in {V}\wedge {Y}\in {V}\right)\right)$
57 simpl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to {W}\in \mathrm{Word}{V}$
58 oveq1 ${⊢}\left|{W}\right|={N}-2\to \left|{W}\right|-1={N}-2-1$
59 58 adantr ${⊢}\left(\left|{W}\right|={N}-2\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left|{W}\right|-1={N}-2-1$
60 eluzelcn ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}\in ℂ$
61 2cnd ${⊢}{N}\in {ℤ}_{\ge 3}\to 2\in ℂ$
62 1cnd ${⊢}{N}\in {ℤ}_{\ge 3}\to 1\in ℂ$
63 60 61 62 subsub4d ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-2-1={N}-\left(2+1\right)$
64 2p1e3 ${⊢}2+1=3$
65 64 a1i ${⊢}{N}\in {ℤ}_{\ge 3}\to 2+1=3$
66 65 oveq2d ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-\left(2+1\right)={N}-3$
67 uznn0sub ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-3\in {ℕ}_{0}$
68 66 67 eqeltrd ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-\left(2+1\right)\in {ℕ}_{0}$
69 63 68 eqeltrd ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-2-1\in {ℕ}_{0}$
70 69 adantl ${⊢}\left(\left|{W}\right|={N}-2\wedge {N}\in {ℤ}_{\ge 3}\right)\to {N}-2-1\in {ℕ}_{0}$
71 59 70 eqeltrd ${⊢}\left(\left|{W}\right|={N}-2\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left|{W}\right|-1\in {ℕ}_{0}$
72 71 ancoms ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\to \left|{W}\right|-1\in {ℕ}_{0}$
73 72 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left|{W}\right|-1\in {ℕ}_{0}$
74 7 11 syl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℝ$
75 74 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left|{W}\right|\in ℝ$
76 75 ltm1d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left|{W}\right|-1<\left|{W}\right|$
77 57 73 76 3jca ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|-1\in {ℕ}_{0}\wedge \left|{W}\right|-1<\left|{W}\right|\right)$
78 77 ex ${⊢}{W}\in \mathrm{Word}{V}\to \left(\left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|-1\in {ℕ}_{0}\wedge \left|{W}\right|-1<\left|{W}\right|\right)\right)$
79 78 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|-1\in {ℕ}_{0}\wedge \left|{W}\right|-1<\left|{W}\right|\right)\right)$
80 79 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to \left(\left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|-1\in {ℕ}_{0}\wedge \left|{W}\right|-1<\left|{W}\right|\right)\right)$
81 80 imp ${⊢}\left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|-1\in {ℕ}_{0}\wedge \left|{W}\right|-1<\left|{W}\right|\right)$
82 ccat2s1fvw ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|-1\in {ℕ}_{0}\wedge \left|{W}\right|-1<\left|{W}\right|\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right)={W}\left(\left|{W}\right|-1\right)$
83 81 82 syl ${⊢}\left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right)={W}\left(\left|{W}\right|-1\right)$
84 nn0cn ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left|{W}\right|\in ℂ$
85 ax-1cn ${⊢}1\in ℂ$
86 npcan ${⊢}\left(\left|{W}\right|\in ℂ\wedge 1\in ℂ\right)\to \left|{W}\right|-1+1=\left|{W}\right|$
87 84 85 86 sylancl ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left|{W}\right|-1+1=\left|{W}\right|$
88 7 87 syl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|-1+1=\left|{W}\right|$
89 88 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left|{W}\right|-1+1=\left|{W}\right|$
90 89 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to \left|{W}\right|-1+1=\left|{W}\right|$
91 90 fveq2d ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)=\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right)$
92 simp1l ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to {W}\in \mathrm{Word}{V}$
93 eqidd ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to \left|{W}\right|=\left|{W}\right|$
94 simp2l ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to {X}\in {V}$
95 ccatw2s1p1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\wedge {X}\in {V}\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right)={X}$
96 92 93 94 95 syl3anc ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right)={X}$
97 91 96 eqtrd ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)={X}$
98 97 adantr ${⊢}\left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)={X}$
99 83 98 preq12d ${⊢}\left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}=\left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}$
100 lsw ${⊢}{W}\in \mathrm{Word}{V}\to \mathrm{lastS}\left({W}\right)={W}\left(\left|{W}\right|-1\right)$
101 100 adantl ${⊢}\left({W}\left(0\right)={X}\wedge {W}\in \mathrm{Word}{V}\right)\to \mathrm{lastS}\left({W}\right)={W}\left(\left|{W}\right|-1\right)$
102 simpl ${⊢}\left({W}\left(0\right)={X}\wedge {W}\in \mathrm{Word}{V}\right)\to {W}\left(0\right)={X}$
103 101 102 preq12d ${⊢}\left({W}\left(0\right)={X}\wedge {W}\in \mathrm{Word}{V}\right)\to \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}=\left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}$
104 103 eleq1d ${⊢}\left({W}\left(0\right)={X}\wedge {W}\in \mathrm{Word}{V}\right)\to \left(\left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}↔\left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}\in {E}\right)$
105 104 biimpd ${⊢}\left({W}\left(0\right)={X}\wedge {W}\in \mathrm{Word}{V}\right)\to \left(\left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\to \left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}\in {E}\right)$
106 105 expcom ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}\left(0\right)={X}\to \left(\left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\to \left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}\in {E}\right)\right)$
107 106 com23 ${⊢}{W}\in \mathrm{Word}{V}\to \left(\left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\to \left({W}\left(0\right)={X}\to \left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}\in {E}\right)\right)$
108 107 imp31 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge {W}\left(0\right)={X}\right)\to \left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}\in {E}$
109 108 3adant2 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\to \left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}\in {E}$
110 109 adantr ${⊢}\left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left\{{W}\left(\left|{W}\right|-1\right),{X}\right\}\in {E}$
111 99 110 eqeltrd ${⊢}\left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\wedge {W}\left(0\right)={X}\right)\wedge \left({N}\in {ℤ}_{\ge 3}\wedge \left|{W}\right|={N}-2\right)\right)\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}$
112 111 exp520 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({W}\left(0\right)={X}\to \left({N}\in {ℤ}_{\ge 3}\to \left(\left|{W}\right|={N}-2\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)\right)\right)$
113 112 com14 ${⊢}{N}\in {ℤ}_{\ge 3}\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({W}\left(0\right)={X}\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left|{W}\right|={N}-2\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)\right)\right)$
114 113 3ad2ant3 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({W}\left(0\right)={X}\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left|{W}\right|={N}-2\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)\right)\right)$
115 56 114 syld ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left({W}\left(0\right)={X}\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left|{W}\right|={N}-2\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)\right)\right)$
116 115 com25 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left|{W}\right|={N}-2\to \left({W}\left(0\right)={X}\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)\right)\right)$
117 116 com14 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left|{W}\right|={N}-2\to \left({W}\left(0\right)={X}\to \left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)\right)\right)$
118 117 3adant2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left|{W}\right|={N}-2\to \left({W}\left(0\right)={X}\to \left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)\right)\right)$
119 118 3imp ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)\right)$
120 119 impcom ${⊢}\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)$
121 120 imp ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}$
122 eqidd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left|{W}\right|=\left|{W}\right|$
123 simprl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {X}\in {V}$
124 3 122 123 95 syl3anc ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right)={X}$
125 eqid ${⊢}\left|{W}\right|=\left|{W}\right|$
126 ccatw2s1p2 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|=\left|{W}\right|\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)={Y}$
127 125 126 mpanl2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)={Y}$
128 124 127 preq12d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}$
129 128 expcom ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({W}\in \mathrm{Word}{V}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}\right)$
130 129 a1i ${⊢}\left\{{X},{Y}\right\}\in {E}\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left({W}\in \mathrm{Word}{V}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}\right)\right)$
131 130 com13 ${⊢}{W}\in \mathrm{Word}{V}\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}\right)\right)$
132 131 3ad2ant1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}\right)\right)$
133 132 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \left(\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}\right)\right)$
134 133 com12 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}\right)\right)$
135 134 3adant3 ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\to \left(\left\{{X},{Y}\right\}\in {E}\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}\right)\right)$
136 135 imp31 ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}=\left\{{X},{Y}\right\}$
137 simpr ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \left\{{X},{Y}\right\}\in {E}$
138 136 137 eqeltrd ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}\in {E}$
139 ovex ${⊢}\left|{W}\right|-1\in \mathrm{V}$
140 fvex ${⊢}\left|{W}\right|\in \mathrm{V}$
141 fveq2 ${⊢}{i}=\left|{W}\right|-1\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right)=\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right)$
142 fvoveq1 ${⊢}{i}=\left|{W}\right|-1\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)=\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)$
143 141 142 preq12d ${⊢}{i}=\left|{W}\right|-1\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}=\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}$
144 143 eleq1d ${⊢}{i}=\left|{W}\right|-1\to \left(\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}↔\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\right)$
145 fveq2 ${⊢}{i}=\left|{W}\right|\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right)=\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right)$
146 fvoveq1 ${⊢}{i}=\left|{W}\right|\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)=\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)$
147 145 146 preq12d ${⊢}{i}=\left|{W}\right|\to \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}=\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}$
148 147 eleq1d ${⊢}{i}=\left|{W}\right|\to \left(\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}↔\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}\in {E}\right)$
149 139 140 144 148 ralpr ${⊢}\forall {i}\in \left\{\left|{W}\right|-1,\left|{W}\right|\right\}\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}↔\left(\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|-1+1\right)\right\}\in {E}\wedge \left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left(\left|{W}\right|+1\right)\right\}\in {E}\right)$
150 121 138 149 sylanbrc ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \forall {i}\in \left\{\left|{W}\right|-1,\left|{W}\right|\right\}\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}$
151 ralunb ${⊢}\forall {i}\in \left(\left(0..^\left|{W}\right|-1\right)\cup \left\{\left|{W}\right|-1,\left|{W}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}↔\left(\forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\wedge \forall {i}\in \left\{\left|{W}\right|-1,\left|{W}\right|\right\}\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}\right)$
152 54 150 151 sylanbrc ${⊢}\left(\left(\left({X}\in {V}\wedge {Y}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}-2\wedge {W}\left(0\right)={X}\right)\right)\wedge \left\{{X},{Y}\right\}\in {E}\right)\to \forall {i}\in \left(\left(0..^\left|{W}\right|-1\right)\cup \left\{\left|{W}\right|-1,\left|{W}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}\right),\left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({i}+1\right)\right\}\in {E}$