Metamath Proof Explorer

Theorem wwlksubclwwlk

Description: Any prefix of a word representing a closed walk represents a walk. (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 28-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Assertion wwlksubclwwlk ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑋 prefix 𝑀 ) ∈ ( ( 𝑀 − 1 ) WWalksN 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 clwwlknp ⊢ ( 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑋 ) , ( 𝑋 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
4 pfxcl ⊢ ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) )
5 4 adantr ⊢ ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) → ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) )
6 5 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) )
7 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
8 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
9 8 ex ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
10 7 9 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
11 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
12 7 11 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℤ )
13 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
14 13 lem1d ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ≤ 𝑀 )
15 eluzuzle ⊢ ( ( ( 𝑀 − 1 ) ∈ ℤ ∧ ( 𝑀 − 1 ) ≤ 𝑀 ) → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ) )
16 12 14 15 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ) )
17 10 16 syld ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ) )
18 17 imp ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
19 fzoss2 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( 0 ..^ ( 𝑀 − 1 ) ) ⊆ ( 0 ..^ ( 𝑁 − 1 ) ) )
20 18 19 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 0 ..^ ( 𝑀 − 1 ) ) ⊆ ( 0 ..^ ( 𝑁 − 1 ) ) )
21 20 adantl ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 0 ..^ ( 𝑀 − 1 ) ) ⊆ ( 0 ..^ ( 𝑁 − 1 ) ) )
22 ssralv ⊢ ( ( 0 ..^ ( 𝑀 − 1 ) ) ⊆ ( 0 ..^ ( 𝑁 − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
23 21 22 syl ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
24 simpll ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) )
25 24 adantr ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) )
26 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) )
27 13 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → 𝑀 ∈ ℝ )
28 peano2re ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
29 13 28 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ℝ )
30 29 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → ( 𝑀 + 1 ) ∈ ℝ )
31 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
32 31 ad2antrl ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → 𝑁 ∈ ℝ )
33 13 lep1d ⊢ ( 𝑀 ∈ ℕ → 𝑀 ≤ ( 𝑀 + 1 ) )
34 33 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → 𝑀 ≤ ( 𝑀 + 1 ) )
35 simpr ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( 𝑀 + 1 ) ≤ 𝑁 )
36 35 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → ( 𝑀 + 1 ) ≤ 𝑁 )
37 27 30 32 34 36 letrd ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → 𝑀 ≤ 𝑁 )
38 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
39 38 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )
40 simpr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
41 40 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
42 0red ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → 0 ∈ ℝ )
43 13 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
44 31 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
45 42 43 44 3jca ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
46 45 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
47 38 nn0ge0d ⊢ ( 𝑀 ∈ ℕ → 0 ≤ 𝑀 )
48 47 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → 0 ≤ 𝑀 )
49 48 anim1i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) )
50 letr ⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) → 0 ≤ 𝑁 ) )
51 46 49 50 sylc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 0 ≤ 𝑁 )
52 elnn0z ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
53 41 51 52 sylanbrc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℕ0 )
54 53 adantlrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℕ0 )
55 simpr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ≤ 𝑁 )
56 39 54 55 3jca ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
57 37 56 mpdan ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
58 57 expcom ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
59 58 3adant1 ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
60 26 59 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
61 60 impcom ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
62 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
63 61 62 sylibr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
64 63 adantl ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
65 oveq2 ⊢ ( ( ♯ ‘ 𝑋 ) = 𝑁 → ( 0 ... ( ♯ ‘ 𝑋 ) ) = ( 0 ... 𝑁 ) )
66 65 eleq2d ⊢ ( ( ♯ ‘ 𝑋 ) = 𝑁 → ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ↔ 𝑀 ∈ ( 0 ... 𝑁 ) ) )
67 66 adantl ⊢ ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) → ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ↔ 𝑀 ∈ ( 0 ... 𝑁 ) ) )
68 67 adantr ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ↔ 𝑀 ∈ ( 0 ... 𝑁 ) ) )
69 64 68 mpbird ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) )
70 69 adantr ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) )
71 eluz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ↔ ( ( 𝑀 − 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ≤ 𝑀 ) )
72 12 7 14 71 syl3anbrc ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
73 fzoss2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( 0 ..^ ( 𝑀 − 1 ) ) ⊆ ( 0 ..^ 𝑀 ) )
74 72 73 syl ⊢ ( 𝑀 ∈ ℕ → ( 0 ..^ ( 𝑀 − 1 ) ) ⊆ ( 0 ..^ 𝑀 ) )
75 74 sseld ⊢ ( 𝑀 ∈ ℕ → ( 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
76 75 ad2antrl ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
77 76 imp ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
78 pfxfv ⊢ ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) = ( 𝑋 ‘ 𝑖 ) )
79 25 70 77 78 syl3anc ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) = ( 𝑋 ‘ 𝑖 ) )
80 79 eqcomd ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → ( 𝑋 ‘ 𝑖 ) = ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) )
81 fzonn0p1p1 ⊢ ( 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ( 𝑀 − 1 ) + 1 ) ) )
82 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
83 npcan1 ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
84 82 83 syl ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
85 84 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( 0 ..^ ( ( 𝑀 − 1 ) + 1 ) ) = ( 0 ..^ 𝑀 ) )
86 85 eleq2d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ( 𝑀 − 1 ) + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
87 81 86 syl5ib ⊢ ( 𝑀 ∈ ℕ → ( 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
88 87 ad2antrl ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
89 88 imp ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
90 pfxfv ⊢ ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑋 ‘ ( 𝑖 + 1 ) ) )
91 25 70 89 90 syl3anc ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑋 ‘ ( 𝑖 + 1 ) ) )
92 91 eqcomd ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → ( 𝑋 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) )
93 80 92 preq12d ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } )
94 93 eleq1d ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) ) → ( { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
95 94 ralbidva ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
96 23 95 sylibd ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
97 96 impancom ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
98 97 imp ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
99 24 69 jca ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ) )
100 99 adantlr ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ) )
101 pfxlen ⊢ ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ) → ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = 𝑀 )
102 100 101 syl ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = 𝑀 )
103 102 oveq1d ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) = ( 𝑀 − 1 ) )
104 103 oveq2d ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) = ( 0 ..^ ( 𝑀 − 1 ) ) )
105 104 raleqdv ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
106 98 105 mpbird ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
107 24 69 101 syl2anc ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = 𝑀 )
108 84 eqcomd ⊢ ( 𝑀 ∈ ℕ → 𝑀 = ( ( 𝑀 − 1 ) + 1 ) )
109 108 ad2antrl ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → 𝑀 = ( ( 𝑀 − 1 ) + 1 ) )
110 107 109 eqtrd ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) )
111 110 adantlr ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) )
112 6 106 111 3jca ⊢ ( ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) → ( ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) ) )
113 112 ex ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) ) ) )
114 113 3adant3 ⊢ ( ( ( 𝑋 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑋 ‘ 𝑖 ) , ( 𝑋 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑋 ) , ( 𝑋 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) ) ) )
115 3 114 syl ⊢ ( 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) ) ) )
116 115 impcom ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) ) )
117 nnm1nn0 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
118 117 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝑀 − 1 ) ∈ ℕ0 )
119 1 2 iswwlksnx ⊢ ( ( 𝑀 − 1 ) ∈ ℕ0 → ( ( 𝑋 prefix 𝑀 ) ∈ ( ( 𝑀 − 1 ) WWalksN 𝐺 ) ↔ ( ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) ) ) )
120 118 119 syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( 𝑋 prefix 𝑀 ) ∈ ( ( 𝑀 − 1 ) WWalksN 𝐺 ) ↔ ( ( 𝑋 prefix 𝑀 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) − 1 ) ) { ( ( 𝑋 prefix 𝑀 ) ‘ 𝑖 ) , ( ( 𝑋 prefix 𝑀 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑋 prefix 𝑀 ) ) = ( ( 𝑀 − 1 ) + 1 ) ) ) )
121 116 120 mpbird ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝑋 prefix 𝑀 ) ∈ ( ( 𝑀 − 1 ) WWalksN 𝐺 ) )
122 121 ex ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑋 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑋 prefix 𝑀 ) ∈ ( ( 𝑀 − 1 ) WWalksN 𝐺 ) ) )