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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clwwlknonex2.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion clwwlknonex2lem2 ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) { ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑖 ) , ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )

Proof

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