Metamath Proof Explorer

Theorem wwlksnextbi

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

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

Proof

Step Hyp Ref Expression
1 wwlksnext.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlksnext.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 wwlknp ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
4 wwlksnred ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
5 4 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
6 fveqeq2 ⊢ ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) )
7 6 3ad2ant2 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) )
8 7 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) )
9 s1cl ⊢ ( 𝑆 ∈ 𝑉 → ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 )
10 9 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) → ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 )
11 10 anim1ci ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( 𝑇 ∈ Word 𝑉 ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) )
12 ccatlen ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) )
13 11 12 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) )
14 13 eqeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ) )
15 s1len ⊢ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1
16 15 a1i ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 )
17 16 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) = ( ( ♯ ‘ 𝑇 ) + 1 ) )
18 17 eqeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ( ♯ ‘ 𝑇 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) ) )
19 lencl ⊢ ( 𝑇 ∈ Word 𝑉 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
20 19 nn0cnd ⊢ ( 𝑇 ∈ Word 𝑉 → ( ♯ ‘ 𝑇 ) ∈ ℂ )
21 20 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
22 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
23 22 nn0cnd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
24 23 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( 𝑁 + 1 ) ∈ ℂ )
25 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → 1 ∈ ℂ )
26 21 24 25 addcan2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( ( ♯ ‘ 𝑇 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) )
27 14 18 26 3bitrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) )
28 oveq2 ⊢ ( ( 𝑁 + 1 ) = ( ♯ ‘ 𝑇 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( ♯ ‘ 𝑇 ) ) )
29 28 eqcoms ⊢ ( ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( ♯ ‘ 𝑇 ) ) )
30 pfxccat1 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( ♯ ‘ 𝑇 ) ) = 𝑇 )
31 11 30 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( ♯ ‘ 𝑇 ) ) = 𝑇 )
32 29 31 sylan9eqr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 )
33 32 ex ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝑇 ) = ( 𝑁 + 1 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 ) )
34 27 33 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑇 ∈ Word 𝑉 ) → ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 ) )
35 34 3ad2antr1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( ♯ ‘ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 ) )
36 8 35 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 ) )
37 36 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 )
38 oveq1 ⊢ ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) = ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) )
39 38 eqeq1d ⊢ ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑇 ↔ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 ) )
40 39 3ad2ant2 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑇 ↔ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 ) )
41 40 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑇 ↔ ( ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) prefix ( 𝑁 + 1 ) ) = 𝑇 ) )
42 37 41 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑇 )
43 42 eleq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
44 43 biimpd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
45 44 ex ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) )
46 45 com23 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) )
47 5 46 syld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) )
48 47 com13 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) )
49 48 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) )
50 3 49 mpcom ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
51 50 com12 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
52 1 2 wwlksnext ⊢ ( ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) )
53 eleq1 ⊢ ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
54 52 53 syl5ibrcom ⊢ ( ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑆 ∈ 𝑉 ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
55 54 3exp ⊢ ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑆 ∈ 𝑉 → ( { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 → ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ) )
56 55 com23 ⊢ ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → ( { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 → ( 𝑆 ∈ 𝑉 → ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ) )
57 56 com14 ⊢ ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) → ( { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 → ( 𝑆 ∈ 𝑉 → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ) )
58 57 imp ⊢ ( ( 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑆 ∈ 𝑉 → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
59 58 3adant1 ⊢ ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑆 ∈ 𝑉 → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
60 59 com12 ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
61 60 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
62 61 imp ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
63 51 62 impbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑇 ∈ Word 𝑉 ∧ 𝑊 = ( 𝑇 ++ ⟨“ 𝑆 ”⟩ ) ∧ { ( lastS ‘ 𝑇 ) , 𝑆 } ∈ 𝐸 ) ) → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ 𝑇 ∈ ( 𝑁 WWalksN 𝐺 ) ) )