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 = Vtx ⁡ G
clwwlknonex2.e ⊢ E = Edg ⁡ G
Assertion clwwlknonex2lem2 ⊢ X ∈ V ∧ Y ∈ V ∧ N ∈ ℤ ≥ 3 ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N − 2 ∧ W ⁡ 0 = X ∧ X Y ∈ E → ∀ i ∈ 0 ..^ W − 1 ∪ W − 1 W W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ i + 1 ∈ E

Proof

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