Metamath Proof Explorer


Theorem wwlksext2clwwlk

Description: If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Revised by AV, 14-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 clwwlkext2edg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 clwwlkext2edg.e 𝐸 = ( Edg ‘ 𝐺 )
3 wwlknbp1 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
4 1 wrdeqi Word 𝑉 = Word ( Vtx ‘ 𝐺 )
5 4 eleq2i ( 𝑊 ∈ Word 𝑉𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
6 5 biimpri ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 )
7 6 3ad2ant2 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑊 ∈ Word 𝑉 )
8 7 ad2antlr ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → 𝑊 ∈ Word 𝑉 )
9 s1cl ( 𝑍𝑉 → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
10 9 adantl ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
11 ccatcl ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 )
12 8 10 11 syl2anc ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 )
13 12 adantr ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 )
14 1 2 wwlknp ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
15 simplll ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑊 ∈ Word 𝑉 )
16 9 adantr ( ( 𝑍𝑉𝑁 ∈ ℕ0 ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
17 16 ad2antlr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
18 elfzo0 ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) )
19 simp1 ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → 𝑖 ∈ ℕ0 )
20 peano2nn ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
21 20 3ad2ant2 ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → ( 𝑁 + 1 ) ∈ ℕ )
22 nn0re ( 𝑖 ∈ ℕ0𝑖 ∈ ℝ )
23 22 3ad2ant1 ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → 𝑖 ∈ ℝ )
24 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
25 24 3ad2ant2 ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → 𝑁 ∈ ℝ )
26 peano2re ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
27 24 26 syl ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
28 27 3ad2ant2 ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → ( 𝑁 + 1 ) ∈ ℝ )
29 simp3 ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → 𝑖 < 𝑁 )
30 24 ltp1d ( 𝑁 ∈ ℕ → 𝑁 < ( 𝑁 + 1 ) )
31 30 3ad2ant2 ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → 𝑁 < ( 𝑁 + 1 ) )
32 23 25 28 29 31 lttrd ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → 𝑖 < ( 𝑁 + 1 ) )
33 elfzo0 ( 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑖 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ ∧ 𝑖 < ( 𝑁 + 1 ) ) )
34 19 21 32 33 syl3anbrc ( ( 𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
35 18 34 sylbi ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
36 35 adantl ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
37 oveq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
38 37 adantl ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
39 38 eleq2d ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
40 39 ad2antrr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
41 36 40 mpbird ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
42 ccatval1 ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) = ( 𝑊𝑖 ) )
43 15 17 41 42 syl3anc ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) = ( 𝑊𝑖 ) )
44 fzonn0p1p1 ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
45 44 adantl ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
46 37 eleq2d ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
47 46 ad3antlr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
48 45 47 mpbird ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
49 ccatval1 ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
50 15 17 48 49 syl3anc ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
51 43 50 preq12d ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } )
52 51 ex ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ) )
53 52 expcom ( ( 𝑍𝑉𝑁 ∈ ℕ0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ) ) )
54 53 expcom ( 𝑁 ∈ ℕ0 → ( 𝑍𝑉 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
55 54 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑍𝑉 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
56 55 imp ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ) ) )
57 56 expdcom ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
58 57 3imp1 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } )
59 58 eleq1d ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
60 59 ralbidva ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
61 60 biimprd ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
62 61 3exp ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) )
63 62 com34 ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) )
64 63 3imp1 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
65 64 adantr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
66 simpll ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → 𝑊 ∈ Word 𝑉 )
67 9 ad2antrl ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
68 nn0p1gt0 ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) )
69 68 ad2antll ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → 0 < ( 𝑁 + 1 ) )
70 breq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
71 70 ad2antlr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
72 69 71 mpbird ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
73 hashneq0 ( 𝑊 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
74 73 ad2antrr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
75 72 74 mpbid ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → 𝑊 ≠ ∅ )
76 ccatval1lsw ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
77 66 67 75 76 syl3anc ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
78 oveq1 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
79 78 ad2antlr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
80 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
81 80 ad2antll ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℂ )
82 pncan1 ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
83 81 82 syl ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
84 79 83 eqtrd ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
85 84 fveq2d ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) )
86 77 85 eqtr3d ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( lastS ‘ 𝑊 ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) )
87 ccatws1ls ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑍 )
88 87 ad2ant2r ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑍 )
89 fveq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) )
90 89 ad2antlr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) )
91 88 90 eqtr3d ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → 𝑍 = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) )
92 86 91 preq12d ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑍𝑉𝑁 ∈ ℕ0 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } )
93 92 expcom ( ( 𝑍𝑉𝑁 ∈ ℕ0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ) )
94 93 expcom ( 𝑁 ∈ ℕ0 → ( 𝑍𝑉 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ) ) )
95 94 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑍𝑉 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ) ) )
96 95 imp ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ) )
97 96 com12 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ) )
98 97 3adant3 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ) )
99 98 imp ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } )
100 99 eleq1d ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ↔ { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
101 100 biimpa ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 )
102 simprl1 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → 𝑁 ∈ ℕ0 )
103 102 adantr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → 𝑁 ∈ ℕ0 )
104 fveq2 ( 𝑖 = 𝑁 → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) )
105 fvoveq1 ( 𝑖 = 𝑁 → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) )
106 104 105 preq12d ( 𝑖 = 𝑁 → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } )
107 106 eleq1d ( 𝑖 = 𝑁 → ( { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
108 107 ralsng ( 𝑁 ∈ ℕ0 → ( ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
109 103 108 syl ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
110 101 109 mpbird ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
111 ralunb ( ∀ 𝑖 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
112 65 110 111 sylanbrc ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
113 elnn0uz ( 𝑁 ∈ ℕ0𝑁 ∈ ( ℤ ‘ 0 ) )
114 102 113 sylib ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → 𝑁 ∈ ( ℤ ‘ 0 ) )
115 114 adantr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → 𝑁 ∈ ( ℤ ‘ 0 ) )
116 fzosplitsn ( 𝑁 ∈ ( ℤ ‘ 0 ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
117 115 116 syl ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
118 117 raleqdv ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
119 112 118 mpbird ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
120 ccatws1len ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
121 120 3ad2ant1 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
122 121 ad2antrr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
123 122 oveq1d ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) )
124 oveq1 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) )
125 124 oveq1d ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) )
126 1cnd ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
127 80 126 addcld ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
128 127 126 pncand ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
129 128 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
130 129 adantr ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
131 125 130 sylan9eq ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
132 131 3ad2antl2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
133 132 adantr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
134 123 133 eqtrd ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( 𝑁 + 1 ) )
135 134 oveq2d ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
136 135 raleqdv ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
137 119 136 mpbird ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
138 137 exp42 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑍𝑉 → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) )
139 14 138 syl ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑍𝑉 → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) )
140 139 imp41 ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
141 140 adantrr ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
142 lswccats1 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
143 8 142 sylancom ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
144 68 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 < ( 𝑁 + 1 ) )
145 70 3ad2ant3 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
146 144 145 mpbird ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
147 146 ad2antlr ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → 0 < ( ♯ ‘ 𝑊 ) )
148 ccatfv0 ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
149 8 10 147 148 syl3anc ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
150 143 149 preq12d ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } )
151 150 eleq1d ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → ( { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ↔ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
152 151 biimprcd ( { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 → ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
153 152 adantl ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
154 153 impcom ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 )
155 13 141 154 3jca ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
156 ccatws1len ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
157 156 3ad2ant2 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
158 124 3ad2ant3 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) )
159 80 126 126 addassd ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + ( 1 + 1 ) ) )
160 1p1e2 ( 1 + 1 ) = 2
161 160 oveq2i ( 𝑁 + ( 1 + 1 ) ) = ( 𝑁 + 2 )
162 159 161 eqtrdi ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
163 162 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
164 157 158 163 3eqtrd ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) )
165 164 ad3antlr ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) )
166 2nn 2 ∈ ℕ
167 nn0nnaddcl ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℕ ) → ( 𝑁 + 2 ) ∈ ℕ )
168 166 167 mpan2 ( 𝑁 ∈ ℕ0 → ( 𝑁 + 2 ) ∈ ℕ )
169 168 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 + 2 ) ∈ ℕ )
170 1 2 isclwwlknx ( ( 𝑁 + 2 ) ∈ ℕ → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) ) ) )
171 169 170 syl ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) ) ) )
172 171 ad3antlr ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) ) ) )
173 155 165 172 mpbir2and ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) )
174 173 exp31 ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑍𝑉 → ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) ) )
175 3 174 mpdan ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑍𝑉 → ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) ) )
176 175 imp ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑍𝑉 ) → ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) )