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

Metamath Proof Explorer

Theorem wwlksm1edg

Description: Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 19-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Assertion wwlksm1edg ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 iswwlks ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
4 lencl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
5 simpl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
6 1red ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 1 ∈ ℝ )
7 2re ⊢ 2 ∈ ℝ
8 7 a1i ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ∈ ℝ )
9 nn0re ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
10 9 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
11 1le2 ⊢ 1 ≤ 2
12 11 a1i ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 1 ≤ 2 )
13 simpr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
14 6 8 10 12 13 letrd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 1 ≤ ( ♯ ‘ 𝑊 ) )
15 5 14 jca ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
16 elnnnn0c ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
17 15 16 sylibr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
18 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
19 17 18 sylibr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
20 nn0ge2m1nn ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ )
21 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ )
22 20 21 sylibr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
23 19 22 jca ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
24 4 23 sylan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
25 inelcm ⊢ ( ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∩ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ≠ ∅ )
26 24 25 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∩ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ≠ ∅ )
27 wrdfn ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
28 27 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 fnresdisj ⊢ ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∩ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ↔ ( 𝑊 ↾ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ) )
30 28 29 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∩ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ↔ ( 𝑊 ↾ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ) )
31 nn0ge2m1nn0 ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
32 10 lem1d ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) )
33 31 5 32 3jca ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
34 4 33 sylan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
35 elfz2nn0 ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
36 34 35 sylibr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
37 pfxres ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ↾ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
38 37 eqeq1d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ ↔ ( 𝑊 ↾ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ) )
39 38 bicomd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ↾ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ↔ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ ) )
40 36 39 syldan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ↾ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ↔ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ ) )
41 30 40 bitr2d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ ↔ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∩ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ∅ ) )
42 41 necon3bid ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ ↔ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∩ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ≠ ∅ ) )
43 26 42 mpbird ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ )
44 43 3ad2antl2 ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ )
45 pfxcl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) )
46 45 a1d ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ) )
47 46 3ad2ant2 ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ) )
48 47 imp ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) )
49 nn0z ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
50 peano2zm ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
51 49 50 syl ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
52 peano2zm ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ℤ )
53 51 52 syl ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ℤ )
54 53 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ℤ )
55 51 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
56 peano2rem ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ )
57 9 56 syl ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ )
58 57 lem1d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) )
59 58 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) )
60 54 55 59 3jca ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
61 4 60 sylan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
62 eluz2 ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ↔ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
63 61 62 sylibr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) )
64 9 lem1d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) )
65 64 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) )
66 31 5 65 3jca ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
67 4 66 sylan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
68 67 35 sylibr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
69 pfxlen ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
70 69 oveq1d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) )
71 68 70 syldan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) )
72 71 fveq2d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) = ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) )
73 63 72 eleqtrrd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) )
74 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
75 73 74 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
76 ssralv ⊢ ( ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
77 75 76 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
78 68 69 syldan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
79 78 oveq1d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) )
80 79 oveq2d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) )
81 80 eleq2d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ↔ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) )
82 simpl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
83 82 adantr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
84 36 adantr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
85 4 31 sylan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
86 nn0z ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
87 fzossrbm1 ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
88 86 87 syl ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
89 85 88 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
90 89 sselda ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
91 pfxfv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) = ( 𝑊 ‘ 𝑥 ) )
92 83 84 90 91 syl3anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) = ( 𝑊 ‘ 𝑥 ) )
93 92 eqcomd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → ( 𝑊 ‘ 𝑥 ) = ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) )
94 4 20 sylan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ )
95 elfzom1p1elfzo ⊢ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → ( 𝑥 + 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
96 94 95 sylan ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → ( 𝑥 + 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
97 pfxfv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑥 + 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) = ( 𝑊 ‘ ( 𝑥 + 1 ) ) )
98 83 84 96 97 syl3anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) = ( 𝑊 ‘ ( 𝑥 + 1 ) ) )
99 98 eqcomd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → ( 𝑊 ‘ ( 𝑥 + 1 ) ) = ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) )
100 93 99 preq12d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) ) → { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } = { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } )
101 100 ex ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) → { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } = { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ) )
102 81 101 sylbid ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) → { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } = { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ) )
103 102 imp ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ) → { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } = { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } )
104 103 eleq1d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ) → ( { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
105 104 biimpd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ) → ( { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
106 105 ralimdva ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
107 77 106 syld ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
108 107 expcom ⊢ ( 2 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
109 108 com3l ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
110 109 a1i ⊢ ( 𝑊 ≠ ∅ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
111 110 3imp1 ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
112 1 2 iswwlks ⊢ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ ∧ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝑥 ) , ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
113 44 48 111 112 syl3anbrc ⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )
114 113 ex ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑥 ) , ( 𝑊 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ) )
115 3 114 sylbi ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ) )
116 115 imp ⊢ ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )