clwwlkf - Metamath Proof Explorer

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

Theorem clwwlkf 30435

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

**Hypotheses**
Ref	Expression
clwwlkf1o.d	⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
clwwlkf1o.f	⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁))

**Assertion**
Ref	Expression
clwwlkf	⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))

Distinct variable groups: 𝑤,𝐺 𝑤,𝑁 𝑡,𝐷 𝑡,𝐺,𝑤 𝑡,𝑁 Allowed substitution hints: 𝐷(𝑤) 𝐹(𝑤, 𝑡)

Proof of Theorem clwwlkf Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6888	. . . . 5 ⊢ (𝑤 = 𝑡 → (lastS‘𝑤) = (lastS‘𝑡))
2		fveq1 6887	. . . . 5 ⊢ (𝑤 = 𝑡 → (𝑤‘0) = (𝑡‘0))
3	1, 2	eqeq12d 2782	. . . 4 ⊢ (𝑤 = 𝑡 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑡) = (𝑡‘0)))
4		clwwlkf1o.d	. . . 4 ⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}
5	3, 4	elrab2 3657	. . 3 ⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0)))
6		nnnn0 12529	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
7		iswwlksn 30224	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1))))
8	6, 7	syl 18	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑡 ∈ (WWalks‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1))))
9		eqid 2766	. . . . . . . . . 10 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
10		eqid 2766	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
11	9, 10	iswwlks 30222	. . . . . . . . 9 ⊢ (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
12	11	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (WWalks‘𝐺) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
13	12	anbi1d 643	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑡 ∈ (WWalks‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))))
14	8, 13	bitrd 282	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))))
15		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑡 ∈ Word (Vtx‘𝐺))
16		peano2nn0 12562	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
17	6, 16	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ₀)
18		nnre 12258	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
19	18	lep1d 12164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1))
20		elfz2nn0 13665	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (0...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℕ₀ ∧ 𝑁 ≤ (𝑁 + 1)))
21	6, 17, 19, 20	syl3anbrc 1362	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...(𝑁 + 1)))
22	21	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(𝑁 + 1)))
23		oveq2 7431	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑡) = (𝑁 + 1) → (0...(♯‘𝑡)) = (0...(𝑁 + 1)))
24	23	eleq2d 2852	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
25	24	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
26	25	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
27	22, 26	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(♯‘𝑡)))
28	15, 27	jca 521	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡))))
29		pfxlen 14745	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡))) → (♯‘(𝑡 prefix 𝑁)) = 𝑁)
30	28, 29	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (♯‘(𝑡 prefix 𝑁)) = 𝑁)
31	30	ex 418	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (♯‘(𝑡 prefix 𝑁)) = 𝑁))
32	31	3ad2antl2 1205	. . . . . . . . . 10 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (♯‘(𝑡 prefix 𝑁)) = 𝑁))
33	32	impcom 413	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (♯‘(𝑡 prefix 𝑁)) = 𝑁)
34	33	adantr 486	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (♯‘(𝑡 prefix 𝑁)) = 𝑁)
35		pfxcl 14739	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ Word (Vtx‘𝐺) → (𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺))
36	35	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺))
37	36	ad2antrl 741	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺))
38	37	ad2antrl 741	. . . . . . . . . 10 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺))
39		oveq1 7430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑡) = (𝑁 + 1) → ((♯‘𝑡) − 1) = ((𝑁 + 1) − 1))
40	39	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑡) = (𝑁 + 1) → (0..^((♯‘𝑡) − 1)) = (0..^((𝑁 + 1) − 1)))
41		nncn 12259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
42		1cnd 11220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
43	41, 42	pncand 11588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
44	43	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = (0..^𝑁))
45	40, 44	sylan9eqr 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (0..^((♯‘𝑡) − 1)) = (0..^𝑁))
46	45	raleqdv 3326	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
47		nnz 12630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
48		peano2zm 12655	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
49	47, 48	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
50	18	lem1d 12166	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ≤ 𝑁)
51		eluz2 12886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) ↔ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ≤ 𝑁))
52	49, 47, 50, 51	syl3anbrc 1362	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
53		fzoss2 13735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
54	52, 53	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
55	54	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
56		ssralv 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0..^(𝑁 − 1)) ⊆ (0..^𝑁) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
57	55, 56	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
58		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
59	21	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(𝑁 + 1)))
60	24	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(♯‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1))))
61	59, 60	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(♯‘𝑡)))
62	61	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(♯‘𝑡)))
63	54	sseld 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℕ → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
64	63	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁)))
65	64	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66		pfxfv 14744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑡 prefix 𝑁)‘𝑖) = (𝑡‘𝑖))
67	66	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑡‘𝑖) = ((𝑡 prefix 𝑁)‘𝑖))
68	58, 62, 65, 67	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘𝑖) = ((𝑡 prefix 𝑁)‘𝑖))
69	47	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → 𝑁 ∈ ℤ)
70		elfzom1elp1fzo 13780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
71	69, 70	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
72		pfxfv 14744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑡 prefix 𝑁)‘(𝑖 + 1)) = (𝑡‘(𝑖 + 1)))
73	72	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → (𝑡‘(𝑖 + 1)) = ((𝑡 prefix 𝑁)‘(𝑖 + 1)))
74	58, 62, 71, 73	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘(𝑖 + 1)) = ((𝑡 prefix 𝑁)‘(𝑖 + 1)))
75	68, 74	preq12d 4712	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))})
76	75	eleq1d 2851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
77	76	ralbidva 3189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
78	77	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
79	78	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
80	79	com23 87	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
81	57, 80	syld 48	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
82	46, 81	sylbid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (♯‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
83	82	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → ((♯‘𝑡) = (𝑁 + 1) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
84	83	com23 87	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((♯‘𝑡) = (𝑁 + 1) → (𝑡 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
85	84	com14 97	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
86	85	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
87	86	3adant1 1148	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
88	87	imp 412	. . . . . . . . . . . . 13 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
89	88	impcom 413	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
90	89	ad2antrl 741	. . . . . . . . . . 11 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
91		oveq1 7430	. . . . . . . . . . . . . 14 ⊢ ((♯‘(𝑡 prefix 𝑁)) = 𝑁 → ((♯‘(𝑡 prefix 𝑁)) − 1) = (𝑁 − 1))
92	91	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝑡 prefix 𝑁)) = 𝑁 → (0..^((♯‘(𝑡 prefix 𝑁)) − 1)) = (0..^(𝑁 − 1)))
93	92	adantr 486	. . . . . . . . . . . 12 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (0..^((♯‘(𝑡 prefix 𝑁)) − 1)) = (0..^(𝑁 − 1)))
94	93	raleqdv 3326	. . . . . . . . . . 11 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
95	90, 94	mpbird 260	. . . . . . . . . 10 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
96		simprl2 1238	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → 𝑡 ∈ Word (Vtx‘𝐺))
97	19	ancli 558	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))
98	47	peano2zd 12721	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℤ)
99		fznn 13639	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 + 1) ∈ ℤ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
100	98, 99	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))))
101	97, 100	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1)))
102	101	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(𝑁 + 1)))
103		oveq2 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑡) = (𝑁 + 1) → (1...(♯‘𝑡)) = (1...(𝑁 + 1)))
104	103	eleq2d 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ (1...(♯‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
105	104	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (1...(♯‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
106	105	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (𝑁 ∈ (1...(♯‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1))))
107	102, 106	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(♯‘𝑡)))
108	96, 107	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))))
109	108	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))))
110		pfxfvlsw 14756	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))) → (lastS‘(𝑡 prefix 𝑁)) = (𝑡‘(𝑁 − 1)))
111	109, 110	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (lastS‘(𝑡 prefix 𝑁)) = (𝑡‘(𝑁 − 1)))
112		pfxfv0 14753	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑡))) → ((𝑡 prefix 𝑁)‘0) = (𝑡‘0))
113	108, 112	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → ((𝑡 prefix 𝑁)‘0) = (𝑡‘0))
114	113	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → ((𝑡 prefix 𝑁)‘0) = (𝑡‘0))
115	111, 114	preq12d 4712	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘0)})
116		eqcom 2773	. . . . . . . . . . . . . . . 16 ⊢ ((lastS‘𝑡) = (𝑡‘0) ↔ (𝑡‘0) = (lastS‘𝑡))
117	116	bilani 510	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (lastS‘𝑡))
118		lsw 14621	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ Word (Vtx‘𝐺) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
119	118	3ad2ant2 1152	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
120	119	ad2antrl 741	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
121	120	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (lastS‘𝑡) = (𝑡‘((♯‘𝑡) − 1)))
122	39	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → ((♯‘𝑡) − 1) = ((𝑁 + 1) − 1))
123	122, 43	sylan9eqr 2823	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → ((♯‘𝑡) − 1) = 𝑁)
124	123	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → ((♯‘𝑡) − 1) = 𝑁)
125	124	fveq2d 6892	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡‘((♯‘𝑡) − 1)) = (𝑡‘𝑁))
126	117, 121, 125	3eqtrd 2805	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (𝑡‘𝑁))
127	126	preq2d 4711	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)})
128	39, 43	sylan9eq 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((♯‘𝑡) − 1) = 𝑁)
129	128	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (0..^((♯‘𝑡) − 1)) = (0..^𝑁))
130	129	raleqdv 3326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
131		fzo0end 13806	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
132		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = (𝑁 − 1) → (𝑡‘𝑖) = (𝑡‘(𝑁 − 1)))
133		fvoveq1 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = (𝑁 − 1) → (𝑡‘(𝑖 + 1)) = (𝑡‘((𝑁 − 1) + 1)))
134	132, 133	preq12d 4712	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = (𝑁 − 1) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))})
135	134	eleq1d 2851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = (𝑁 − 1) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
136	135	rspcva 3582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 − 1) ∈ (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
137	131, 136	sylan 592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
138	41, 42	npcand 11591	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
139	138	fveq2d 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ → (𝑡‘((𝑁 − 1) + 1)) = (𝑡‘𝑁))
140	139	preq2d 4711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)})
141	140	eleq1d 2851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
142	141	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
143	142	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
144	137, 143	mpd 16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))
145	144	ex 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
146	145	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
147	130, 146	sylbid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑡) = (𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
148	147	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))))
149	148	com3r 88	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))))
150	149	3ad2ant3 1153	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))))
151	150	imp 412	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺)))
152	151	impcom 413	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))
153	152	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ (Edg‘𝐺))
154	127, 153	eqeltrd 2866	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} ∈ (Edg‘𝐺))
155	115, 154	eqeltrd 2866	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))
156	155	adantl 487	. . . . . . . . . 10 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))
157	38, 95, 156	3jca 1146	. . . . . . . . 9 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → ((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)))
158		simpl 488	. . . . . . . . 9 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (♯‘(𝑡 prefix 𝑁)) = 𝑁)
159	157, 158	jca 521	. . . . . . . 8 ⊢ (((♯‘(𝑡 prefix 𝑁)) = 𝑁 ∧ ((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0))) → (((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 prefix 𝑁)) = 𝑁))
160	34, 159	mpancom 701	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1))) ∧ (lastS‘𝑡) = (𝑡‘0)) → (((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 prefix 𝑁)) = 𝑁))
161	160	exp31 425	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑡) = (𝑁 + 1)) → ((lastS‘𝑡) = (𝑡‘0) → (((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 prefix 𝑁)) = 𝑁))))
162	14, 161	sylbid 243	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝑡 ∈ (𝑁 WWalksN 𝐺) → ((lastS‘𝑡) = (𝑡‘0) → (((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 prefix 𝑁)) = 𝑁))))
163	162	imp32 424	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0))) → (((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 prefix 𝑁)) = 𝑁))
164	9, 10	isclwwlknx 30424	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((𝑡 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺) ↔ (((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 prefix 𝑁)) = 𝑁)))
165	164	adantr 486	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0))) → ((𝑡 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺) ↔ (((𝑡 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑡 prefix 𝑁)) − 1)){((𝑡 prefix 𝑁)‘𝑖), ((𝑡 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑡 prefix 𝑁)), ((𝑡 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘(𝑡 prefix 𝑁)) = 𝑁)))
166	163, 165	mpbird 260	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑡 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑡) = (𝑡‘0))) → (𝑡 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺))
167	5, 166	sylan2b 606	. 2 ⊢ ((𝑁 ∈ ℕ ∧ 𝑡 ∈ 𝐷) → (𝑡 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺))
168		clwwlkf1o.f	. 2 ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁))
169	167, 168	fmptd 7116	1 ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 ∀wral 3082 {crab 3419 ⊆ wss 3908 ∅c0 4289 {cpr 4596 class class class wbr 5114 ↦ cmpt 5197 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 0cc0 11118 1c1 11119 + caddc 11121 ≤ cle 11262 − cmin 11459 ℕcn 12251 ℕ₀cn0 12522 ℤcz 12609 ℤ_≥cuz 12880 ...cfz 13553 ..^cfzo 13701 ♯chash 14386 Word cword 14570 lastSclsw 14619 prefix cpfx 14732 Vtxcvtx 29383 Edgcedg 29434 WWalkscwwlks 30211 WWalksN cwwlksn 30212 ClWWalksN cclwwlkn 30412

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8703 df-map 8835 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-nn 12252 df-n0 12523 df-xnn0 12596 df-z 12610 df-uz 12881 df-fz 13554 df-fzo 13702 df-hash 14387 df-word 14571 df-lsw 14620 df-substr 14701 df-pfx 14733 df-wwlks 30216 df-wwlksn 30217 df-clwwlk 30370 df-clwwlkn 30413

This theorem is used by: clwwlkf1 30437 clwwlkfo 30438

W3C validator