clwlkclwwlklem2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > clwlkclwwlklem2		Structured version Visualization version GIF version

Theorem clwlkclwwlklem2 41209

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

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

Distinct variable groups: 𝑖,𝐸 𝑃,𝑖 𝑅,𝑖 𝑖,𝑉 𝑖,𝐹

**Proof of Theorem clwlkclwwlklem2**
Step	Hyp	Ref	Expression
1		f1fn 6015	. . . 4 ⊢ (𝐸:dom 𝐸–1-1→𝑅 → 𝐸 Fn dom 𝐸)
2		dffn3 5967	. . . 4 ⊢ (𝐸 Fn dom 𝐸 ↔ 𝐸:dom 𝐸⟶ran 𝐸)
3	1, 2	sylib 207	. . 3 ⊢ (𝐸:dom 𝐸–1-1→𝑅 → 𝐸:dom 𝐸⟶ran 𝐸)
4		lencl 13179	. . . . . . . . . . 11 ⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈ ℕ₀)
5		ffn 5958	. . . . . . . . . . 11 ⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 Fn (0...(#‘𝐹)))
6		fnfz0hash 13087	. . . . . . . . . . 11 ⊢ (((#‘𝐹) ∈ ℕ₀ ∧ 𝑃 Fn (0...(#‘𝐹))) → (#‘𝑃) = ((#‘𝐹) + 1))
7	4, 5, 6	syl2an 493	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (#‘𝑃) = ((#‘𝐹) + 1))
8		ffz0iswrd 13187	. . . . . . . . . . . . . 14 ⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 ∈ Word 𝑉)
9		lsw 13204	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
10	9	ad6antr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
11		oveq1 6556	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((#‘𝑃) = ((#‘𝐹) + 1) → ((#‘𝑃) − 1) = (((#‘𝐹) + 1) − 1))
12	11	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ ((#‘𝑃) = ((#‘𝐹) + 1) → (𝑃‘((#‘𝑃) − 1)) = (𝑃‘(((#‘𝐹) + 1) − 1)))
13	12	ad4antlr 765	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (𝑃‘((#‘𝑃) − 1)) = (𝑃‘(((#‘𝐹) + 1) − 1)))
14		eqcom 2617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘(#‘𝐹)) = (𝑃‘0))
15		nn0cn 11179	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) ∈ ℂ)
16		1cnd 9935	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((#‘𝐹) ∈ ℕ₀ → 1 ∈ ℂ)
17	15, 16	pncand 10272	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((#‘𝐹) ∈ ℕ₀ → (((#‘𝐹) + 1) − 1) = (#‘𝐹))
18	17	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) = (((#‘𝐹) + 1) − 1))
19	18	ad4antlr 765	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (#‘𝐹) = (((#‘𝐹) + 1) − 1))
20	19	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝑃‘(#‘𝐹)) = (𝑃‘(((#‘𝐹) + 1) − 1)))
21	20	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) ↔ (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0)))
22	21	biimpd 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0)))
23	14, 22	syl5bi 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0)))
24	23	adantld 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0)))
25	24	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0))
26	10, 13, 25	3eqtrd 2648	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ( lastS ‘𝑃) = (𝑃‘0))
27		nn0z 11277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) ∈ ℤ)
28		peano2zm 11297	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝐹) ∈ ℤ → ((#‘𝐹) − 1) ∈ ℤ)
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝐹) ∈ ℕ₀ → ((#‘𝐹) − 1) ∈ ℤ)
30		nn0re 11178	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) ∈ ℝ)
31	30	lem1d 10836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝐹) ∈ ℕ₀ → ((#‘𝐹) − 1) ≤ (#‘𝐹))
32		eluz2 11569	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘((#‘𝐹) − 1)) ↔ (((#‘𝐹) − 1) ∈ ℤ ∧ (#‘𝐹) ∈ ℤ ∧ ((#‘𝐹) − 1) ≤ (#‘𝐹)))
33	29, 27, 31, 32	syl3anbrc 1239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) ∈ (ℤ_≥‘((#‘𝐹) − 1)))
34	33	ad4antlr 765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (#‘𝐹) ∈ (ℤ_≥‘((#‘𝐹) − 1)))
35		fzoss2 12365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘((#‘𝐹) − 1)) → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
36		ssralv 3629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
37	34, 35, 36	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
38		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → 𝐸:dom 𝐸⟶ran 𝐸)
39	38	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → 𝐸:dom 𝐸⟶ran 𝐸)
40		wrdf 13165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸)
41		simpll 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ₀) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸)
42		fzossrbm1 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((#‘𝐹) ∈ ℤ → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
43	27, 42	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((#‘𝐹) ∈ ℕ₀ → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
44	43	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ₀) → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
45	44	sselda 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ₀) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → 𝑖 ∈ (0..^(#‘𝐹)))
46	41, 45	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ₀) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → (𝐹‘𝑖) ∈ dom 𝐸)
47	46	exp31 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((#‘𝐹) ∈ ℕ₀ → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)))
48	40, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) ∈ ℕ₀ → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)))
49	48	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) → ((#‘𝐹) ∈ ℕ₀ → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)))
50	49	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸))
51	50	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸))
52	51	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → (𝐹‘𝑖) ∈ dom 𝐸)
53	39, 52	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸)
54		eqcom 2617	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = (𝐸‘(𝐹‘𝑖)))
55	54	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = (𝐸‘(𝐹‘𝑖)))
56	55	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸))
57	53, 56	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
58	57	ralimdva 2945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
59	37, 58	syld 46	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
60	59	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
61	60	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
62	61	impcom 445	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)
63		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) ↔ 2 ≤ ((#‘𝐹) + 1)))
64	63	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) → (2 ≤ (#‘𝑃) ↔ 2 ≤ ((#‘𝐹) + 1)))
65		2re 10967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 2 ∈ ℝ
66	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((#‘𝐹) ∈ ℕ₀ → 2 ∈ ℝ)
67		1red 9934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((#‘𝐹) ∈ ℕ₀ → 1 ∈ ℝ)
68	66, 67, 30	lesubaddd 10503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((#‘𝐹) ∈ ℕ₀ → ((2 − 1) ≤ (#‘𝐹) ↔ 2 ≤ ((#‘𝐹) + 1)))
69		2m1e1 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 − 1) = 1
70	69	breq1i 4590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((2 − 1) ≤ (#‘𝐹) ↔ 1 ≤ (#‘𝐹))
71		elnnnn0c 11215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((#‘𝐹) ∈ ℕ ↔ ((#‘𝐹) ∈ ℕ₀ ∧ 1 ≤ (#‘𝐹)))
72	71	simplbi2 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((#‘𝐹) ∈ ℕ₀ → (1 ≤ (#‘𝐹) → (#‘𝐹) ∈ ℕ))
73	70, 72	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((#‘𝐹) ∈ ℕ₀ → ((2 − 1) ≤ (#‘𝐹) → (#‘𝐹) ∈ ℕ))
74	68, 73	sylbird 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((#‘𝐹) ∈ ℕ₀ → (2 ≤ ((#‘𝐹) + 1) → (#‘𝐹) ∈ ℕ))
75	74	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) → (2 ≤ ((#‘𝐹) + 1) → (#‘𝐹) ∈ ℕ))
76	75	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) → (2 ≤ ((#‘𝐹) + 1) → (#‘𝐹) ∈ ℕ))
77	64, 76	sylbid 229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) → (2 ≤ (#‘𝑃) → (#‘𝐹) ∈ ℕ))
78	77	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) → (#‘𝐹) ∈ ℕ)
79	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (#‘𝐹) ∈ ℕ)
80		lbfzo0 12375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ (0..^(#‘𝐹)) ↔ (#‘𝐹) ∈ ℕ)
81	79, 80	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → 0 ∈ (0..^(#‘𝐹)))
82		fzoend 12425	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 ∈ (0..^(#‘𝐹)) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
84		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = ((#‘𝐹) − 1) → (𝐹‘𝑖) = (𝐹‘((#‘𝐹) − 1)))
85	84	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = ((#‘𝐹) − 1) → (𝐸‘(𝐹‘𝑖)) = (𝐸‘(𝐹‘((#‘𝐹) − 1))))
86		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = ((#‘𝐹) − 1) → (𝑃‘𝑖) = (𝑃‘((#‘𝐹) − 1)))
87		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = ((#‘𝐹) − 1) → (𝑖 + 1) = (((#‘𝐹) − 1) + 1))
88	87	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 = ((#‘𝐹) − 1) → (𝑃‘(𝑖 + 1)) = (𝑃‘(((#‘𝐹) − 1) + 1)))
89	86, 88	preq12d 4220	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = ((#‘𝐹) − 1) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))})
90	85, 89	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = ((#‘𝐹) − 1) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))}))
91	90	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 = ((#‘𝐹) − 1)) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))}))
92	83, 91	rspcdv 3285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))}))
93	15, 16	npcand 10275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((#‘𝐹) ∈ ℕ₀ → (((#‘𝐹) − 1) + 1) = (#‘𝐹))
94	93	ad4antlr 765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (((#‘𝐹) − 1) + 1) = (#‘𝐹))
95	94	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝑃‘(((#‘𝐹) − 1) + 1)) = (𝑃‘(#‘𝐹)))
96	95	preq2d 4219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))})
97	96	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))}))
98	40	ad4antlr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸)
99	74	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 ≤ ((#‘𝐹) + 1) → ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) ∈ ℕ))
100	63, 99	syl6bi 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) ∈ ℕ)))
101	100	com3r 85	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((#‘𝐹) ∈ ℕ₀ → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (#‘𝐹) ∈ ℕ)))
102	101	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (#‘𝐹) ∈ ℕ)))
103	102	imp31 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) → (#‘𝐹) ∈ ℕ)
104	103, 80	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) → 0 ∈ (0..^(#‘𝐹)))
105	104, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
106	98, 105	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) → (𝐹‘((#‘𝐹) − 1)) ∈ dom 𝐸)
107	106	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝐹‘((#‘𝐹) − 1)) ∈ dom 𝐸)
108	38, 107	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝐸‘(𝐹‘((#‘𝐹) − 1))) ∈ ran 𝐸)
109		eqcom 2617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} = (𝐸‘(𝐹‘((#‘𝐹) − 1))))
110	109	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} = (𝐸‘(𝐹‘((#‘𝐹) − 1))))
111	110	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) ∈ ran 𝐸))
112	108, 111	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
113	97, 112	sylbid 229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
114	92, 113	syld 46	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
115	114	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
116	115	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
117	116	impcom 445	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)
118		preq2 4213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))})
119	118	eleq1d 2672	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
120	119	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
121	120	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸))
122	117, 121	mpbird 246	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)
123	26, 62, 122	3jca 1235	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) ∧ 2 ≤ (#‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))
124	123	exp41 636	. . . . . . . . . . . . . . 15 ⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ₀) ∧ (#‘𝑃) = ((#‘𝐹) + 1)) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))
125	124	exp41 636	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ Word 𝑉 → (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) ∈ ℕ₀ → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))))
126	8, 125	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) ∈ ℕ₀ → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))))
127	126	com13 86	. . . . . . . . . . . 12 ⊢ ((#‘𝐹) ∈ ℕ₀ → (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))))
128	4, 127	mpcom 37	. . . . . . . . . . 11 ⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))))
129	128	imp 444	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))
130	7, 129	mpd 15	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))
131	130	expcom 450	. . . . . . . 8 ⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝐹 ∈ Word dom 𝐸 → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))
132	131	com14 94	. . . . . . 7 ⊢ (𝐸:dom 𝐸⟶ran 𝐸 → (𝐹 ∈ Word dom 𝐸 → (2 ≤ (#‘𝑃) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))
133	132	imp 444	. . . . . 6 ⊢ ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → (2 ≤ (#‘𝑃) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))
134	133	com13 86	. . . . 5 ⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (2 ≤ (#‘𝑃) → ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))
135	134	imp 444	. . . 4 ⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))
136	135	com12 32	. . 3 ⊢ ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))
137	3, 136	sylan 487	. 2 ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝐹 ∈ Word dom 𝐸) → ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))
138	137	3imp 1249	1 ⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ⊆ wss 3540 {cpr 4127 class class class wbr 4583 dom cdm 5038 ran crn 5039 Fn wfn 5799 ⟶wf 5800 –1-1→wf1 5801 ‘cfv 5804 (class class class)co 6549 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 ≤ cle 9954 − cmin 10145 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 ..^cfzo 12334 #chash 12979 Word cword 13146 lastS clsw 13147

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-lsw 13155

This theorem is referenced by: clwlkclwwlklem3 41210 clwlksfclwwlk 41269

W3C validator