clwwlksf - Metamath Proof Explorer

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

Theorem clwwlksf 26915

Description: Lemma 1 for clwwlksbij 26920: 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.

Step	Hyp	Ref	Expression
1		fveq2 6191	. . . . 5 ⊢ (𝑤 = 𝑡 → ( lastS ‘𝑤) = ( lastS ‘𝑡))
2		fveq1 6190	. . . . 5 ⊢ (𝑤 = 𝑡 → (𝑤‘0) = (𝑡‘0))
3	1, 2	eqeq12d 2637	. . . 4 ⊢ (𝑤 = 𝑡 → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘𝑡) = (𝑡‘0)))
4		clwwlksbij.d	. . . 4 ⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}
5	3, 4	elrab2 3366	. . 3 ⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0)))
6		nnnn0 11299	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
7		iswwlksn 26730	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1))))
8	6, 7	syl 17	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1))))
9		eqid 2622	. . . . . . . . . 10 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
10		eqid 2622	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
11	9, 10	iswwlks 26728	. . . . . . . . 9 ⊢ (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
12	11	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
13	12	anbi1d 741	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑡 ∈ (WWalks‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))))
14	8, 13	bitrd 268	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))))
15		simpll 790	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑡 ∈ Word (Vtx‘𝐺))
16		peano2nn0 11333	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
17	6, 16	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ₀)
18		nnre 11027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
19	18	lep1d 10955	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
20		elfz2nn0 12431	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (0...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℕ₀ ∧ 𝑁 ≤ (𝑁 + 1)))
21	6, 17, 19, 20	syl3anbrc 1246	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...(𝑁 + 1)))
22	21	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(𝑁 + 1)))
23		oveq2 6658	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝑡) = (𝑁 + 1) → (0...(#‘𝑡)) = (0...(𝑁 + 1)))
24	23	eleq2d 2687	. . . . . . . . . . . . . . . . 17 ⊢ ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
25	24	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
26	25	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
27	22, 26	mpbird 247	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(#‘𝑡)))
28	15, 27	jca 554	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡))))
29		swrd0len 13422	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡))) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
30	28, 29	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
31	30	ex 450	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
32	31	3ad2antl2 1224	. . . . . . . . . 10 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁))
33	32	impcom 446	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
34	33	adantr 481	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁)
35		swrdcl 13419	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ Word (Vtx‘𝐺) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
36	35	3ad2ant2 1083	. . . . . . . . . . . 12 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
37	36	ad2antrl 764	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
38	37	ad2antrl 764	. . . . . . . . . 10 ⊢ (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
39		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝑡) = (𝑁 + 1) → ((#‘𝑡) − 1) = ((𝑁 + 1) − 1))
40	39	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑡) = (𝑁 + 1) → (0..^((#‘𝑡) − 1)) = (0..^((𝑁 + 1) − 1)))
41		nncn 11028	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
42		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
43	41, 42	pncand 10393	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
44	43	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = (0..^𝑁))
45	40, 44	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (0..^((#‘𝑡) − 1)) = (0..^𝑁))
46	45	raleqdv 3144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
47		nnz 11399	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
48		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
49	47, 48	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
50	18	lem1d 10957	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ≤ 𝑁)
51		eluz2 11693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) ↔ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ≤ 𝑁))
52	49, 47, 50, 51	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
53		fzoss2 12496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
55	54	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
56		ssralv 3666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0..^(𝑁 − 1)) ⊆ (0..^𝑁) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
58		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
59	21	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(𝑁 + 1)))
60	24	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
61	59, 60	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(#‘𝑡)))
62	61	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(#‘𝑡)))
63	54	sseld 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℕ → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
64	63	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
65	64	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66		swrd0fv 13439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖) = (𝑡‘𝑖))
67	66	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑡‘𝑖) = ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖))
68	58, 62, 65, 67	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘𝑖) = ((𝑡 substr ⟨0, 𝑁⟩)‘𝑖))
69	47	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → 𝑁 ∈ ℤ)
70		elfzom1elp1fzo 12534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
71	69, 70	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
72		swrd0fv 13439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)) = (𝑡‘(𝑖 + 1)))
73	72	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)))
74	58, 62, 71, 73	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)))
75	68, 74	preq12d 4276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))})
76	75	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
77	76	ralbidva 2985	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
78	77	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
79	78	ex 450	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
80	79	com23 86	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
81	57, 80	syld 47	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
82	46, 81	sylbid 230	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
83	82	ex 450	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → ((#‘𝑡) = (𝑁 + 1) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
84	83	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((#‘𝑡) = (𝑁 + 1) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
85	84	com14 96	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
86	85	imp 445	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
87	86	3adant1 1079	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
88	87	imp 445	. . . . . . . . . . . . 13 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
89	88	impcom 446	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
90	89	ad2antrl 764	. . . . . . . . . . 11 ⊢ (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑡 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
91		oveq1 6657	. . . . . . . . . . . . . 14 ⊢ ((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 → ((#‘(𝑡 substr ⟨0, 𝑁⟩)) − 1) = (𝑁 − 1))
92	91	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ ((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 → (0..^((#‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
93	92	adantr 481	. . . . . . . . . . . 12 ⊢ (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (0..^((#‘(𝑡 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
94	93	raleqdv 3144	. . . . . . . . . . 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‘𝐺)))
95	90, 94	mpbird 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 1107	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
97	19	ancli 574	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))
98	47	peano2zd 11485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℤ)
99		fznn 12408	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 + 1) ∈ ℤ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
101	97, 100	mpbird 247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1)))
102	101	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(𝑁 + 1)))
103		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((#‘𝑡) = (𝑁 + 1) → (1...(#‘𝑡)) = (1...(𝑁 + 1)))
104	103	eleq2d 2687	. . . . . . . . . . . . . . . . . . 19 ⊢ ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
105	104	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
106	105	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
107	102, 106	mpbird 247	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(#‘𝑡)))
108	96, 107	jca 554	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))))
109	108	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))))
110		swrd0fvlsw 13443	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))) → ( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)) = (𝑡‘(𝑁 − 1)))
111	109, 110	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)) = (𝑡‘(𝑁 − 1)))
112		swrd0fv0 13440	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑡))) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
113	108, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
114	113	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((𝑡 substr ⟨0, 𝑁⟩)‘0) = (𝑡‘0))
115	111, 114	preq12d 4276	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘0)})
116		eqcom 2629	. . . . . . . . . . . . . . . . 17 ⊢ (( lastS ‘𝑡) = (𝑡‘0) ↔ (𝑡‘0) = ( lastS ‘𝑡))
117	116	biimpi 206	. . . . . . . . . . . . . . . 16 ⊢ (( lastS ‘𝑡) = (𝑡‘0) → (𝑡‘0) = ( lastS ‘𝑡))
118	117	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = ( lastS ‘𝑡))
119		lsw 13351	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
120	119	3ad2ant2 1083	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
121	120	ad2antrl 764	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
122	121	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1)))
123	39	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → ((#‘𝑡) − 1) = ((𝑁 + 1) − 1))
124	123, 43	sylan9eqr 2678	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → ((#‘𝑡) − 1) = 𝑁)
125	124	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((#‘𝑡) − 1) = 𝑁)
126	125	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘((#‘𝑡) − 1)) = (𝑡‘𝑁))
127	118, 122, 126	3eqtrd 2660	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (𝑡‘𝑁))
128	127	preq2d 4275	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)})
129	39, 43	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((#‘𝑡) − 1) = 𝑁)
130	129	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (0..^((#‘𝑡) − 1)) = (0..^𝑁))
131	130	raleqdv 3144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132		fzo0end 12560	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
133		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = (𝑁 − 1) → (𝑡‘𝑖) = (𝑡‘(𝑁 − 1)))
134		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
135	134	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = (𝑁 − 1) → (𝑡‘(𝑖 + 1)) = (𝑡‘((𝑁 − 1) + 1)))
136	133, 135	preq12d 4276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = (𝑁 − 1) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))})
137	136	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = (𝑁 − 1) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
138	137	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 − 1) ∈ (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
139	132, 138	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
140	41, 42	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
141	140	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → (𝑡‘((𝑁 − 1) + 1)) = (𝑡‘𝑁))
142	141	preq2d 4275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)})
143	142	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
144	143	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
145	144	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
146	139, 145	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))
147	146	ex 450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
148	147	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
149	131, 148	sylbid 230	. . . . . . . . . . . . . . . . . . 19 ⊢ (((#‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
150	149	ex 450	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))))
151	150	com3r 87	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))))
152	151	3ad2ant3 1084	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))))
153	152	imp 445	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
154	153	impcom 446	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))
155	154	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))
156	128, 155	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} ∈ (Edg‘𝐺))
157	115, 156	eqeltrd 2701	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
158	157	adantl 482	. . . . . . . . . 10 ⊢ (((#‘(𝑡 substr ⟨0, 𝑁⟩)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → {( lastS ‘(𝑡 substr ⟨0, 𝑁⟩)), ((𝑡 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
159	38, 95, 158	3jca 1242	. . . . . . . . 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, 𝑁⟩)) = 𝑁)
161	159, 160	jca 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, 𝑁⟩)) = 𝑁))
162	34, 161	mpancom 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, 𝑁⟩)) = 𝑁))
163	162	exp31 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, 𝑁⟩)) = 𝑁))))
164	14, 163	sylbid 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, 𝑁⟩)) = 𝑁))))
165	164	imp32 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, 𝑁⟩)) = 𝑁))
166	9, 10	isclwwlksnx 26889	. . . . 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, 𝑁⟩)) = 𝑁)))
167	166	adantr 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, 𝑁⟩)) = 𝑁)))
168	165, 167	mpbird 247	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
169	5, 168	sylan2b 492	. 2 ⊢ ((𝑁 ∈ ℕ ∧ 𝑡 ∈ 𝐷) → (𝑡 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
170		clwwlksbij.f	. 2 ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr ⟨0, 𝑁⟩))
171	169, 170	fmptd 6385	1 ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 {crab 2916 ⊆ wss 3574 ∅c0 3915 {cpr 4179 ⟨cop 4183 class class class wbr 4653 ↦ cmpt 4729 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 0cc0 9936 1c1 9937 + caddc 9939 ≤ cle 10075 − cmin 10266 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 ..^cfzo 12465 #chash 13117 Word cword 13291 lastS clsw 13292 substr csubstr 13295 Vtxcvtx 25874 Edgcedg 25939 WWalkscwwlks 26717 WWalksN cwwlksn 26718 ClWWalksN cclwwlksn 26876

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-lsw 13300 df-substr 13303 df-wwlks 26722 df-wwlksn 26723 df-clwwlks 26877 df-clwwlksn 26878

This theorem is referenced by: clwwlksf1 26917 clwwlksfo 26918

W3C validator