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

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 𝐺 ) )