Metamath Proof Explorer


Theorem clwwlkf

Description: Lemma 1 for clwwlkf1o : F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwwlkf1o.d 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
clwwlkf1o.f 𝐹 = ( 𝑡𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
Assertion clwwlkf ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 ⟶ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
2 clwwlkf1o.f 𝐹 = ( 𝑡𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
3 fveq2 ( 𝑤 = 𝑡 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑡 ) )
4 fveq1 ( 𝑤 = 𝑡 → ( 𝑤 ‘ 0 ) = ( 𝑡 ‘ 0 ) )
5 3 4 eqeq12d ( 𝑤 = 𝑡 → ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ↔ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) )
6 5 1 elrab2 ( 𝑡𝐷 ↔ ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) )
7 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8 iswwlksn ( 𝑁 ∈ ℕ0 → ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑡 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) )
9 7 8 syl ( 𝑁 ∈ ℕ → ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑡 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) )
10 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
11 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
12 10 11 iswwlks ( 𝑡 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
13 12 a1i ( 𝑁 ∈ ℕ → ( 𝑡 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
14 13 anbi1d ( 𝑁 ∈ ℕ → ( ( 𝑡 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ↔ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) )
15 9 14 bitrd ( 𝑁 ∈ ℕ → ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) )
16 simpll ( ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) )
17 peano2nn0 ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
18 7 17 syl ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ0 )
19 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
20 19 lep1d ( 𝑁 ∈ ℕ → 𝑁 ≤ ( 𝑁 + 1 ) )
21 elfz2nn0 ( 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ0𝑁 ≤ ( 𝑁 + 1 ) ) )
22 7 18 20 21 syl3anbrc ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
23 22 adantl ( ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
24 oveq2 ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 0 ... ( ♯ ‘ 𝑡 ) ) = ( 0 ... ( 𝑁 + 1 ) ) )
25 24 eleq2d ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ↔ 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
26 25 adantl ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ↔ 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
27 26 adantr ( ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ↔ 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
28 23 27 mpbird ( ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) )
29 16 28 jca ( ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) )
30 pfxlen ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 )
31 29 30 syl ( ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 )
32 31 ex ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) )
33 32 3ad2antl2 ( ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) )
34 33 impcom ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 )
35 34 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 )
36 pfxcl ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) )
37 36 3ad2ant2 ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) )
38 37 ad2antrl ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) )
39 38 ad2antrl ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) )
40 oveq1 ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑡 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
41 40 oveq2d ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) = ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) )
42 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
43 1cnd ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
44 42 43 pncand ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
45 44 oveq2d ( 𝑁 ∈ ℕ → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ 𝑁 ) )
46 41 45 sylan9eqr ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) = ( 0 ..^ 𝑁 ) )
47 46 raleqdv ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
48 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
49 peano2zm ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
50 48 49 syl ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℤ )
51 19 lem1d ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ≤ 𝑁 )
52 eluz2 ( 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) ↔ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − 1 ) ≤ 𝑁 ) )
53 50 48 51 52 syl3anbrc ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
54 fzoss2 ( 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
55 53 54 syl ( 𝑁 ∈ ℕ → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
56 55 adantr ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
57 ssralv ( ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
58 56 57 syl ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
59 simplr ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) )
60 22 adantr ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
61 25 adantl ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ↔ 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
62 60 61 mpbird ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) )
63 62 ad2antrr ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) )
64 55 sseld ( 𝑁 ∈ ℕ → ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) ) )
65 64 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) ) )
66 65 imp ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
67 pfxfv ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) = ( 𝑡𝑖 ) )
68 67 eqcomd ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑡𝑖 ) = ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) )
69 59 63 66 68 syl3anc ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑡𝑖 ) = ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) )
70 48 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) → 𝑁 ∈ ℤ )
71 elfzom1elp1fzo ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
72 70 71 sylan ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
73 pfxfv ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑡 ‘ ( 𝑖 + 1 ) ) )
74 73 eqcomd ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑡 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) )
75 59 63 72 74 syl3anc ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑡 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) )
76 69 75 preq12d ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } )
77 76 eleq1d ( ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
78 77 ralbidva ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
79 78 biimpd ( ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
80 79 ex ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
81 80 com23 ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
82 58 81 syld ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
83 47 82 sylbid ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
84 83 ex ( 𝑁 ∈ ℕ → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
85 84 com23 ( 𝑁 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
86 85 com14 ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
87 86 imp ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
88 87 3adant1 ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
89 88 imp ( ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
90 89 impcom ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
91 90 ad2antrl ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
92 oveq1 ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 → ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) = ( 𝑁 − 1 ) )
93 92 oveq2d ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 → ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
94 93 adantr ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
95 94 raleqdv ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
96 91 95 mpbird ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
97 simprl2 ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) )
98 20 ancli ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) )
99 48 peano2zd ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℤ )
100 fznn ( ( 𝑁 + 1 ) ∈ ℤ → ( 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) ) )
101 99 100 syl ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) ) )
102 98 101 mpbird ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
103 102 adantr ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
104 oveq2 ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 1 ... ( ♯ ‘ 𝑡 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
105 104 eleq2d ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
106 105 adantl ( ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
107 106 adantl ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
108 103 107 mpbird ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) )
109 97 108 jca ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) ) )
110 109 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) ) )
111 pfxfvlsw ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) ) → ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) = ( 𝑡 ‘ ( 𝑁 − 1 ) ) )
112 110 111 syl ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) = ( 𝑡 ‘ ( 𝑁 − 1 ) ) )
113 pfxfv0 ( ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑡 ) ) ) → ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) = ( 𝑡 ‘ 0 ) )
114 109 113 syl ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) = ( 𝑡 ‘ 0 ) )
115 114 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) = ( 𝑡 ‘ 0 ) )
116 112 115 preq12d ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } = { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ 0 ) } )
117 eqcom ( ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ↔ ( 𝑡 ‘ 0 ) = ( lastS ‘ 𝑡 ) )
118 117 biimpi ( ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) → ( 𝑡 ‘ 0 ) = ( lastS ‘ 𝑡 ) )
119 118 adantl ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( 𝑡 ‘ 0 ) = ( lastS ‘ 𝑡 ) )
120 lsw ( 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ ( ( ♯ ‘ 𝑡 ) − 1 ) ) )
121 120 3ad2ant2 ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ ( ( ♯ ‘ 𝑡 ) − 1 ) ) )
122 121 ad2antrl ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ ( ( ♯ ‘ 𝑡 ) − 1 ) ) )
123 122 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ ( ( ♯ ‘ 𝑡 ) − 1 ) ) )
124 40 adantl ( ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑡 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
125 124 44 sylan9eqr ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → ( ( ♯ ‘ 𝑡 ) − 1 ) = 𝑁 )
126 125 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( ( ♯ ‘ 𝑡 ) − 1 ) = 𝑁 )
127 126 fveq2d ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( 𝑡 ‘ ( ( ♯ ‘ 𝑡 ) − 1 ) ) = ( 𝑡𝑁 ) )
128 119 123 127 3eqtrd ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( 𝑡 ‘ 0 ) = ( 𝑡𝑁 ) )
129 128 preq2d ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ 0 ) } = { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } )
130 40 44 sylan9eq ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ 𝑡 ) − 1 ) = 𝑁 )
131 130 oveq2d ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) = ( 0 ..^ 𝑁 ) )
132 131 raleqdv ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
133 fzo0end ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
134 fveq2 ( 𝑖 = ( 𝑁 − 1 ) → ( 𝑡𝑖 ) = ( 𝑡 ‘ ( 𝑁 − 1 ) ) )
135 fvoveq1 ( 𝑖 = ( 𝑁 − 1 ) → ( 𝑡 ‘ ( 𝑖 + 1 ) ) = ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
136 134 135 preq12d ( 𝑖 = ( 𝑁 − 1 ) → { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } )
137 136 eleq1d ( 𝑖 = ( 𝑁 − 1 ) → ( { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
138 137 rspcva ( ( ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
139 133 138 sylan ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
140 42 43 npcand ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
141 140 fveq2d ( 𝑁 ∈ ℕ → ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝑡𝑁 ) )
142 141 preq2d ( 𝑁 ∈ ℕ → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } = { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } )
143 142 eleq1d ( 𝑁 ∈ ℕ → ( { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
144 143 biimpd ( 𝑁 ∈ ℕ → ( { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
145 144 adantr ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
146 139 145 mpd ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) )
147 146 ex ( 𝑁 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
148 147 adantl ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
149 132 148 sylbid ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
150 149 ex ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
151 150 com3r ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
152 151 3ad2ant3 ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
153 152 imp ( ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) ) )
154 153 impcom ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) )
155 154 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡𝑁 ) } ∈ ( Edg ‘ 𝐺 ) )
156 129 155 eqeltrd ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → { ( 𝑡 ‘ ( 𝑁 − 1 ) ) , ( 𝑡 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
157 116 156 eqeltrd ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
158 157 adantl ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
159 39 96 158 3jca ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
160 simpl ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 )
161 159 160 jca ( ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ∧ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) )
162 35 161 mpancom ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) → ( ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) )
163 162 exp31 ( 𝑁 ∈ ℕ → ( ( ( 𝑡 ≠ ∅ ∧ 𝑡 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑡 ) − 1 ) ) { ( 𝑡𝑖 ) , ( 𝑡 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 1 ) ) → ( ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) → ( ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) ) ) )
164 15 163 sylbid ( 𝑁 ∈ ℕ → ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) → ( ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) ) ) )
165 164 imp32 ( ( 𝑁 ∈ ℕ ∧ ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) )
166 10 11 isclwwlknx ( 𝑁 ∈ ℕ → ( ( 𝑡 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) ) )
167 166 adantr ( ( 𝑁 ∈ ℕ ∧ ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( ( 𝑡 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( 𝑡 prefix 𝑁 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) − 1 ) ) { ( ( 𝑡 prefix 𝑁 ) ‘ 𝑖 ) , ( ( 𝑡 prefix 𝑁 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑡 prefix 𝑁 ) ) , ( ( 𝑡 prefix 𝑁 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑡 prefix 𝑁 ) ) = 𝑁 ) ) )
168 165 167 mpbird ( ( 𝑁 ∈ ℕ ∧ ( 𝑡 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑡 ) = ( 𝑡 ‘ 0 ) ) ) → ( 𝑡 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
169 6 168 sylan2b ( ( 𝑁 ∈ ℕ ∧ 𝑡𝐷 ) → ( 𝑡 prefix 𝑁 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
170 169 2 fmptd ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 ⟶ ( 𝑁 ClWWalksN 𝐺 ) )