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

Metamath Proof Explorer

Theorem wwlksnred

Description: Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Assertion wwlksnred ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
2 iswwlksn ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
3 1 2 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
6 4 5 iswwlks ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
7 simp1 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
8 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
9 8 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℕ )
10 1 nn0red ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
11 10 lep1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
12 11 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
13 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
14 13 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
15 12 14 mpbird ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) )
16 pfxn0 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ )
17 7 9 15 16 syl3anc ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ )
18 17 3exp ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) ) )
19 18 3ad2ant2 ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) ) )
20 19 imp ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) )
21 20 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ )
22 pfxcl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) )
23 22 3ad2ant2 ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) )
24 23 adantr ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) )
25 24 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) )
26 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) )
27 1 nn0cnd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
28 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
29 27 28 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
30 26 29 sylan9eq ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) )
31 30 oveq2d ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
32 31 raleqdv ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
33 32 adantl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
34 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
35 nn0z ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ )
36 1 35 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ )
37 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
38 37 lep1d ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ ( 𝑁 + 1 ) )
39 34 36 38 3jca ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) )
40 39 ad2antll ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) )
41 eluz2 ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) )
42 40 41 sylibr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
43 fzoss2 ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
44 42 43 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
45 ssralv ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
46 44 45 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
47 simpll ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
48 nn0fz0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
49 1 48 sylib ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
50 49 ad2antll ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
51 fzelp1 ⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
52 50 51 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
53 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
54 53 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) )
55 54 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) )
56 55 adantl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) )
57 52 56 mpbird ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
58 57 adantr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
59 fzossfzop1 ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
60 59 sseld ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
61 60 ad2antll ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
62 61 imp ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
63 pfxfv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
64 47 58 62 63 syl3anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
65 64 eqcomd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑊 ‘ 𝑖 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) )
66 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) )
67 66 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) )
68 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
69 68 eqcomd ⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) )
70 34 69 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) )
71 70 eleq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
72 71 ad2antll ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
73 72 adantr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
74 67 73 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
75 pfxfv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
76 47 58 74 75 syl3anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
77 76 eqcomd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑊 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) )
78 65 77 preq12d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } )
79 78 eleq1d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
80 79 biimpd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
81 80 ralimdva ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
82 46 81 syld ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
83 33 82 sylbid ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
84 83 imp ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
85 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
86 85 28 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
87 86 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ 𝑁 ) )
88 87 ad2antll ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ 𝑁 ) )
89 88 adantr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ 𝑁 ) )
90 89 raleqdv ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
91 84 90 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
92 pfxlen ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
93 57 92 syldan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
94 93 oveq1d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
95 94 oveq2d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) = ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) )
96 95 raleqdv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
97 96 adantr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
98 91 97 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
99 98 exp31 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
100 99 com23 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
101 100 imp ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
102 101 3adant1 ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
103 102 expdimp ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
104 103 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
105 4 5 iswwlks ⊢ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ∧ ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
106 21 25 104 105 syl3anbrc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )
107 peano2nn0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
108 1 107 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
109 elfz2nn0 ⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ↔ ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
110 1 108 11 109 syl3anbrc ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
111 110 adantl ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
112 111 55 mpbird ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
113 112 anim2i ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
114 113 exp32 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) ) )
115 114 3ad2ant2 ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) ) )
116 115 imp ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
117 116 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
118 117 92 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
119 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) ) )
120 119 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) ) )
121 106 118 120 mpbir2and ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) )
122 121 expcom ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
123 6 122 sylanb ⊢ ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
124 123 com12 ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
125 3 124 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )