Metamath Proof Explorer

Theorem clwwlkext2edg

Description: If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses clwwlkext2edg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clwwlkext2edg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion clwwlkext2edg ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 clwwlkext2edg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clwwlkext2edg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 clwwlknnn ⊢ ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ )
4 1 2 isclwwlknx ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ) )
5 ige2m2fzo ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
6 5 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
7 6 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
8 oveq1 ⊢ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( 𝑁 − 1 ) )
9 8 oveq2d ⊢ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
10 9 eleq2d ⊢ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
11 10 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
12 7 11 mpbird ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) )
13 fveq2 ⊢ ( 𝑖 = ( 𝑁 − 2 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) )
14 fvoveq1 ⊢ ( 𝑖 = ( 𝑁 − 2 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) )
15 13 14 preq12d ⊢ ( 𝑖 = ( 𝑁 − 2 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } )
16 15 eleq1d ⊢ ( 𝑖 = ( 𝑁 − 2 ) → ( { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ) )
17 16 rspcv ⊢ ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ) )
18 12 17 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ) )
19 wrdlenccats1lenm1 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑊 ) )
20 19 eqcomd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) )
21 20 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) )
22 21 8 sylan9eq ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) )
23 22 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) )
24 23 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) )
25 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ )
26 1cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℂ )
27 25 26 26 subsub4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − ( 1 + 1 ) ) )
28 1p1e2 ⊢ ( 1 + 1 ) = 2
29 28 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 + 1 ) = 2 )
30 29 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − ( 1 + 1 ) ) = ( 𝑁 − 2 ) )
31 27 30 eqtr2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) = ( ( 𝑁 − 1 ) − 1 ) )
32 31 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 − 2 ) = ( ( 𝑁 − 1 ) − 1 ) )
33 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 − 1 ) − 1 ) )
34 33 eqcomd ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( 𝑁 − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
35 32 34 sylan9eq ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
36 35 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
37 24 36 syld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
38 37 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
39 38 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
40 simpl1 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 𝑊 ∈ Word 𝑉 )
41 s1cl ⊢ ( 𝑍 ∈ 𝑉 → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
42 41 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
43 42 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
44 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
45 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
46 1red ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 ∈ ℝ )
47 2re ⊢ 2 ∈ ℝ
48 47 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 2 ∈ ℝ )
49 simpl ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
50 1lt2 ⊢ 1 < 2
51 50 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 < 2 )
52 simpr ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 2 ≤ 𝑁 )
53 46 48 49 51 52 ltletrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 < 𝑁 )
54 1red ⊢ ( 𝑁 ∈ ℝ → 1 ∈ ℝ )
55 id ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
56 54 55 posdifd ⊢ ( 𝑁 ∈ ℝ → ( 1 < 𝑁 ↔ 0 < ( 𝑁 − 1 ) ) )
57 56 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → ( 1 < 𝑁 ↔ 0 < ( 𝑁 − 1 ) ) )
58 53 57 mpbid ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 0 < ( 𝑁 − 1 ) )
59 58 ex ⊢ ( 𝑁 ∈ ℝ → ( 2 ≤ 𝑁 → 0 < ( 𝑁 − 1 ) ) )
60 45 59 syl ⊢ ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 → 0 < ( 𝑁 − 1 ) ) )
61 60 a1i ⊢ ( 2 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 → 0 < ( 𝑁 − 1 ) ) ) )
62 61 3imp ⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → 0 < ( 𝑁 − 1 ) )
63 44 62 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( 𝑁 − 1 ) )
64 63 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( 𝑁 − 1 ) )
65 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 1 ) ) )
66 65 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 1 ) ) )
67 64 66 mpbird ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
68 hashneq0 ⊢ ( 𝑊 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
69 68 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
70 69 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
71 67 70 mpbid ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 𝑊 ≠ ∅ )
72 71 3adantl2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 𝑊 ≠ ∅ )
73 40 43 72 3jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) )
74 73 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ) )
75 24 74 syld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ) )
76 75 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) )
77 ccatval1lsw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
78 76 77 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
79 39 78 eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = ( lastS ‘ 𝑊 ) )
80 2m1e1 ⊢ ( 2 − 1 ) = 1
81 80 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 − 1 ) = 1 )
82 81 eqcomd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 = ( 2 − 1 ) )
83 82 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) = ( 𝑁 − ( 2 − 1 ) ) )
84 2cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℂ )
85 25 84 26 subsubd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − ( 2 − 1 ) ) = ( ( 𝑁 − 2 ) + 1 ) )
86 83 85 eqtr2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) )
87 86 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) )
88 eqeq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) ↔ ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) ) )
89 87 88 syl5ibrcom ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) ) )
90 24 89 syld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) ) )
91 90 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
92 91 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) )
93 id ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) )
94 93 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) )
95 94 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) )
96 ccatws1ls ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑍 )
97 95 96 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑍 )
98 92 97 eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = 𝑍 )
99 79 98 preq12d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } = { ( lastS ‘ 𝑊 ) , 𝑍 } )
100 99 eleq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) )
101 18 100 sylibd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) )
102 101 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) ) )
103 102 com13 ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) ) )
104 103 3ad2ant2 ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) ) )
105 104 imp31 ⊢ ( ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 )
106 94 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) )
107 lswccats1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
108 106 107 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
109 63 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 0 < ( 𝑁 − 1 ) )
110 109 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( 𝑁 − 1 ) )
111 65 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 1 ) ) )
112 110 111 mpbird ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
113 ccatfv0 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
114 40 43 112 113 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
115 108 114 preq12d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } )
116 115 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } ) )
117 24 116 syld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } ) )
118 117 impcom ⊢ ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } )
119 118 eleq1d ⊢ ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ↔ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
120 119 biimpcd ⊢ ( { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 → ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
121 120 3ad2ant3 ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) → ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
122 121 impl ⊢ ( ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 )
123 105 122 jca ⊢ ( ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
124 123 ex ⊢ ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
125 4 124 biimtrdi ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
126 3 125 mpcom ⊢ ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
127 126 impcom ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )