clwlkclwwlklem2a - Metamath Proof Explorer

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

Theorem clwlkclwwlklem2a 30379

Description: Lemma for clwlkclwwlklem2 30381. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.)

**Hypothesis**
Ref	Expression
clwlkclwwlklem2.f	⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ if(𝑥 < ((♯‘𝑃) − 2), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})))

**Assertion**
Ref	Expression
clwlkclwwlklem2a	⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))))

Distinct variable groups: 𝑥,𝑃 𝑥,𝐸 𝑥,𝑉 𝑖,𝐸 𝑖,𝐹 𝑃,𝑖 𝑅,𝑖,𝑥 𝑖,𝑉 Allowed substitution hint: 𝐹(𝑥)

**Proof of Theorem clwlkclwwlklem2a**
Step	Hyp	Ref	Expression
1		simpl 488	. . . . . . . . . 10 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → 𝑥 < ((♯‘𝑃) − 2))
2		f1f1orn 6839	. . . . . . . . . . . . . 14 ⊢ (𝐸:dom 𝐸–1-1→𝑅 → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
3	2	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
4	3	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
5	4	ad2antrl 741	. . . . . . . . . . 11 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
6		elfzo0 13748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↔ (𝑥 ∈ ℕ₀ ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ 𝑥 < ((♯‘𝑃) − 1)))
7		lencl 14590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℕ₀)
8		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
9	8	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) ∧ (𝑥 < ((♯‘𝑃) − 2) ∧ 2 ≤ (♯‘𝑃))) → 𝑥 ∈ ℕ₀)
10		elnn0z 12622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 ∈ ℕ₀ ↔ (𝑥 ∈ ℤ ∧ 0 ≤ 𝑥))
11		0red 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑥 ∈ ℤ ∧ (♯‘𝑃) ∈ ℕ₀) → 0 ∈ ℝ)
12		zre 12613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
13	12	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑥 ∈ ℤ ∧ (♯‘𝑃) ∈ ℕ₀) → 𝑥 ∈ ℝ)
14		nn0re 12531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℝ)
15		2re 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ 2 ∈ ℝ
16	15	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((♯‘𝑃) ∈ ℕ₀ → 2 ∈ ℝ)
17	14, 16	resubcld 11660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) ∈ ℝ)
18	17	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑥 ∈ ℤ ∧ (♯‘𝑃) ∈ ℕ₀) → ((♯‘𝑃) − 2) ∈ ℝ)
19		lelttr 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ((♯‘𝑃) − 2) ∈ ℝ) → ((0 ≤ 𝑥 ∧ 𝑥 < ((♯‘𝑃) − 2)) → 0 < ((♯‘𝑃) − 2)))
20	11, 13, 18, 19	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑥 ∈ ℤ ∧ (♯‘𝑃) ∈ ℕ₀) → ((0 ≤ 𝑥 ∧ 𝑥 < ((♯‘𝑃) − 2)) → 0 < ((♯‘𝑃) − 2)))
21		nn0z 12633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℤ)
22		2z 12644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ 2 ∈ ℤ
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((♯‘𝑃) ∈ ℕ₀ → 2 ∈ ℤ)
24	21, 23	zsubcld 12723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) ∈ ℤ)
25	24	anim1i 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 0 < ((♯‘𝑃) − 2)) → (((♯‘𝑃) − 2) ∈ ℤ ∧ 0 < ((♯‘𝑃) − 2)))
26		elnnz 12619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((♯‘𝑃) − 2) ∈ ℕ ↔ (((♯‘𝑃) − 2) ∈ ℤ ∧ 0 < ((♯‘𝑃) − 2)))
27	25, 26	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 0 < ((♯‘𝑃) − 2)) → ((♯‘𝑃) − 2) ∈ ℕ)
28		nn0cn 12532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℂ)
29		peano2cnm 11542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((♯‘𝑃) ∈ ℂ → ((♯‘𝑃) − 1) ∈ ℂ)
30	28, 29	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ∈ ℂ)
31	30	subid1d 11576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (((♯‘𝑃) − 1) − 0) = ((♯‘𝑃) − 1))
32	31	oveq1d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((((♯‘𝑃) − 1) − 0) − 1) = (((♯‘𝑃) − 1) − 1))
33		1cnd 11220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((♯‘𝑃) ∈ ℕ₀ → 1 ∈ ℂ)
34	28, 33, 33	subsub4d 11618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (((♯‘𝑃) − 1) − 1) = ((♯‘𝑃) − (1 + 1)))
35		1p1e2 12382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (1 + 1) = 2
36	35	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 + 1) = 2)
37	36	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − (1 + 1)) = ((♯‘𝑃) − 2))
38	34, 37	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (((♯‘𝑃) − 1) − 1) = ((♯‘𝑃) − 2))
39	32, 38	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((((♯‘𝑃) − 1) − 0) − 1) = ((♯‘𝑃) − 2))
40	39	eleq1d 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ ↔ ((♯‘𝑃) − 2) ∈ ℕ))
41	40	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 0 < ((♯‘𝑃) − 2)) → (((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ ↔ ((♯‘𝑃) − 2) ∈ ℕ))
42	27, 41	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 0 < ((♯‘𝑃) − 2)) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ)
43	42	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (0 < ((♯‘𝑃) − 2) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))
44	43	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑥 ∈ ℤ ∧ (♯‘𝑃) ∈ ℕ₀) → (0 < ((♯‘𝑃) − 2) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))
45	20, 44	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑥 ∈ ℤ ∧ (♯‘𝑃) ∈ ℕ₀) → ((0 ≤ 𝑥 ∧ 𝑥 < ((♯‘𝑃) − 2)) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))
46	45	exp4b 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑥 ∈ ℤ → ((♯‘𝑃) ∈ ℕ₀ → (0 ≤ 𝑥 → (𝑥 < ((♯‘𝑃) − 2) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))))
47	46	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑥 ∈ ℤ → (0 ≤ 𝑥 → ((♯‘𝑃) ∈ ℕ₀ → (𝑥 < ((♯‘𝑃) − 2) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))))
48	47	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑥 ∈ ℤ ∧ 0 ≤ 𝑥) → ((♯‘𝑃) ∈ ℕ₀ → (𝑥 < ((♯‘𝑃) − 2) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ)))
49	10, 48	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 ∈ ℕ₀ → ((♯‘𝑃) ∈ ℕ₀ → (𝑥 < ((♯‘𝑃) − 2) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ)))
50	49	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 < ((♯‘𝑃) − 2) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))
51	50	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 < ((♯‘𝑃) − 2) → ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))
52	51	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ 2 ≤ (♯‘𝑃)) → ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ))
53	52	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) ∧ (𝑥 < ((♯‘𝑃) − 2) ∧ 2 ≤ (♯‘𝑃))) → ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ)
54		df-2 12321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 2 = (1 + 1)
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((♯‘𝑃) ∈ ℕ₀ → 2 = (1 + 1))
56	55	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) = ((♯‘𝑃) − (1 + 1)))
57	31	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) − 0))
58	57	oveq1d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (((♯‘𝑃) − 1) − 1) = ((((♯‘𝑃) − 1) − 0) − 1))
59	56, 34, 58	3eqtr2d 2807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) = ((((♯‘𝑃) − 1) − 0) − 1))
60	59	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → ((♯‘𝑃) − 2) = ((((♯‘𝑃) − 1) − 0) − 1))
61	60	breq2d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 < ((♯‘𝑃) − 2) ↔ 𝑥 < ((((♯‘𝑃) − 1) − 0) − 1)))
62	61	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 < ((♯‘𝑃) − 2) → ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → 𝑥 < ((((♯‘𝑃) − 1) − 0) − 1)))
63	62	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ 2 ≤ (♯‘𝑃)) → ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → 𝑥 < ((((♯‘𝑃) − 1) − 0) − 1)))
64	63	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) ∧ (𝑥 < ((♯‘𝑃) − 2) ∧ 2 ≤ (♯‘𝑃))) → 𝑥 < ((((♯‘𝑃) − 1) − 0) − 1))
65		elfzo0 13748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)) ↔ (𝑥 ∈ ℕ₀ ∧ ((((♯‘𝑃) − 1) − 0) − 1) ∈ ℕ ∧ 𝑥 < ((((♯‘𝑃) − 1) − 0) − 1)))
66	9, 53, 64, 65	syl3anbrc 1362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) ∧ (𝑥 < ((♯‘𝑃) − 2) ∧ 2 ≤ (♯‘𝑃))) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))
67	66	exp32 426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 < ((♯‘𝑃) − 2) → (2 ≤ (♯‘𝑃) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))))
68	67	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 < ((♯‘𝑃) − 1) → (𝑥 < ((♯‘𝑃) − 2) → (2 ≤ (♯‘𝑃) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1))))))
69	68	com24 96	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (2 ≤ (♯‘𝑃) → (𝑥 < ((♯‘𝑃) − 2) → (𝑥 < ((♯‘𝑃) − 1) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1))))))
70	69	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℕ₀ → ((♯‘𝑃) ∈ ℕ₀ → (2 ≤ (♯‘𝑃) → (𝑥 < ((♯‘𝑃) − 2) → (𝑥 < ((♯‘𝑃) − 1) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))))))
71	70	com25 100	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ℕ₀ → (𝑥 < ((♯‘𝑃) − 1) → (2 ≤ (♯‘𝑃) → (𝑥 < ((♯‘𝑃) − 2) → ((♯‘𝑃) ∈ ℕ₀ → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))))))
72	71	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) → (2 ≤ (♯‘𝑃) → (𝑥 < ((♯‘𝑃) − 2) → ((♯‘𝑃) ∈ ℕ₀ → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1))))))
73	72	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℕ₀ ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ 𝑥 < ((♯‘𝑃) − 1)) → (2 ≤ (♯‘𝑃) → (𝑥 < ((♯‘𝑃) − 2) → ((♯‘𝑃) ∈ ℕ₀ → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1))))))
74	73	com14 97	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (2 ≤ (♯‘𝑃) → (𝑥 < ((♯‘𝑃) − 2) → ((𝑥 ∈ ℕ₀ ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ 𝑥 < ((♯‘𝑃) − 1)) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1))))))
75	7, 74	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (♯‘𝑃) → (𝑥 < ((♯‘𝑃) − 2) → ((𝑥 ∈ ℕ₀ ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ 𝑥 < ((♯‘𝑃) − 1)) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1))))))
76	75	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑥 < ((♯‘𝑃) − 2) → ((𝑥 ∈ ℕ₀ ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ 𝑥 < ((♯‘𝑃) − 1)) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))))
77	76	3adant1 1148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑥 < ((♯‘𝑃) − 2) → ((𝑥 ∈ ℕ₀ ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ 𝑥 < ((♯‘𝑃) − 1)) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))))
78	6, 77	syl7bi 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑥 < ((♯‘𝑃) − 2) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))))
79	78	com13 89	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → (𝑥 < ((♯‘𝑃) − 2) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))))
80	79	imp31 423	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ (0..^((♯‘𝑃) − 1)) ∧ 𝑥 < ((♯‘𝑃) − 2)) ∧ (𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃))) → 𝑥 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)))
81		fveq2 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑥 → (𝑃‘𝑖) = (𝑃‘𝑥))
82		fvoveq1 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑥 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑥 + 1)))
83	81, 82	preq12d 4712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑥 → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})
84	83	eleq1d 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑥 → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸))
85	84	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ (0..^((♯‘𝑃) − 1)) ∧ 𝑥 < ((♯‘𝑃) − 2)) ∧ (𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃))) ∧ 𝑖 = 𝑥) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸))
86	80, 85	rspcdv 3576	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ (0..^((♯‘𝑃) − 1)) ∧ 𝑥 < ((♯‘𝑃) − 2)) ∧ (𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃))) → (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸))
87	86	ex 418	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (0..^((♯‘𝑃) − 1)) ∧ 𝑥 < ((♯‘𝑃) − 2)) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)))
88	87	com13 89	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑥 ∈ (0..^((♯‘𝑃) − 1)) ∧ 𝑥 < ((♯‘𝑃) − 2)) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)))
89	88	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑥 ∈ (0..^((♯‘𝑃) − 1)) ∧ 𝑥 < ((♯‘𝑃) − 2)) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)))
90	89	impcom 413	. . . . . . . . . . . . 13 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ((𝑥 ∈ (0..^((♯‘𝑃) − 1)) ∧ 𝑥 < ((♯‘𝑃) − 2)) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸))
91	90	expdimp 458	. . . . . . . . . . . 12 ⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → (𝑥 < ((♯‘𝑃) − 2) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸))
92	91	impcom 413	. . . . . . . . . . 11 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)
93		f1ocnvdm 7294	. . . . . . . . . . 11 ⊢ ((𝐸:dom 𝐸–1-1-onto→ran 𝐸 ∧ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸) → (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸)
94	5, 92, 93	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸)
95	1, 94	jca 521	. . . . . . . . 9 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → (𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸))
96	95	orcd 887	. . . . . . . 8 ⊢ ((𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → ((𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) ∨ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) ∈ dom 𝐸)))
97		simpl 488	. . . . . . . . . 10 ⊢ ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → ¬ 𝑥 < ((♯‘𝑃) − 2))
98	4	ad2antrl 741	. . . . . . . . . . 11 ⊢ ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
99		nn0z 12633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ∈ ℤ)
100		peano2zm 12655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((♯‘𝑃) ∈ ℤ → ((♯‘𝑃) − 1) ∈ ℤ)
101	21, 100	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ∈ ℤ)
102	99, 101	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 ∈ ℤ ∧ ((♯‘𝑃) − 1) ∈ ℤ))
103		zltlem1 12665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑥 ∈ ℤ ∧ ((♯‘𝑃) − 1) ∈ ℤ) → (𝑥 < ((♯‘𝑃) − 1) ↔ 𝑥 ≤ (((♯‘𝑃) − 1) − 1)))
104	102, 103	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 < ((♯‘𝑃) − 1) ↔ 𝑥 ≤ (((♯‘𝑃) − 1) − 1)))
105	38	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (((♯‘𝑃) − 1) − 1) = ((♯‘𝑃) − 2))
106	105	breq2d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 ≤ (((♯‘𝑃) − 1) − 1) ↔ 𝑥 ≤ ((♯‘𝑃) − 2)))
107	106	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 ≤ (((♯‘𝑃) − 1) − 1) → 𝑥 ≤ ((♯‘𝑃) − 2)))
108	104, 107	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℕ₀ ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 < ((♯‘𝑃) − 1) → 𝑥 ≤ ((♯‘𝑃) − 2)))
109	108	impancom 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) → ((♯‘𝑃) ∈ ℕ₀ → 𝑥 ≤ ((♯‘𝑃) − 2)))
110	109	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) → 𝑥 ≤ ((♯‘𝑃) − 2))
111		nn0re 12531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ∈ ℝ)
112	111	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) → 𝑥 ∈ ℝ)
113	112, 17	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 ∈ ℝ ∧ ((♯‘𝑃) − 2) ∈ ℝ))
114		lenlt 11306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ ((♯‘𝑃) − 2) ∈ ℝ) → (𝑥 ≤ ((♯‘𝑃) − 2) ↔ ¬ ((♯‘𝑃) − 2) < 𝑥))
115	113, 114	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) → (𝑥 ≤ ((♯‘𝑃) − 2) ↔ ¬ ((♯‘𝑃) − 2) < 𝑥))
116	110, 115	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) → ¬ ((♯‘𝑃) − 2) < 𝑥)
117	116	anim1i 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) ∧ ¬ 𝑥 < ((♯‘𝑃) − 2)) → (¬ ((♯‘𝑃) − 2) < 𝑥 ∧ ¬ 𝑥 < ((♯‘𝑃) − 2)))
118	113	ancomd 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) → (((♯‘𝑃) − 2) ∈ ℝ ∧ 𝑥 ∈ ℝ))
119	118	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) ∧ ¬ 𝑥 < ((♯‘𝑃) − 2)) → (((♯‘𝑃) − 2) ∈ ℝ ∧ 𝑥 ∈ ℝ))
120		lttri3 11311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((♯‘𝑃) − 2) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((♯‘𝑃) − 2) = 𝑥 ↔ (¬ ((♯‘𝑃) − 2) < 𝑥 ∧ ¬ 𝑥 < ((♯‘𝑃) − 2))))
121	119, 120	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) ∧ ¬ 𝑥 < ((♯‘𝑃) − 2)) → (((♯‘𝑃) − 2) = 𝑥 ↔ (¬ ((♯‘𝑃) − 2) < 𝑥 ∧ ¬ 𝑥 < ((♯‘𝑃) − 2))))
122	117, 121	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) ∧ (♯‘𝑃) ∈ ℕ₀) ∧ ¬ 𝑥 < ((♯‘𝑃) − 2)) → ((♯‘𝑃) − 2) = 𝑥)
123	122	exp31 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) → ((♯‘𝑃) ∈ ℕ₀ → (¬ 𝑥 < ((♯‘𝑃) − 2) → ((♯‘𝑃) − 2) = 𝑥)))
124	123	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑥 < ((♯‘𝑃) − 1)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) = 𝑥)))
125	124	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℕ₀ ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ 𝑥 < ((♯‘𝑃) − 1)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) = 𝑥)))
126	6, 125	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) = 𝑥)))
127	126	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 2) = 𝑥))
128	7, 127	syl5com 32	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ Word 𝑉 → ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → ((♯‘𝑃) − 2) = 𝑥))
129	128	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → ((♯‘𝑃) − 2) = 𝑥))
130	129	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → ((♯‘𝑃) − 2) = 𝑥)
131	130	fveq2d 6892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → (𝑃‘((♯‘𝑃) − 2)) = (𝑃‘𝑥))
132	131	preq1d 4710	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝑥), (𝑃‘0)})
133	132	eleq1d 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → ({(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))
134	133	biimpd 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → ({(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))
135	134	exp32 426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → ({(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))))
136	135	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 < ((♯‘𝑃) − 2) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → ({(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))))
137	136	com14 97	. . . . . . . . . . . . . . . 16 ⊢ ({(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))))
138	137	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))))
139	138	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))))
140	139	com12 33	. . . . . . . . . . . . 13 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → (¬ 𝑥 < ((♯‘𝑃) − 2) → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))))
141	140	imp31 423	. . . . . . . . . . . 12 ⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → (¬ 𝑥 < ((♯‘𝑃) − 2) → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸))
142	141	impcom 413	. . . . . . . . . . 11 ⊢ ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸)
143		f1ocnvdm 7294	. . . . . . . . . . 11 ⊢ ((𝐸:dom 𝐸–1-1-onto→ran 𝐸 ∧ {(𝑃‘𝑥), (𝑃‘0)} ∈ ran 𝐸) → (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) ∈ dom 𝐸)
144	98, 142, 143	syl2anc 596	. . . . . . . . . 10 ⊢ ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) ∈ dom 𝐸)
145	97, 144	jca 521	. . . . . . . . 9 ⊢ ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) ∈ dom 𝐸))
146	145	olcd 888	. . . . . . . 8 ⊢ ((¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1)))) → ((𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) ∨ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) ∈ dom 𝐸)))
147	96, 146	pm2.61ian 824	. . . . . . 7 ⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → ((𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) ∨ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) ∈ dom 𝐸)))
148		ifel 4537	. . . . . . 7 ⊢ (if(𝑥 < ((♯‘𝑃) − 2), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})) ∈ dom 𝐸 ↔ ((𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) ∨ (¬ 𝑥 < ((♯‘𝑃) − 2) ∧ (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) ∈ dom 𝐸)))
149	147, 148	sylibr 237	. . . . . 6 ⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → if(𝑥 < ((♯‘𝑃) − 2), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})) ∈ dom 𝐸)
150		clwlkclwwlklem2.f	. . . . . 6 ⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ if(𝑥 < ((♯‘𝑃) − 2), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (^◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})))
151	149, 150	fmptd 7116	. . . . 5 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → 𝐹:(0..^((♯‘𝑃) − 1))⟶dom 𝐸)
152		iswrdi 14574	. . . . 5 ⊢ (𝐹:(0..^((♯‘𝑃) − 1))⟶dom 𝐸 → 𝐹 ∈ Word dom 𝐸)
153	151, 152	syl 18	. . . 4 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → 𝐹 ∈ Word dom 𝐸)
154		wrdf 14575	. . . . . . . 8 ⊢ (𝑃 ∈ Word 𝑉 → 𝑃:(0..^(♯‘𝑃))⟶𝑉)
155	154	adantr 486	. . . . . . 7 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃:(0..^(♯‘𝑃))⟶𝑉)
156	150	clwlkclwwlklem2a2 30374	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘𝐹) = ((♯‘𝑃) − 1))
157		fzoval 13707	. . . . . . . . . . 11 ⊢ ((♯‘𝑃) ∈ ℤ → (0..^(♯‘𝑃)) = (0...((♯‘𝑃) − 1)))
158	7, 21, 157	3syl 19	. . . . . . . . . 10 ⊢ (𝑃 ∈ Word 𝑉 → (0..^(♯‘𝑃)) = (0...((♯‘𝑃) − 1)))
159		oveq2 7431	. . . . . . . . . . 11 ⊢ (((♯‘𝑃) − 1) = (♯‘𝐹) → (0...((♯‘𝑃) − 1)) = (0...(♯‘𝐹)))
160	159	eqcoms 2774	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = ((♯‘𝑃) − 1) → (0...((♯‘𝑃) − 1)) = (0...(♯‘𝐹)))
161	158, 160	sylan9eq 2821	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ (♯‘𝐹) = ((♯‘𝑃) − 1)) → (0..^(♯‘𝑃)) = (0...(♯‘𝐹)))
162	156, 161	syldan 603	. . . . . . . 8 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (0..^(♯‘𝑃)) = (0...(♯‘𝐹)))
163	162	feq2d 6696	. . . . . . 7 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃:(0..^(♯‘𝑃))⟶𝑉 ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉))
164	155, 163	mpbid 235	. . . . . 6 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
165	164	3adant1 1148	. . . . 5 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
166	165	adantr 486	. . . 4 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
167		clwlkclwwlklem2a1 30373	. . . . . . 7 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
168	167	3adant1 1148	. . . . . 6 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
169	168	imp 412	. . . . 5 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)
170	156	3adant1 1148	. . . . . . . 8 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘𝐹) = ((♯‘𝑃) − 1))
171	170	adantr 486	. . . . . . 7 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (lastS‘𝑃) = (𝑃‘0)) → (♯‘𝐹) = ((♯‘𝑃) − 1))
172	150	clwlkclwwlklem2a4 30378	. . . . . . . . . 10 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))
173	172	impl 461	. . . . . . . . 9 ⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (lastS‘𝑃) = (𝑃‘0)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
174	173	ralimdva 3180	. . . . . . . 8 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (lastS‘𝑃) = (𝑃‘0)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
175		oveq2 7431	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = ((♯‘𝑃) − 1) → (0..^(♯‘𝐹)) = (0..^((♯‘𝑃) − 1)))
176	175	raleqdv 3326	. . . . . . . . 9 ⊢ ((♯‘𝐹) = ((♯‘𝑃) − 1) → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
177	176	imbi2d 343	. . . . . . . 8 ⊢ ((♯‘𝐹) = ((♯‘𝑃) − 1) → ((∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))
178	174, 177	imbitrrid 249	. . . . . . 7 ⊢ ((♯‘𝐹) = ((♯‘𝑃) − 1) → (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (lastS‘𝑃) = (𝑃‘0)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))
179	171, 178	mpcom 39	. . . . . 6 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (lastS‘𝑃) = (𝑃‘0)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
180	179	adantrr 730	. . . . 5 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
181	169, 180	mpd 16	. . . 4 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})
182	153, 166, 181	3jca 1146	. . 3 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
183	150	clwlkclwwlklem2a3 30375	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃‘(♯‘𝐹)) = (lastS‘𝑃))
184	183	3adant1 1148	. . . . . . . . 9 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃‘(♯‘𝐹)) = (lastS‘𝑃))
185	184	eqcomd 2772	. . . . . . . 8 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (lastS‘𝑃) = (𝑃‘(♯‘𝐹)))
186	185	eqeq2d 2777	. . . . . . 7 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃‘0) = (lastS‘𝑃) ↔ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
187	186	biimpcd 252	. . . . . 6 ⊢ ((𝑃‘0) = (lastS‘𝑃) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃‘0) = (𝑃‘(♯‘𝐹))))
188	187	eqcoms 2774	. . . . 5 ⊢ ((lastS‘𝑃) = (𝑃‘0) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃‘0) = (𝑃‘(♯‘𝐹))))
189	188	adantr 486	. . . 4 ⊢ (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃‘0) = (𝑃‘(♯‘𝐹))))
190	189	impcom 413	. . 3 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
191	182, 190	jca 521	. 2 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
192	191	ex 418	1 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ∀wral 3082 ifcif 4492 {cpr 4596 class class class wbr 5114 ↦ cmpt 5197 ^◡ccnv 5665 dom cdm 5666 ran crn 5667 ⟶wf 6539 –1-1→wf1 6540 –1-1-onto→wf1o 6542 ‘cfv 6543 (class class class)co 7423 ℂcc 11116 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 < clt 11261 ≤ cle 11262 − cmin 11459 ℕcn 12251 2c2 12313 ℕ₀cn0 12522 ℤcz 12609 ...cfz 13553 ..^cfzo 13701 ♯chash 14386 Word cword 14570 lastSclsw 14619

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-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-2 12321 df-n0 12523 df-z 12610 df-uz 12881 df-fz 13554 df-fzo 13702 df-hash 14387 df-word 14571 df-lsw 14620

This theorem is used by: clwlkclwwlklem1 30380

W3C validator