This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 112 117 raleqtrrdv ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
119 ccatws1len ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
120 119 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
121 120 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
122 121 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) )
123 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) )
124 123 oveq1d ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) )
125 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
126 80 125 addcld ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
127 126 125 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
128 127 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
129 128 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
130 124 129 sylan9eq ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
131 130 3ad2antl2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
132 131 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
133 122 132 eqtrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( 𝑁 + 1 ) )
134 133 oveq2d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
135 118 134 raleqtrrdv ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑍 ∈ 𝑉 ) ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
136 135 exp42 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑍 ∈ 𝑉 → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) )
137 14 136 syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑍 ∈ 𝑉 → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) )
138 137 imp41 ⊢ ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) ∧ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
139 138 adantrr ⊢ ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
140 lswccats1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
141 8 140 sylancom ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
142 68 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 < ( 𝑁 + 1 ) )
143 70 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
144 142 143 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
145 144 ad2antlr ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) → 0 < ( ♯ ‘ 𝑊 ) )
146 ccatfv0 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
147 8 10 145 146 syl3anc ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
148 141 147 preq12d ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } )
149 148 eleq1d ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) → ( { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ↔ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
150 149 biimprcd ⊢ ( { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 → ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
151 150 adantl ⊢ ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
152 151 impcom ⊢ ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 )
153 13 139 152 3jca ⊢ ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) )
154 ccatws1len ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
155 154 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
156 123 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) )
157 80 125 125 addassd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + ( 1 + 1 ) ) )
158 1p1e2 ⊢ ( 1 + 1 ) = 2
159 158 oveq2i ⊢ ( 𝑁 + ( 1 + 1 ) ) = ( 𝑁 + 2 )
160 157 159 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
161 160 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
162 155 156 161 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) )
163 162 ad3antlr ⊢ ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) )
164 2nn ⊢ 2 ∈ ℕ
165 nn0nnaddcl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℕ ) → ( 𝑁 + 2 ) ∈ ℕ )
166 164 165 mpan2 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 2 ) ∈ ℕ )
167 166 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 + 2 ) ∈ ℕ )
168 1 2 isclwwlknx ⊢ ( ( 𝑁 + 2 ) ∈ ℕ → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) ) ) )
169 167 168 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) ) ) )
170 169 ad3antlr ⊢ ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( 𝑁 + 2 ) ) ) )
171 153 163 170 mpbir2and ⊢ ( ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑍 ∈ 𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) )
172 171 exp31 ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑍 ∈ 𝑉 → ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) ) )
173 3 172 mpdan ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑍 ∈ 𝑉 → ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) ) )
174 173 imp ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑍 ∈ 𝑉 ) → ( ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) )