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 𝐺 ) ) )