Metamath Proof Explorer

Theorem clwwlkinwwlk

Description: If the initial vertex of a walk occurs another time in the walk, the walk starts with a closed walk. Since the walk is expressed as a word over vertices, the closed walk can be expressed as a subword of this word. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 23-Jan-2022) (Revised by AV, 30-Oct-2022)

Ref Expression
Assertion clwwlkinwwlk ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑊 ∈ ( 𝑀 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 wwlknp ⊢ ( 𝑊 ∈ ( 𝑀 WWalksN 𝐺 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
4 pfxcl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) )
5 4 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) → ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) )
6 5 adantr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) )
7 simpll ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
8 simprl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
9 eluz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ≤ 𝑀 ) )
10 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
11 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
12 id ⊢ ( 𝑁 ≤ 𝑀 → 𝑁 ≤ 𝑀 )
13 10 11 12 3anim123i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ≤ 𝑀 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ≤ 𝑀 ) )
14 9 13 sylbi ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ≤ 𝑀 ) )
15 letrp1 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ≤ 𝑀 ) → 𝑁 ≤ ( 𝑀 + 1 ) )
16 14 15 syl ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ ( 𝑀 + 1 ) )
17 16 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ ( 𝑀 + 1 ) )
18 17 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ≤ ( 𝑀 + 1 ) )
19 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ↔ 𝑁 ≤ ( 𝑀 + 1 ) ) )
20 19 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ↔ 𝑁 ≤ ( 𝑀 + 1 ) ) )
21 18 20 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ≤ ( ♯ ‘ 𝑊 ) )
22 pfxn0 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix 𝑁 ) ≠ ∅ )
23 7 8 21 22 syl3anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑊 prefix 𝑁 ) ≠ ∅ )
24 6 23 jca ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 prefix 𝑁 ) ≠ ∅ ) )
25 24 3adantl3 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 prefix 𝑁 ) ≠ ∅ ) )
26 25 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 prefix 𝑁 ) ≠ ∅ ) )
27 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
28 1nn0 ⊢ 1 ∈ ℕ0
29 eluzmn ⊢ ( ( 𝑁 ∈ ℤ ∧ 1 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
30 27 28 29 sylancl ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
31 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
32 30 31 syl ⊢ ( 𝑁 ∈ ℕ → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
33 32 sselda ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
34 fzoss2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑀 ) )
35 33 34 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑀 ) )
36 35 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑀 ) )
37 ssralv ⊢ ( ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑀 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
38 36 37 syl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
39 38 3exp ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
40 39 com34 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
41 40 3imp1 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
42 41 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
43 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
44 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
45 43 44 sylib ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
46 eluzfz ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 0 ... 𝑀 ) )
47 45 46 sylan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 0 ... 𝑀 ) )
48 fzelp1 ⊢ ( 𝑁 ∈ ( 0 ... 𝑀 ) → 𝑁 ∈ ( 0 ... ( 𝑀 + 1 ) ) )
49 47 48 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 0 ... ( 𝑀 + 1 ) ) )
50 49 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( 0 ... ( 𝑀 + 1 ) ) )
51 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( 𝑀 + 1 ) ) )
52 51 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ... ( 𝑀 + 1 ) ) ) )
53 52 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ... ( 𝑀 + 1 ) ) ) )
54 50 53 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
55 pfxlen ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) = 𝑁 )
56 7 54 55 syl2anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) = 𝑁 )
57 56 oveq1d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) = ( 𝑁 − 1 ) )
58 57 oveq2d ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
59 58 raleqdv ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
60 7 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
61 54 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
62 30 ad2antrl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
63 fzoss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
64 62 63 syl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
65 64 sselda ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
66 pfxfv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
67 60 61 65 66 syl3anc ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
68 27 ad2antrl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℤ )
69 elfzom1elp1fzo ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
70 68 69 sylan ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
71 pfxfv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
72 60 61 70 71 syl3anc ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
73 67 72 preq12d ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } )
74 73 eleq1d ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
75 74 ralbidva ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
76 59 75 bitrd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
77 76 3adantl3 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
78 77 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
79 42 78 mpbird ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
80 elfz1uz ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 1 ... 𝑀 ) )
81 fzelp1 ⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑁 ∈ ( 1 ... ( 𝑀 + 1 ) ) )
82 80 81 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 1 ... ( 𝑀 + 1 ) ) )
83 82 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( 1 ... ( 𝑀 + 1 ) ) )
84 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( 𝑀 + 1 ) ) )
85 84 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑀 + 1 ) ) ) )
86 85 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑀 + 1 ) ) ) )
87 83 86 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
88 pfxfvlsw ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
89 pfxfv0 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
90 88 89 preq12d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } )
91 7 87 90 syl2anc ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } )
92 91 3adantl3 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } )
93 92 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } )
94 fz1fzo0m1 ⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑀 ) )
95 80 94 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑀 ) )
96 95 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑀 ) )
97 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 = ( 𝑁 − 1 ) ) → 𝑖 = ( 𝑁 − 1 ) )
98 97 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 = ( 𝑁 − 1 ) ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
99 oveq1 ⊢ ( 𝑖 = ( 𝑁 − 1 ) → ( 𝑖 + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
100 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
101 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
102 100 101 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
103 99 102 sylan9eqr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 = ( 𝑁 − 1 ) ) → ( 𝑖 + 1 ) = 𝑁 )
104 103 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 = ( 𝑁 − 1 ) ) → ( 𝑊 ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ 𝑁 ) )
105 98 104 preq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 = ( 𝑁 − 1 ) ) → { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } )
106 105 eleq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 = ( 𝑁 − 1 ) ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
107 106 ex ⊢ ( 𝑁 ∈ ℕ → ( 𝑖 = ( 𝑁 − 1 ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
108 107 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑖 = ( 𝑁 − 1 ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
109 108 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑖 = ( 𝑁 − 1 ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
110 109 imp ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ 𝑖 = ( 𝑁 − 1 ) ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
111 96 110 rspcdv ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
112 111 3exp ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
113 112 com34 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
114 113 3imp1 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) )
115 114 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) )
116 preq2 ⊢ ( ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } )
117 116 eleq1d ⊢ ( ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) → ( { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
118 117 adantl ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
119 115 118 mpbid ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
120 93 119 eqeltrd ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
121 26 79 120 3jca ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( ( ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 prefix 𝑁 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
122 121 exp31 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) → ( ( ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 prefix 𝑁 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
123 122 3imp21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( ( ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 prefix 𝑁 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
124 1 2 isclwwlk ⊢ ( ( 𝑊 prefix 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( ( 𝑊 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 prefix 𝑁 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑊 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑊 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑊 prefix 𝑁 ) ) , ( ( 𝑊 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
125 123 124 sylibr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 prefix 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) )
126 47 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( 0 ... 𝑀 ) )
127 126 48 syl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( 0 ... ( 𝑀 + 1 ) ) )
128 127 53 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
129 7 128 jca ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
130 129 ex ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
131 130 3adant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
132 131 impcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
133 132 3adant3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
134 133 55 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) = 𝑁 )
135 isclwwlkn ⊢ ( ( 𝑊 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( 𝑊 prefix 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix 𝑁 ) ) = 𝑁 ) )
136 125 134 135 sylanbrc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑀 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
137 3 136 syl3an2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑊 ∈ ( 𝑀 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )