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

Theorem clwwlksf 26908
Description: Lemma 1 for clwwlksbij 26913: F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 26-Apr-2021.)
Hypotheses
Ref Expression
clwwlksbij.d 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}
clwwlksbij.f 𝐹 = (𝑡𝐷 ↦ (𝑡 substr ⟨0, 𝑁⟩))
Assertion
Ref Expression
clwwlksf (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
Distinct variable groups:   𝑤,𝐺   𝑤,𝑁   𝑡,𝐷   𝑡,𝐺,𝑤   𝑡,𝑁
Allowed substitution hints:   𝐷(𝑤)   𝐹(𝑤,𝑡)

Proof of Theorem clwwlksf
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6189 . . . . 5 (𝑤 = 𝑡 → ( lastS ‘𝑤) = ( lastS ‘𝑡))
2 fveq1 6188 . . . . 5 (𝑤 = 𝑡 → (𝑤‘0) = (𝑡‘0))
31, 2eqeq12d 2636 . . . 4 (𝑤 = 𝑡 → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘𝑡) = (𝑡‘0)))
4 clwwlksbij.d . . . 4 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}
53, 4elrab2 3364 . . 3 (𝑡𝐷 ↔ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0)))
6 nnnn0 11296 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
7 iswwlksn 26724 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1))))
86, 7syl 17 . . . . . . 7 (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1))))
9 eqid 2621 . . . . . . . . . 10 (Vtx‘𝐺) = (Vtx‘𝐺)
10 eqid 2621 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
119, 10iswwlks 26722 . . . . . . . . 9 (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
1211a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
1312anbi1d 741 . . . . . . 7 (𝑁 ∈ ℕ → ((𝑡 ∈ (WWalks‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))))
148, 13bitrd 268 . . . . . 6 (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))))
15 simpll 790 . . . . . . . . . . . . . 14 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑡 ∈ Word (Vtx‘𝐺))
16 peano2nn0 11330 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
176, 16syl 17 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
18 nnre 11024 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
1918lep1d 10952 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
20 elfz2nn0 12427 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (0...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ0𝑁 ≤ (𝑁 + 1)))
216, 17, 19, 20syl3anbrc 1245 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ (0...(𝑁 + 1)))
2221adantl 482 . . . . . . . . . . . . . . 15 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(𝑁 + 1)))
23 oveq2 6655 . . . . . . . . . . . . . . . . . 18 ((#‘𝑡) = (𝑁 + 1) → (0...(#‘𝑡)) = (0...(𝑁 + 1)))
2423eleq2d 2686 . . . . . . . . . . . . . . . . 17 ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
2524adantl 482 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
2625adantr 481 . . . . . . . . . . . . . . 15 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
2722, 26mpbird 247 . . . . . . . . . . . . . 14 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(#‘𝑡)))
2815, 27jca 554 . . . . . . . . . . . . 13 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡))))
29 swrd0len 13416 . . . . . . . . . . . . 13 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡))) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
3028, 29syl 17 . . . . . . . . . . . 12 (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
3130ex 450 . . . . . . . . . . 11 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
32313ad2antl2 1223 . . . . . . . . . 10 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
3332impcom 446 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
3433adantr 481 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
35 swrdcl 13413 . . . . . . . . . . . . 13 (𝑡 ∈ Word (Vtx‘𝐺) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
36353ad2ant2 1082 . . . . . . . . . . . 12 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
3736ad2antrl 764 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
3837ad2antrl 764 . . . . . . . . . 10 (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
39 oveq1 6654 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑡) = (𝑁 + 1) → ((#‘𝑡) − 1) = ((𝑁 + 1) − 1))
4039oveq2d 6663 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝑡) = (𝑁 + 1) → (0..^((#‘𝑡) − 1)) = (0..^((𝑁 + 1) − 1)))
41 nncn 11025 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
42 1cnd 10053 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 1 ∈ ℂ)
4341, 42pncand 10390 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
4443oveq2d 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = (0..^𝑁))
4540, 44sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (0..^((#‘𝑡) − 1)) = (0..^𝑁))
4645raleqdv 3142 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
47 nnz 11396 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
48 peano2zm 11417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
4947, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
5018lem1d 10954 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (𝑁 − 1) ≤ 𝑁)
51 eluz2 11690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘(𝑁 − 1)) ↔ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ≤ 𝑁))
5249, 47, 50, 51syl3anbrc 1245 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
53 fzoss2 12492 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
5554adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
56 ssralv 3664 . . . . . . . . . . . . . . . . . . . . . 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 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
5921adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(𝑁 + 1)))
6024adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
6159, 60mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(#‘𝑡)))
6261ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(#‘𝑡)))
6354sseld 3600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℕ → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
6463ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
6564imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66 swrd0fv 13433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖) = (𝑡𝑖))
6766eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑡𝑖) = ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖))
6858, 62, 65, 67syl3anc 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡𝑖) = ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖))
6947ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → 𝑁 ∈ ℤ)
70 elfzom1elp1fzo 12530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
7169, 70sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
72 swrd0fv 13433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)) = (𝑡‘(𝑖 + 1)))
7372eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)))
7458, 62, 71, 73syl3anc 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)))
7568, 74preq12d 4274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑡𝑖), (𝑡‘(𝑖 + 1))} = {((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))})
7675eleq1d 2685 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7776ralbidva 2984 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7877biimpd 219 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7978ex 450 . . . . . . . . . . . . . . . . . . . . . 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 230 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8382ex 450 . . . . . . . . . . . . . . . . . 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 445 . . . . . . . . . . . . . . 15 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
87863adant1 1078 . . . . . . . . . . . . . 14 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8887imp 445 . . . . . . . . . . . . 13 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
8988impcom 446 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
9089ad2antrl 764 . . . . . . . . . . 11 (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
91 oveq1 6654 . . . . . . . . . . . . . 14 ((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 → ((#‘(𝑡 substr ⟨0, 𝑁⟩)) − 1) = (𝑁 − 1))
9291oveq2d 6663 . . . . . . . . . . . . 13 ((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 → (0..^((#‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
9392adantr 481 . . . . . . . . . . . 12 (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (0..^((#‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
9493raleqdv 3142 . . . . . . . . . . 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 247 . . . . . . . . . 10 (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^((#‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
96 simprl2 1106 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
9719ancli 574 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))
9847peano2zd 11482 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℤ)
99 fznn 12405 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 + 1) ∈ ℤ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
10098, 99syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
10197, 100mpbird 247 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1)))
102101adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(𝑁 + 1)))
103 oveq2 6655 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝑡) = (𝑁 + 1) → (1...(#‘𝑡)) = (1...(𝑁 + 1)))
104103eleq2d 2686 . . . . . . . . . . . . . . . . . . 19 ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
105104adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
106105adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
107102, 106mpbird 247 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(#‘𝑡)))
10896, 107jca 554 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))))
109108adantr 481 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))))
110 swrd0fvlsw 13437 . . . . . . . . . . . . . 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 swrd0fv0 13434 . . . . . . . . . . . . . . 15 ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
113108, 112syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
114113adantr 481 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
115111, 114preq12d 4274 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘0)})
116 eqcom 2628 . . . . . . . . . . . . . . . . 17 (( lastS ‘𝑡) = (𝑡‘0) ↔ (𝑡‘0) = ( lastS ‘𝑡))
117116biimpi 206 . . . . . . . . . . . . . . . 16 (( lastS ‘𝑡) = (𝑡‘0) → (𝑡‘0) = ( lastS ‘𝑡))
118117adantl 482 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = ( lastS ‘𝑡))
119 lsw 13346 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
1201193ad2ant2 1082 . . . . . . . . . . . . . . . . 17 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
121120ad2antrl 764 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
122121adantr 481 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
12339adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → ((#‘𝑡) − 1) = ((𝑁 + 1) − 1))
124123, 43sylan9eqr 2677 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ((#‘𝑡) − 1) = 𝑁)
125124adantr 481 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((#‘𝑡) − 1) = 𝑁)
126125fveq2d 6193 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘((#‘𝑡) − 1)) = (𝑡𝑁))
127118, 122, 1263eqtrd 2659 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (𝑡𝑁))
128127preq2d 4273 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡𝑁)})
12939, 43sylan9eq 2675 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((#‘𝑡) − 1) = 𝑁)
130129oveq2d 6663 . . . . . . . . . . . . . . . . . . . . 21 (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (0..^((#‘𝑡) − 1)) = (0..^𝑁))
131130raleqdv 3142 . . . . . . . . . . . . . . . . . . . 20 (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132 fzo0end 12556 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
133 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = (𝑁 − 1) → (𝑡𝑖) = (𝑡‘(𝑁 − 1)))
134 oveq1 6654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
135134fveq2d 6193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = (𝑁 − 1) → (𝑡‘(𝑖 + 1)) = (𝑡‘((𝑁 − 1) + 1)))
136133, 135preq12d 4274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = (𝑁 − 1) → {(𝑡𝑖), (𝑡‘(𝑖 + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))})
137136eleq1d 2685 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = (𝑁 − 1) → ({(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
138137rspcva 3305 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 − 1) ∈ (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
139132, 138sylan 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
14041, 42npcand 10393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
141140fveq2d 6193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → (𝑡‘((𝑁 − 1) + 1)) = (𝑡𝑁))
142141preq2d 4273 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡𝑁)})
143142eleq1d 2685 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
144143biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
145144adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
146139, 145mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))
147146ex 450 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
148147adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
149131, 148sylbid 230 . . . . . . . . . . . . . . . . . . 19 (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
150149ex 450 . . . . . . . . . . . . . . . . . 18 ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))))
151150com3r 87 . . . . . . . . . . . . . . . . 17 (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))))
1521513ad2ant3 1083 . . . . . . . . . . . . . . . 16 ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))))
153152imp 445 . . . . . . . . . . . . . . 15 (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺)))
154153impcom 446 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))
155154adantr 481 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡𝑁)} ∈ (Edg‘𝐺))
156128, 155eqeltrd 2700 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} ∈ (Edg‘𝐺))
157115, 156eqeltrd 2700 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
158157adantl 482 . . . . . . . . . 10 (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → {( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
15938, 95, 1583jca 1241 . . . . . . . . 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‘𝐺)))
160 simpl 473 . . . . . . . . 9 (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
161159, 160jca 554 . . . . . . . 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, 𝑁⟩)) = 𝑁))
16234, 161mpancom 703 . . . . . . 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, 𝑁⟩)) = 𝑁))
163162exp31 630 . . . . . 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, 𝑁⟩)) = 𝑁))))
16414, 163sylbid 230 . . . . 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, 𝑁⟩)) = 𝑁))))
165164imp32 449 . . . 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, 𝑁⟩)) = 𝑁))
1669, 10isclwwlksnx 26883 . . . . 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, 𝑁⟩)) = 𝑁)))
167166adantr 481 . . . 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, 𝑁⟩)) = 𝑁)))
168165, 167mpbird 247 . . 3 ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
1695, 168sylan2b 492 . 2 ((𝑁 ∈ ℕ ∧ 𝑡𝐷) → (𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
170 clwwlksbij.f . 2 𝐹 = (𝑡𝐷 ↦ (𝑡 substr ⟨0, 𝑁⟩))
171169, 170fmptd 6383 1 (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wcel 1989  wne 2793  wral 2911  {crab 2915  wss 3572  c0 3913  {cpr 4177  cop 4181   class class class wbr 4651  cmpt 4727  wf 5882  cfv 5886  (class class class)co 6647  0cc0 9933  1c1 9934   + caddc 9936  cle 10072  cmin 10263  cn 11017  0cn0 11289  cz 11374  cuz 11684  ...cfz 12323  ..^cfzo 12461  #chash 13112  Word cword 13286   lastS clsw 13287   substr csubstr 13290  Vtxcvtx 25868  Edgcedg 25933  WWalkscwwlks 26711   WWalksN cwwlksn 26712   ClWWalksN cclwwlksn 26870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-oadd 7561  df-er 7739  df-map 7856  df-pm 7857  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-card 8762  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-nn 11018  df-n0 11290  df-z 11375  df-uz 11685  df-fz 12324  df-fzo 12462  df-hash 13113  df-word 13294  df-lsw 13295  df-substr 13298  df-wwlks 26716  df-wwlksn 26717  df-clwwlks 26871  df-clwwlksn 26872
This theorem is referenced by:  clwwlksf1  26910  clwwlksfo  26911
  Copyright terms: Public domain W3C validator