Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  clwwlkfOLD Structured version   Visualization version   GIF version

Theorem clwwlkfOLD 27438
 Description: Obsolete version of clwwlkf 27443 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 26-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
clwwlkf1o.d 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
clwwlkf1oOLD.f 𝐹 = (𝑡𝐷 ↦ (𝑡 substr ⟨0, 𝑁⟩))
Assertion
Ref Expression
clwwlkfOLD (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
Distinct variable groups:   𝑤,𝐺   𝑤,𝑁   𝑡,𝐷   𝑡,𝐺,𝑤   𝑡,𝑁
Allowed substitution hints:   𝐷(𝑤)   𝐹(𝑤,𝑡)

Proof of Theorem clwwlkfOLD
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6446 . . . . 5 (𝑤 = 𝑡 → (lastS‘𝑤) = (lastS‘𝑡))
2 fveq1 6445 . . . . 5 (𝑤 = 𝑡 → (𝑤‘0) = (𝑡‘0))
31, 2eqeq12d 2792 . . . 4 (𝑤 = 𝑡 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑡) = (𝑡‘0)))
4 clwwlkf1o.d . . . 4 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
53, 4elrab2 3575 . . 3 (𝑡𝐷 ↔ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0)))
6 nnnn0 11650 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
7 iswwlksn 27187 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1))))
86, 7syl 17 . . . . . . 7 (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1))))
9 eqid 2777 . . . . . . . . . 10 (Vtx‘𝐺) = (Vtx‘𝐺)
10 eqid 2777 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
119, 10iswwlks 27185 . . . . . . . . 9 (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
1211a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
1312anbi1d 623 . . . . . . 7 (𝑁 ∈ ℕ → ((𝑡 ∈ (WWalks‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))))
148, 13bitrd 271 . . . . . 6 (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))))
15 simpll 757 . . . . . . . . . . . . . 14 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑡 ∈ Word (Vtx‘𝐺))
16 peano2nn0 11684 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
176, 16syl 17 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
18 nnre 11382 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
1918lep1d 11309 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
20 elfz2nn0 12749 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (0...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ0𝑁 ≤ (𝑁 + 1)))
216, 17, 19, 20syl3anbrc 1400 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ (0...(𝑁 + 1)))
2221adantl 475 . . . . . . . . . . . . . . 15 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(𝑁 + 1)))
23 oveq2 6930 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑡) = (𝑁 + 1) → (0...(♯‘𝑡)) = (0...(𝑁 + 1)))
2423eleq2d 2844 . . . . . . . . . . . . . . . . 17 ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
2524adantl 475 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
2625adantr 474 . . . . . . . . . . . . . . 15 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
2722, 26mpbird 249 . . . . . . . . . . . . . 14 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(♯‘𝑡)))
2815, 27jca 507 . . . . . . . . . . . . 13 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡))))
29 swrd0lenOLD 13738 . . . . . . . . . . . . 13 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡))) → (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
3028, 29syl 17 . . . . . . . . . . . 12 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
3130ex 403 . . . . . . . . . . 11 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
32313ad2antl2 1194 . . . . . . . . . 10 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
3332impcom 398 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
3433adantr 474 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
35 swrdcl 13735 . . . . . . . . . . . . 13 (𝑡 ∈ Word (Vtx‘𝐺) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
36353ad2ant2 1125 . . . . . . . . . . . 12 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
3736ad2antrl 718 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
3837ad2antrl 718 . . . . . . . . . 10 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
39 oveq1 6929 . . . . . . . . . . . . . . . . . . . . . . 23 ((♯‘𝑡) = (𝑁 + 1) → ((♯‘𝑡) − 1) = ((𝑁 + 1) − 1))
4039oveq2d 6938 . . . . . . . . . . . . . . . . . . . . . 22 ((♯‘𝑡) = (𝑁 + 1) → (0..^((♯‘𝑡) − 1)) = (0..^((𝑁 + 1) − 1)))
41 nncn 11383 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
42 1cnd 10371 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 1 ∈ ℂ)
4341, 42pncand 10735 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
4443oveq2d 6938 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = (0..^𝑁))
4540, 44sylan9eqr 2835 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (0..^((♯‘𝑡) − 1)) = (0..^𝑁))
4645raleqdv 3339 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
47 nnz 11751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
48 peano2zm 11772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
4947, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
5018lem1d 11311 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (𝑁 − 1) ≤ 𝑁)
51 eluz2 11998 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘(𝑁 − 1)) ↔ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ≤ 𝑁))
5249, 47, 50, 51syl3anbrc 1400 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
53 fzoss2 12815 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
5554adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
56 ssralv 3884 . . . . . . . . . . . . . . . . . . . . . 22 ((0..^(𝑁 − 1)) ⊆ (0..^𝑁) → (∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
58 simplr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
5921adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(𝑁 + 1)))
6024adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
6159, 60mpbird 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(♯‘𝑡)))
6261ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(♯‘𝑡)))
6354sseld 3819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℕ → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
6463ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
6564imp 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66 swrd0fvOLD 13758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖) = (𝑡𝑖))
6766eqcomd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑡𝑖) = ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖))
6858, 62, 65, 67syl3anc 1439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡𝑖) = ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖))
6947ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → 𝑁 ∈ ℤ)
70 elfzom1elp1fzo 12854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
7169, 70sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
72 swrd0fvOLD 13758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)) = (𝑡‘(𝑖 + 1)))
7372eqcomd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)))
7458, 62, 71, 73syl3anc 1439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)))
7568, 74preq12d 4507 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑡𝑖), (𝑡‘(𝑖 + 1))} = {((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))})
7675eleq1d 2843 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7776ralbidva 3166 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7877biimpd 221 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7978ex 403 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8079com23 86 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8157, 80syld 47 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8246, 81sylbid 232 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8382ex 403 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → ((♯‘𝑡) = (𝑁 + 1) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
8483com23 86 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((♯‘𝑡) = (𝑁 + 1) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
8584com14 96 . . . . . . . . . . . . . . . 16 (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
8685imp 397 . . . . . . . . . . . . . . 15 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
87863adant1 1121 . . . . . . . . . . . . . 14 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8887imp 397 . . . . . . . . . . . . 13 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
8988impcom 398 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
9089ad2antrl 718 . . . . . . . . . . 11 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
91 oveq1 6929 . . . . . . . . . . . . . 14 ((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 → ((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1) = (𝑁 − 1))
9291oveq2d 6938 . . . . . . . . . . . . 13 ((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 → (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
9392adantr 474 . . . . . . . . . . . 12 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
9493raleqdv 3339 . . . . . . . . . . 11 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
9590, 94mpbird 249 . . . . . . . . . 10 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
96 simprl2 1240 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
9719ancli 544 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))
9847peano2zd 11837 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℤ)
99 fznn 12726 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 + 1) ∈ ℤ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
10098, 99syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
10197, 100mpbird 249 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1)))
102101adantr 474 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(𝑁 + 1)))
103 oveq2 6930 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝑡) = (𝑁 + 1) → (1...(♯‘𝑡)) = (1...(𝑁 + 1)))
104103eleq2d 2844 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (1...(♯‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
105104adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (1...(♯‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
106105adantl 475 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (𝑁 ∈ (1...(♯‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
107102, 106mpbird 249 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(♯‘𝑡)))
10896, 107jca 507 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))))
109108adantr 474 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))))
110 swrd0fvlswOLD 13762 . . . . . . . . . . . . . 14 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))) → (lastS‘(𝑡 substr ⟨0, 𝑁⟩)) = (𝑡‘(𝑁 − 1)))
111109, 110syl 17 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (lastS‘(𝑡 substr ⟨0, 𝑁⟩)) = (𝑡‘(𝑁 − 1)))
112 swrd0fv0OLD 13759 . . . . . . . . . . . . . . 15 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
113108, 112syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
114113adantr 474 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
115111, 114preq12d 4507 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘0)})
116 eqcom 2784 . . . . . . . . . . . . . . . . 17 ((lastS‘𝑡) = (𝑡‘0) ↔ (𝑡‘0) = (lastS‘𝑡))
117116biimpi 208 . . . . . . . . . . . . . . . 16 ((lastS‘𝑡) = (𝑡‘0) → (𝑡‘0) = (lastS‘𝑡))
118117adantl 475 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (lastS‘𝑡))
119 lsw 13654 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ Word (Vtx‘𝐺) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
1201193ad2ant2 1125 . . . . . . . . . . . . . . . . 17 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
121120ad2antrl 718 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
122121adantr 474 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
12339adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → ((♯‘𝑡) − 1) = ((𝑁 + 1) − 1))
124123, 43sylan9eqr 2835 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → ((♯‘𝑡) − 1) = 𝑁)
125124adantr 474 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → ((♯‘𝑡) − 1) = 𝑁)
126125fveq2d 6450 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡‘((♯‘𝑡) − 1)) = (𝑡𝑁))
127118, 122, 1263eqtrd 2817 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (𝑡𝑁))
128127preq2d 4506 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡𝑁)})
12939, 43sylan9eq 2833 . . . . . . . . . . . . . . . . . . . . . 22 (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((♯‘𝑡) − 1) = 𝑁)
130129oveq2d 6938 . . . . . . . . . . . . . . . . . . . . 21 (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (0..^((♯‘𝑡) − 1)) = (0..^𝑁))
131130raleqdv 3339 . . . . . . . . . . . . . . . . . . . 20 (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132 fzo0end 12879 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
133 fveq2 6446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = (𝑁 − 1) → (𝑡𝑖) = (𝑡‘(𝑁 − 1)))
134 fvoveq1 6945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = (𝑁 − 1) → (𝑡‘(𝑖 + 1)) = (𝑡‘((𝑁 − 1) + 1)))
135133, 134preq12d 4507 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = (𝑁 − 1) → {(𝑡𝑖), (𝑡‘(𝑖 + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))})
136135eleq1d 2843 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = (𝑁 − 1) → ({(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
137136rspcva 3508 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 − 1) ∈ (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
138132, 137sylan 575 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
13941, 42npcand 10738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
140139fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → (𝑡‘((𝑁 − 1) + 1)) = (𝑡𝑁))
141140preq2d 4506 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡𝑁)})
142141eleq1d 2843 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
143142biimpd 221 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
144143adantr 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
145138, 144mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))
146145ex 403 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
147146adantl 475 . . . . . . . . . . . . . . . . . . . 20 (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
148131, 147sylbid 232 . . . . . . . . . . . . . . . . . . 19 (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
149148ex 403 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))))
150149com3r 87 . . . . . . . . . . . . . . . . 17 (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))))
1511503ad2ant3 1126 . . . . . . . . . . . . . . . 16 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))))
152151imp 397 . . . . . . . . . . . . . . 15 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
153152impcom 398 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))
154153adantr 474 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))
155128, 154eqeltrd 2858 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} ∈ (Edg‘𝐺))
156115, 155eqeltrd 2858 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
157156adantl 475 . . . . . . . . . 10 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
15838, 95, 1573jca 1119 . . . . . . . . 9 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → ((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))
159 simpl 476 . . . . . . . . 9 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
160158, 159jca 507 . . . . . . . 8 (((♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
16134, 160mpancom 678 . . . . . . 7 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
162161exp31 412 . . . . . 6 (𝑁 ∈ ℕ → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → ((lastS‘𝑡) = (𝑡‘0) → (((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))))
16314, 162sylbid 232 . . . . 5 (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) → ((lastS‘𝑡) = (𝑡‘0) → (((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))))
164163imp32 411 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0))) → (((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
1659, 10isclwwlknx 27425 . . . . 5 (𝑁 ∈ ℕ → ((𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ (((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)))
166165adantr 474 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0))) → ((𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ (((𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)))
167164, 166mpbird 249 . . 3 ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
1685, 167sylan2b 587 . 2 ((𝑁 ∈ ℕ ∧ 𝑡𝐷) → (𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
169 clwwlkf1oOLD.f . 2 𝐹 = (𝑡𝐷 ↦ (𝑡 substr ⟨0, 𝑁⟩))
170168, 169fmptd 6648 1 (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2106   ≠ wne 2968  ∀wral 3089  {crab 3093   ⊆ wss 3791  ∅c0 4140  {cpr 4399  ⟨cop 4403   class class class wbr 4886   ↦ cmpt 4965  ⟶wf 6131  ‘cfv 6135  (class class class)co 6922  0cc0 10272  1c1 10273   + caddc 10275   ≤ cle 10412   − cmin 10606  ℕcn 11374  ℕ0cn0 11642  ℤcz 11728  ℤ≥cuz 11992  ...cfz 12643  ..^cfzo 12784  ♯chash 13435  Word cword 13599  lastSclsw 13652   substr csubstr 13730  Vtxcvtx 26344  Edgcedg 26395  WWalkscwwlks 27174   WWalksN cwwlksn 27175   ClWWalksN cclwwlkn 27413 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785  df-hash 13436  df-word 13600  df-lsw 13653  df-substr 13731  df-wwlks 27179  df-wwlksn 27180  df-clwwlk 27362  df-clwwlkn 27414 This theorem is referenced by:  clwwlkf1OLD  27440  clwwlkfoOLD  27441
 Copyright terms: Public domain W3C validator