Metamath Proof Explorer

Theorem wwlksnext

Description: Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021)

Ref Expression
Hypotheses wwlksnext.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wwlksnext.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion wwlksnext ( ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 wwlksnext.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlksnext.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 wwlknbp ⊢ ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉 ) )
4 1 2 wwlknp ⊢ ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
5 simp1 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → 𝑇 ∈ Word 𝑉 )
6 simprl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → 𝑆 ∈ 𝑉 )
7 cats1un ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) = ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) )
8 5 6 7 syl2an ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) = ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) )
9 opex ⊢ ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ ∈ V
10 9 snnz ⊢ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ≠ ∅
11 10 neii ⊢ ¬ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } = ∅
12 11 intnan ⊢ ¬ ( 𝑇 = ∅ ∧ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } = ∅ )
13 df-ne ⊢ ( ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) ≠ ∅ ↔ ¬ ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) = ∅ )
14 un00 ⊢ ( ( 𝑇 = ∅ ∧ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } = ∅ ) ↔ ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) = ∅ )
15 13 14 xchbinxr ⊢ ( ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) ≠ ∅ ↔ ¬ ( 𝑇 = ∅ ∧ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } = ∅ ) )
16 12 15 mpbir ⊢ ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) ≠ ∅
17 16 a1i ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( 𝑇 ∪ { ⟨ ( ♯ ‘ 𝑇 ) , 𝑆 ⟩ } ) ≠ ∅ )
18 8 17 eqnetrd ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ )
19 s1cl ⊢ ( 𝑆 ∈ 𝑉 → ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 )
20 19 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 )
21 ccatcl ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 )
22 5 20 21 syl2an ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 )
23 simplrl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ Word 𝑉 )
24 fzossfzop1 ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
25 24 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
26 25 sselda ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
27 oveq2 ⊢ ( ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ♯ ‘ 𝑇 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
28 27 eleq2d ⊢ ( ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
29 28 adantl ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
30 29 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
31 26 30 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
32 ccats1val1 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) = ( 𝑇 ‘ 𝑖 ) )
33 23 31 32 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) = ( 𝑇 ‘ 𝑖 ) )
34 fzonn0p1p1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
35 34 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
36 27 adantl ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( 0 ..^ ( ♯ ‘ 𝑇 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
37 36 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ 𝑇 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
38 35 37 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
39 ccats1val1 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑇 ‘ ( 𝑖 + 1 ) ) )
40 23 38 39 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑇 ‘ ( 𝑖 + 1 ) ) )
41 33 40 preq12d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } )
42 41 exp31 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ) ) )
43 42 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ) ) )
44 43 impcom ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ) )
45 44 imp ⊢ ( ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } )
46 45 eleq1d ⊢ ( ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
47 46 ralbidva ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
48 47 exbiri ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
49 48 com23 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
50 49 3impia ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
51 50 imp ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
52 oveq1 ⊢ ( ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑇 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
53 52 adantl ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑇 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
54 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
55 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
56 54 55 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
57 56 adantl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
58 53 57 sylan9eqr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( ( ♯ ‘ 𝑇 ) − 1 ) = 𝑁 )
59 58 fveq2d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( 𝑇 ‘ ( ( ♯ ‘ 𝑇 ) − 1 ) ) = ( 𝑇 ‘ 𝑁 ) )
60 lsw ⊢ ( 𝑇 ∈ Word 𝑉 → ( lastS ‘ 𝑇 ) = ( 𝑇 ‘ ( ( ♯ ‘ 𝑇 ) − 1 ) ) )
61 60 ad2antrl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( lastS ‘ 𝑇 ) = ( 𝑇 ‘ ( ( ♯ ‘ 𝑇 ) − 1 ) ) )
62 simprl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → 𝑇 ∈ Word 𝑉 )
63 fzonn0p1 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
64 63 ad2antlr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
65 27 eleq2d ⊢ ( ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
66 65 ad2antll ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
67 64 66 mpbird ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
68 ccats1val1 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) = ( 𝑇 ‘ 𝑁 ) )
69 62 67 68 syl2anc ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) = ( 𝑇 ‘ 𝑁 ) )
70 59 61 69 3eqtr4d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( lastS ‘ 𝑇 ) = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) )
71 simpll ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → 𝑆 ∈ 𝑉 )
72 simprr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) )
73 72 eqcomd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( 𝑁 + 1 ) = ( ♯ ‘ 𝑇 ) )
74 ccats1val2 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ ( 𝑁 + 1 ) = ( ♯ ‘ 𝑇 ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) = 𝑆 )
75 74 eqcomd ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ ( 𝑁 + 1 ) = ( ♯ ‘ 𝑇 ) ) → 𝑆 = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) )
76 62 71 73 75 syl3anc ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → 𝑆 = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) )
77 70 76 preq12d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → { ( lastS ‘ 𝑇 ) , 𝑆 } = { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } )
78 77 eleq1d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → ( { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ↔ { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
79 78 biimpcd ⊢ ( { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 → ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
80 79 exp4c ⊢ ( { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 → ( 𝑆 ∈ 𝑉 → ( 𝑁 ∈ ℕ0 → ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) ) ) )
81 80 impcom ⊢ ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑁 ∈ ℕ0 → ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) ) )
82 81 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
83 82 impcom ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 )
84 83 3adantl3 ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 )
85 fveq2 ⊢ ( 𝑖 = 𝑁 → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) )
86 fvoveq1 ⊢ ( 𝑖 = 𝑁 → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) )
87 85 86 preq12d ⊢ ( 𝑖 = 𝑁 → { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } )
88 87 eleq1d ⊢ ( 𝑖 = 𝑁 → ( { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
89 88 ralsng ⊢ ( 𝑁 ∈ ℕ0 → ( ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
90 89 ad2antrl ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑁 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
91 84 90 mpbird ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
92 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ ∀ 𝑖 ∈ { 𝑁 } { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
93 51 91 92 sylanbrc ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ∀ 𝑖 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
94 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
95 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
96 94 95 sylbi ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... 𝑁 ) )
97 fzelp1 ⊢ ( 𝑁 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
98 fzosplit ⊢ ( 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ ( 𝑁 ..^ ( 𝑁 + 1 ) ) ) )
99 96 97 98 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ ( 𝑁 ..^ ( 𝑁 + 1 ) ) ) )
100 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
101 fzosn ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ..^ ( 𝑁 + 1 ) ) = { 𝑁 } )
102 100 101 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ..^ ( 𝑁 + 1 ) ) = { 𝑁 } )
103 102 uneq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ..^ 𝑁 ) ∪ ( 𝑁 ..^ ( 𝑁 + 1 ) ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
104 99 103 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
105 104 ad2antrl ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
106 93 105 raleqtrrdv ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
107 ccatlen ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) )
108 5 20 107 syl2an ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) )
109 108 oveq1d ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) − 1 ) )
110 simpl2 ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) )
111 s1len ⊢ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1
112 111 a1i ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 )
113 110 112 oveq12d ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) )
114 113 oveq1d ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) )
115 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
116 115 nn0cnd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
117 116 55 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
118 117 ad2antrl ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
119 109 114 118 3eqtrd ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) = ( 𝑁 + 1 ) )
120 119 oveq2d ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
121 106 120 raleqtrrdv ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
122 18 22 121 3jca ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
123 108 113 eqtrd ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) )
124 122 123 jca ⊢ ( ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ) → ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) )
125 124 ex ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑇 ‘ 𝑖 ) , ( 𝑇 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
126 4 125 syl ⊢ ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
127 126 expd ⊢ ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 → ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) ) )
128 127 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
129 128 adantll ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
130 iswwlksn ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
131 115 130 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
132 131 adantl ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
133 1 2 iswwlks ⊢ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
134 133 anbi1i ⊢ ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ↔ ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) )
135 132 134 bitrdi ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
136 135 adantr ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ≠ ∅ ∧ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) ) { ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
137 129 136 sylibrd ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
138 137 ex ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
139 138 3adant3 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉 ) → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
140 3 139 mpcom ⊢ ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
141 140 3impib ⊢ ( ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) )