Proof of Theorem clwlkclwwlklem2
Step | Hyp | Ref
| Expression |
1 | | f1fn 6263 |
. . . 4
⊢ (𝐸:dom 𝐸–1-1→𝑅 → 𝐸 Fn dom 𝐸) |
2 | | dffn3 6215 |
. . . 4
⊢ (𝐸 Fn dom 𝐸 ↔ 𝐸:dom 𝐸⟶ran 𝐸) |
3 | 1, 2 | sylib 208 |
. . 3
⊢ (𝐸:dom 𝐸–1-1→𝑅 → 𝐸:dom 𝐸⟶ran 𝐸) |
4 | | lencl 13510 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word dom 𝐸 → (♯‘𝐹) ∈
ℕ0) |
5 | | ffn 6206 |
. . . . . . . . . . 11
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹))) |
6 | | fnfz0hash 13422 |
. . . . . . . . . . 11
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ 𝑃 Fn (0...(♯‘𝐹))) → (♯‘𝑃) = ((♯‘𝐹) + 1)) |
7 | 4, 5, 6 | syl2an 495 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (♯‘𝑃) = ((♯‘𝐹) + 1)) |
8 | | ffz0iswrd 13518 |
. . . . . . . . . . . . . 14
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 ∈ Word 𝑉) |
9 | | lsw 13538 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → (lastS‘𝑃) = (𝑃‘((♯‘𝑃) − 1))) |
10 | 9 | ad6antr 779 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → (lastS‘𝑃) = (𝑃‘((♯‘𝑃) − 1))) |
11 | | oveq1 6820 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ ((♯‘𝑃)
− 1) = (((♯‘𝐹) + 1) − 1)) |
12 | 11 | fveq2d 6356 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ (𝑃‘((♯‘𝑃) − 1)) = (𝑃‘(((♯‘𝐹) + 1) − 1))) |
13 | 12 | ad4antlr 773 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → (𝑃‘((♯‘𝑃) − 1)) = (𝑃‘(((♯‘𝐹) + 1) − 1))) |
14 | | eqcom 2767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘(♯‘𝐹)) = (𝑃‘0)) |
15 | | nn0cn 11494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℂ) |
16 | | 1cnd 10248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝐹)
∈ ℕ0 → 1 ∈ ℂ) |
17 | 15, 16 | pncand 10585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝐹)
∈ ℕ0 → (((♯‘𝐹) + 1) − 1) = (♯‘𝐹)) |
18 | 17 | eqcomd 2766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) = (((♯‘𝐹) + 1) − 1)) |
19 | 18 | ad4antlr 773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (♯‘𝐹) = (((♯‘𝐹) + 1) − 1)) |
20 | 19 | fveq2d 6356 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝑃‘(♯‘𝐹)) = (𝑃‘(((♯‘𝐹) + 1) − 1))) |
21 | 20 | eqeq1d 2762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘(♯‘𝐹)) = (𝑃‘0) ↔ (𝑃‘(((♯‘𝐹) + 1) − 1)) = (𝑃‘0))) |
22 | 21 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘(♯‘𝐹)) = (𝑃‘0) → (𝑃‘(((♯‘𝐹) + 1) − 1)) = (𝑃‘0))) |
23 | 14, 22 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘(((♯‘𝐹) + 1) − 1)) = (𝑃‘0))) |
24 | 23 | adantld 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(((♯‘𝐹) + 1) − 1)) = (𝑃‘0))) |
25 | 24 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → (𝑃‘(((♯‘𝐹) + 1) − 1)) = (𝑃‘0)) |
26 | 10, 13, 25 | 3eqtrd 2798 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → (lastS‘𝑃) = (𝑃‘0)) |
27 | | nn0z 11592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℤ) |
28 | | peano2zm 11612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝐹)
∈ ℤ → ((♯‘𝐹) − 1) ∈
ℤ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) − 1) ∈
ℤ) |
30 | | nn0re 11493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℝ) |
31 | 30 | lem1d 11149 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) − 1) ≤ (♯‘𝐹)) |
32 | | eluz2 11885 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝐹)
∈ (ℤ≥‘((♯‘𝐹) − 1)) ↔ (((♯‘𝐹) − 1) ∈ ℤ
∧ (♯‘𝐹)
∈ ℤ ∧ ((♯‘𝐹) − 1) ≤ (♯‘𝐹))) |
33 | 29, 27, 31, 32 | syl3anbrc 1429 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈
(ℤ≥‘((♯‘𝐹) − 1))) |
34 | 33 | ad4antlr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (♯‘𝐹) ∈
(ℤ≥‘((♯‘𝐹) − 1))) |
35 | | fzoss2 12690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹)
∈ (ℤ≥‘((♯‘𝐹) − 1)) →
(0..^((♯‘𝐹)
− 1)) ⊆ (0..^(♯‘𝐹))) |
36 | | ssralv 3807 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹))
→ (∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((♯‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((♯‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
38 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → 𝐸:dom 𝐸⟶ran 𝐸) |
39 | 38 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((♯‘𝐹) − 1))) → 𝐸:dom 𝐸⟶ran 𝐸) |
40 | | wrdf 13496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐸) |
41 | | simpll 807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹:(0..^(♯‘𝐹))⟶dom 𝐸 ∧ (♯‘𝐹) ∈ ℕ0) ∧ 𝑖 ∈
(0..^((♯‘𝐹)
− 1))) → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐸) |
42 | | fzossrbm1 12691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((♯‘𝐹)
∈ ℤ → (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹))) |
43 | 27, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((♯‘𝐹)
∈ ℕ0 → (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹))) |
44 | 43 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐹:(0..^(♯‘𝐹))⟶dom 𝐸 ∧ (♯‘𝐹) ∈ ℕ0) →
(0..^((♯‘𝐹)
− 1)) ⊆ (0..^(♯‘𝐹))) |
45 | 44 | sselda 3744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹:(0..^(♯‘𝐹))⟶dom 𝐸 ∧ (♯‘𝐹) ∈ ℕ0) ∧ 𝑖 ∈
(0..^((♯‘𝐹)
− 1))) → 𝑖
∈ (0..^(♯‘𝐹))) |
46 | 41, 45 | ffvelrnd 6523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐹:(0..^(♯‘𝐹))⟶dom 𝐸 ∧ (♯‘𝐹) ∈ ℕ0) ∧ 𝑖 ∈
(0..^((♯‘𝐹)
− 1))) → (𝐹‘𝑖) ∈ dom 𝐸) |
47 | 46 | exp31 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐸 → ((♯‘𝐹) ∈ ℕ0 → (𝑖 ∈
(0..^((♯‘𝐹)
− 1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
48 | 40, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 ∈ Word dom 𝐸 → ((♯‘𝐹) ∈ ℕ0
→ (𝑖 ∈
(0..^((♯‘𝐹)
− 1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
49 | 48 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) → ((♯‘𝐹) ∈ ℕ0 → (𝑖 ∈
(0..^((♯‘𝐹)
− 1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
50 | 49 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) → (𝑖 ∈
(0..^((♯‘𝐹)
− 1)) → (𝐹‘𝑖) ∈ dom 𝐸)) |
51 | 50 | ad3antrrr 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝑖 ∈ (0..^((♯‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)) |
52 | 51 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((♯‘𝐹) − 1))) → (𝐹‘𝑖) ∈ dom 𝐸) |
53 | 39, 52 | ffvelrnd 6523 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((♯‘𝐹) − 1))) → (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸) |
54 | | eqcom 2767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = (𝐸‘(𝐹‘𝑖))) |
55 | 54 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = (𝐸‘(𝐹‘𝑖))) |
56 | 55 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸)) |
57 | 53, 56 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((♯‘𝐹) − 1))) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
58 | 57 | ralimdva 3100 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^((♯‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
59 | 37, 58 | syldc 48 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
60 | 59 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
61 | 60 | impcom 445 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
62 | | breq2 4808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ (2 ≤ (♯‘𝑃) ↔ 2 ≤ ((♯‘𝐹) + 1))) |
63 | 62 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
→ (2 ≤ (♯‘𝑃) ↔ 2 ≤ ((♯‘𝐹) + 1))) |
64 | | 2re 11282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 2 ∈
ℝ |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝐹)
∈ ℕ0 → 2 ∈ ℝ) |
66 | | 1red 10247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝐹)
∈ ℕ0 → 1 ∈ ℝ) |
67 | 65, 66, 30 | lesubaddd 10816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝐹)
∈ ℕ0 → ((2 − 1) ≤ (♯‘𝐹) ↔ 2 ≤
((♯‘𝐹) +
1))) |
68 | | 2m1e1 11327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (2
− 1) = 1 |
69 | 68 | breq1i 4811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((2
− 1) ≤ (♯‘𝐹) ↔ 1 ≤ (♯‘𝐹)) |
70 | | elnnnn0c 11530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((♯‘𝐹)
∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ0 ∧ 1 ≤
(♯‘𝐹))) |
71 | 70 | simplbi2 656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝐹)
∈ ℕ0 → (1 ≤ (♯‘𝐹) → (♯‘𝐹) ∈ ℕ)) |
72 | 69, 71 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝐹)
∈ ℕ0 → ((2 − 1) ≤ (♯‘𝐹) → (♯‘𝐹) ∈
ℕ)) |
73 | 67, 72 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝐹)
∈ ℕ0 → (2 ≤ ((♯‘𝐹) + 1) → (♯‘𝐹) ∈
ℕ)) |
74 | 73 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) → (2 ≤
((♯‘𝐹) + 1)
→ (♯‘𝐹)
∈ ℕ)) |
75 | 74 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
→ (2 ≤ ((♯‘𝐹) + 1) → (♯‘𝐹) ∈
ℕ)) |
76 | 63, 75 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
→ (2 ≤ (♯‘𝑃) → (♯‘𝐹) ∈ ℕ)) |
77 | 76 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) → (♯‘𝐹) ∈ ℕ) |
78 | 77 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (♯‘𝐹) ∈ ℕ) |
79 | | lbfzo0 12702 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
(0..^(♯‘𝐹))
↔ (♯‘𝐹)
∈ ℕ) |
80 | 78, 79 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → 0 ∈ (0..^(♯‘𝐹))) |
81 | | fzoend 12753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 ∈
(0..^(♯‘𝐹))
→ ((♯‘𝐹)
− 1) ∈ (0..^(♯‘𝐹))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) |
83 | | fveq2 6352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = ((♯‘𝐹) − 1) → (𝐹‘𝑖) = (𝐹‘((♯‘𝐹) − 1))) |
84 | 83 | fveq2d 6356 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = ((♯‘𝐹) − 1) → (𝐸‘(𝐹‘𝑖)) = (𝐸‘(𝐹‘((♯‘𝐹) − 1)))) |
85 | | fveq2 6352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = ((♯‘𝐹) − 1) → (𝑃‘𝑖) = (𝑃‘((♯‘𝐹) − 1))) |
86 | | oveq1 6820 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = ((♯‘𝐹) − 1) → (𝑖 + 1) = (((♯‘𝐹) − 1) +
1)) |
87 | 86 | fveq2d 6356 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = ((♯‘𝐹) − 1) → (𝑃‘(𝑖 + 1)) = (𝑃‘(((♯‘𝐹) − 1) + 1))) |
88 | 85, 87 | preq12d 4420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = ((♯‘𝐹) − 1) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(((♯‘𝐹) − 1) + 1))}) |
89 | 84, 88 | eqeq12d 2775 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = ((♯‘𝐹) − 1) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(((♯‘𝐹) − 1) + 1))})) |
90 | 89 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 = ((♯‘𝐹) − 1)) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(((♯‘𝐹) − 1) + 1))})) |
91 | 82, 90 | rspcdv 3452 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(((♯‘𝐹) − 1) + 1))})) |
92 | 15, 16 | npcand 10588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝐹)
∈ ℕ0 → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
93 | 92 | ad4antlr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
94 | 93 | fveq2d 6356 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝑃‘(((♯‘𝐹) − 1) + 1)) = (𝑃‘(♯‘𝐹))) |
95 | 94 | preq2d 4419 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(((♯‘𝐹) − 1) + 1))} = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))}) |
96 | 95 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(((♯‘𝐹) − 1) + 1))} ↔ (𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))})) |
97 | 40 | ad4antlr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐸) |
98 | 73 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (2 ≤
((♯‘𝐹) + 1)
→ ((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℕ)) |
99 | 62, 98 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ (2 ≤ (♯‘𝑃) → ((♯‘𝐹) ∈ ℕ0 →
(♯‘𝐹) ∈
ℕ))) |
100 | 99 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝑃) = ((♯‘𝐹) + 1) → (2 ≤ (♯‘𝑃) → (♯‘𝐹) ∈
ℕ))) |
101 | 100 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) →
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ (2 ≤ (♯‘𝑃) → (♯‘𝐹) ∈ ℕ))) |
102 | 101 | imp31 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) → (♯‘𝐹) ∈ ℕ) |
103 | 102, 79 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) → 0 ∈ (0..^(♯‘𝐹))) |
104 | 103, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) |
105 | 97, 104 | ffvelrnd 6523 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) → (𝐹‘((♯‘𝐹) − 1)) ∈ dom 𝐸) |
106 | 105 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝐹‘((♯‘𝐹) − 1)) ∈ dom 𝐸) |
107 | 38, 106 | ffvelrnd 6523 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → (𝐸‘(𝐹‘((♯‘𝐹) − 1))) ∈ ran 𝐸) |
108 | | eqcom 2767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ↔ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} = (𝐸‘(𝐹‘((♯‘𝐹) − 1)))) |
109 | 108 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} = (𝐸‘(𝐹‘((♯‘𝐹) − 1)))) |
110 | 109 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} → ({(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘((♯‘𝐹) − 1))) ∈ ran 𝐸)) |
111 | 107, 110 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸)) |
112 | 96, 111 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((♯‘𝐹) − 1))) = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(((♯‘𝐹) − 1) + 1))} → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸)) |
113 | 91, 112 | syldc 48 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸)) |
114 | 113 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸)) |
115 | 114 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸) |
116 | | preq2 4413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} = {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))}) |
117 | 116 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → ({(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸)) |
118 | 117 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ({(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸)) |
119 | 118 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → ({(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘(♯‘𝐹))} ∈ ran 𝐸)) |
120 | 115, 119 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸) |
121 | 26, 61, 120 | 3jca 1123 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
∧ 2 ≤ (♯‘𝑃)) ∧ 𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |
122 | 121 | exp41 639 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (♯‘𝐹) ∈ ℕ0) ∧
(♯‘𝑃) =
((♯‘𝐹) + 1))
→ (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
123 | 122 | exp41 639 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (𝐹 ∈ Word dom 𝐸 → ((♯‘𝐹) ∈ ℕ0 →
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))))) |
124 | 8, 123 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝐹 ∈ Word dom 𝐸 → ((♯‘𝐹) ∈ ℕ0 →
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))))) |
125 | 124 | com13 88 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝑃) = ((♯‘𝐹) + 1) → (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))))) |
126 | 4, 125 | mpcom 38 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝑃) = ((♯‘𝐹) + 1) → (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))) |
127 | 126 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → ((♯‘𝑃) = ((♯‘𝐹) + 1) → (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
128 | 7, 127 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
129 | 128 | expcom 450 |
. . . . . . . 8
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝐹 ∈ Word dom 𝐸 → (2 ≤ (♯‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
130 | 129 | com14 96 |
. . . . . . 7
⊢ (𝐸:dom 𝐸⟶ran 𝐸 → (𝐹 ∈ Word dom 𝐸 → (2 ≤ (♯‘𝑃) → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
131 | 130 | imp 444 |
. . . . . 6
⊢ ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → (2 ≤ (♯‘𝑃) → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
132 | 131 | com13 88 |
. . . . 5
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (2 ≤ (♯‘𝑃) → ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
133 | 132 | imp 444 |
. . . 4
⊢ ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
134 | 133 | com12 32 |
. . 3
⊢ ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
135 | 3, 134 | sylan 489 |
. 2
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝐹 ∈ Word dom 𝐸) → ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
136 | 135 | 3imp 1102 |
1
⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) → ((lastS‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |