Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑤 = 𝑡 → ( lastS ‘𝑤) = ( lastS ‘𝑡)) |
2 | | fveq1 6102 |
. . . . 5
⊢ (𝑤 = 𝑡 → (𝑤‘0) = (𝑡‘0)) |
3 | 1, 2 | eqeq12d 2625 |
. . . 4
⊢ (𝑤 = 𝑡 → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘𝑡) = (𝑡‘0))) |
4 | | clwwlkbij.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} |
5 | 3, 4 | elrab2 3333 |
. . 3
⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑡) = (𝑡‘0))) |
6 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
7 | | iswwlkn 26212 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑡 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)))) |
8 | 6, 7 | syl3an3 1353 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑡 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)))) |
9 | | iswwlk 26211 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑡 ∈ (𝑉 WWalks 𝐸) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸))) |
10 | 9 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ (𝑉 WWalks 𝐸) ↔ (𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸))) |
11 | 10 | anbi1d 737 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑡 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)))) |
12 | 8, 11 | bitrd 267 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)))) |
13 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑡 ∈ Word 𝑉) |
14 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
15 | 6, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) |
16 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
17 | 16 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1)) |
18 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (0...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ0
∧ 𝑁 ≤ (𝑁 + 1))) |
19 | 6, 15, 17, 18 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...(𝑁 + 1))) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(𝑁 + 1))) |
21 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑡) =
(𝑁 + 1) →
(0...(#‘𝑡)) =
(0...(𝑁 +
1))) |
22 | 21 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑡) =
(𝑁 + 1) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
25 | 20, 24 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (0...(#‘𝑡))) |
26 | 13, 25 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑡)))) |
27 | | swrd0len 13274 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑡))) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
29 | 28 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word 𝑉 ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
30 | 29 | 3ad2antl2 1217 |
. . . . . . . . . . . 12
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
31 | 30 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
32 | 31 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
33 | 32 | imp 444 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
34 | 33 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
35 | | swrdcl 13271 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ Word 𝑉 → (𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉) |
36 | 35 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉) |
37 | 36 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉) |
38 | 37 | ad2antrl 760 |
. . . . . . . . . 10
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉) |
39 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑡) =
(𝑁 + 1) →
((#‘𝑡) − 1) =
((𝑁 + 1) −
1)) |
40 | 39 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑡) =
(𝑁 + 1) →
(0..^((#‘𝑡) −
1)) = (0..^((𝑁 + 1) −
1))) |
41 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
42 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
43 | 41, 42 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
44 | 43 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 + 1) − 1)) =
(0..^𝑁)) |
45 | 40, 44 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) →
(0..^((#‘𝑡) −
1)) = (0..^𝑁)) |
46 | 45 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸)) |
47 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
48 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℤ) |
50 | 16 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ≤ 𝑁) |
51 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) ↔ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ≤ 𝑁)) |
52 | 49, 47, 50, 51 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘(𝑁 − 1))) |
53 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ →
(0..^(𝑁 − 1)) ⊆
(0..^𝑁)) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
56 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((0..^(𝑁 − 1))
⊆ (0..^𝑁) →
(∀𝑖 ∈
(0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸)) |
58 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑡 ∈ Word 𝑉) |
59 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(𝑁 + 1))) |
60 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (0...(#‘𝑡)) ↔ 𝑁 ∈ (0...(𝑁 + 1)))) |
61 | 59, 60 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → 𝑁 ∈ (0...(#‘𝑡))) |
62 | 61 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(#‘𝑡))) |
63 | 54 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁))) |
64 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) → (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ (0..^𝑁))) |
65 | 64 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁)) |
66 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑡 substr 〈0, 𝑁〉)‘𝑖) = (𝑡‘𝑖)) |
67 | 66 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑡‘𝑖) = ((𝑡 substr 〈0, 𝑁〉)‘𝑖)) |
68 | 58, 62, 65, 67 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘𝑖) = ((𝑡 substr 〈0, 𝑁〉)‘𝑖)) |
69 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) → 𝑁 ∈ ℤ) |
70 | | elfzom1elp1fzo 12402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
71 | 69, 70 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
72 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1)) = (𝑡‘(𝑖 + 1))) |
73 | 72 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑡)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))) |
74 | 58, 62, 71, 73 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑡‘(𝑖 + 1)) = ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))) |
75 | 68, 74 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))}) |
76 | 75 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
77 | 76 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
78 | 77 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) ∧ 𝑡 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
79 | 78 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (𝑡 ∈ Word 𝑉 → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
80 | 79 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑡 ∈ Word 𝑉 → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
81 | 57, 80 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑡 ∈ Word 𝑉 → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
82 | 46, 81 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑡) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑡 ∈ Word 𝑉 → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
83 | 82 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ →
((#‘𝑡) = (𝑁 + 1) → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑡 ∈ Word 𝑉 → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)))) |
84 | 83 | com23 84 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘𝑡) = (𝑁 + 1) → (𝑡 ∈ Word 𝑉 → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)))) |
85 | 84 | com14 94 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ Word 𝑉 → (∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)))) |
86 | 85 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
87 | 86 | 3adant1 1072 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
88 | 87 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
89 | 88 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
90 | 89 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
91 | 90 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
92 | 91 | ad2antrl 760 |
. . . . . . . . . . 11
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
93 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢
((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 → ((#‘(𝑡 substr 〈0, 𝑁〉)) − 1) = (𝑁 − 1)) |
94 | 93 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 → (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)) =
(0..^(𝑁 −
1))) |
95 | 94 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)) =
(0..^(𝑁 −
1))) |
96 | 95 | raleqdv 3121 |
. . . . . . . . . . 11
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
97 | 92, 96 | mpbird 246 |
. . . . . . . . . 10
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
98 | | simprl2 1100 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑡 ∈ Word 𝑉) |
99 | 17 | ancli 572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1))) |
100 | 47 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℤ) |
101 | | fznn 12278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 + 1) ∈ ℤ →
(𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ (1...(𝑁 + 1)) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≤ (𝑁 + 1)))) |
103 | 99, 102 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1))) |
104 | 103 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (1...(𝑁 + 1))) |
105 | 104 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(𝑁 + 1))) |
106 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑡) =
(𝑁 + 1) →
(1...(#‘𝑡)) =
(1...(𝑁 +
1))) |
107 | 106 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑡) =
(𝑁 + 1) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
109 | 108 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑁 ∈ (1...(#‘𝑡)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
110 | 105, 109 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → 𝑁 ∈ (1...(#‘𝑡))) |
111 | 98, 110 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → (𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑡)))) |
112 | 111 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑡)))) |
113 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑡))) → ( lastS ‘(𝑡 substr 〈0, 𝑁〉)) = (𝑡‘(𝑁 − 1))) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ( lastS ‘(𝑡 substr 〈0, 𝑁〉)) = (𝑡‘(𝑁 − 1))) |
115 | | swrd0fv0 13292 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑡))) → ((𝑡 substr 〈0, 𝑁〉)‘0) = (𝑡‘0)) |
116 | 111, 115 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → ((𝑡 substr 〈0, 𝑁〉)‘0) = (𝑡‘0)) |
117 | 116 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((𝑡 substr 〈0, 𝑁〉)‘0) = (𝑡‘0)) |
118 | 114, 117 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘0)}) |
119 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ (( lastS
‘𝑡) = (𝑡‘0) ↔ (𝑡‘0) = ( lastS ‘𝑡)) |
120 | 119 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (( lastS
‘𝑡) = (𝑡‘0) → (𝑡‘0) = ( lastS ‘𝑡)) |
121 | 120 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = ( lastS ‘𝑡)) |
122 | | lsw 13204 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ Word 𝑉 → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
123 | 122 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
124 | 123 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ( lastS ‘𝑡) = (𝑡‘((#‘𝑡) − 1))) |
126 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → ((#‘𝑡) − 1) = ((𝑁 + 1) − 1)) |
127 | 43 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑁 + 1) − 1) = 𝑁) |
128 | 126, 127 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → ((#‘𝑡) − 1) = 𝑁) |
129 | 128 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → ((#‘𝑡) − 1) = 𝑁) |
130 | 129 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘((#‘𝑡) − 1)) = (𝑡‘𝑁)) |
131 | 121, 125,
130 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (𝑡‘0) = (𝑡‘𝑁)) |
132 | 131 | preq2d 4219 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)}) |
133 | 39, 43 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
((#‘𝑡) − 1) =
𝑁) |
134 | 133 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(0..^((#‘𝑡) −
1)) = (0..^𝑁)) |
135 | 134 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸)) |
136 | | fzo0end 12426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) |
137 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = (𝑁 − 1) → (𝑡‘𝑖) = (𝑡‘(𝑁 − 1))) |
138 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1)) |
139 | 138 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = (𝑁 − 1) → (𝑡‘(𝑖 + 1)) = (𝑡‘((𝑁 − 1) + 1))) |
140 | 137, 139 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = (𝑁 − 1) → {(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))}) |
141 | 140 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = (𝑁 − 1) → ({(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ ran 𝐸)) |
142 | 141 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 − 1) ∈ (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ ran 𝐸) |
143 | 136, 142 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧
∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ ran 𝐸) |
144 | 41, 42 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
145 | 144 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ → (𝑡‘((𝑁 − 1) + 1)) = (𝑡‘𝑁)) |
146 | 145 | preq2d 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} = {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)}) |
147 | 146 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ ran 𝐸 ↔ {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
148 | 147 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ ran 𝐸 → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
149 | 148 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧
∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → ({(𝑡‘(𝑁 − 1)), (𝑡‘((𝑁 − 1) + 1))} ∈ ran 𝐸 → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
150 | 143, 149 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧
∀𝑖 ∈ (0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸) |
151 | 150 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
152 | 151 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈
(0..^𝑁){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
153 | 135, 152 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑡) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
154 | 153 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑡) =
(𝑁 + 1) → (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸))) |
155 | 154 | com3r 85 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑖 ∈
(0..^((#‘𝑡) −
1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸))) |
156 | 155 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑡) = (𝑁 + 1) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸))) |
157 | 156 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → (𝑁 ∈ ℕ → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
158 | 157 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
159 | 158 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸)) |
160 | 159 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸) |
161 | 160 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘𝑁)} ∈ ran 𝐸) |
162 | 132, 161 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {(𝑡‘(𝑁 − 1)), (𝑡‘0)} ∈ ran 𝐸) |
163 | 118, 162 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) |
164 | 163 | adantl 481 |
. . . . . . . . . 10
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) |
165 | 38, 97, 164 | 3jca 1235 |
. . . . . . . . 9
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸)) |
166 | | simpl 472 |
. . . . . . . . 9
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) |
167 | 165, 166 | jca 553 |
. . . . . . . 8
⊢
(((#‘(𝑡 substr
〈0, 𝑁〉)) = 𝑁 ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
168 | 34, 167 | mpancom 700 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ ((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1))) ∧ ( lastS ‘𝑡) = (𝑡‘0)) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
169 | 168 | exp31 628 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑡 ≠ ∅ ∧ 𝑡 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑡) − 1)){(𝑡‘𝑖), (𝑡‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘𝑡) = (𝑁 + 1)) → (( lastS ‘𝑡) = (𝑡‘0) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)))) |
170 | 12, 169 | sylbid 229 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (( lastS ‘𝑡) = (𝑡‘0) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)))) |
171 | 170 | imp32 448 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁)) |
172 | | isclwwlkn 26297 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑡 substr 〈0, 𝑁〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝑡 substr 〈0, 𝑁〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁))) |
173 | 6, 172 | syl3an3 1353 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑡 substr 〈0, 𝑁〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝑡 substr 〈0, 𝑁〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁))) |
174 | | isclwwlk 26296 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑡 substr 〈0, 𝑁〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸))) |
175 | 174 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑡 substr 〈0, 𝑁〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸))) |
176 | 175 | anbi1d 737 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑡 substr 〈0, 𝑁〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁) ↔ (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁))) |
177 | 173, 176 | bitrd 267 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑡 substr 〈0, 𝑁〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁))) |
178 | 177 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → ((𝑡 substr 〈0, 𝑁〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (((𝑡 substr 〈0, 𝑁〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑡 substr 〈0, 𝑁〉)) − 1)){((𝑡 substr 〈0, 𝑁〉)‘𝑖), ((𝑡 substr 〈0, 𝑁〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑡 substr 〈0, 𝑁〉)), ((𝑡 substr 〈0, 𝑁〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑡 substr 〈0, 𝑁〉)) = 𝑁))) |
179 | 171, 178 | mpbird 246 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑡 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑡) = (𝑡‘0))) → (𝑡 substr 〈0, 𝑁〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
180 | 5, 179 | sylan2b 491 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑡 ∈ 𝐷) → (𝑡 substr 〈0, 𝑁〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
181 | | clwwlkbij.f |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) |
182 | 180, 181 | fmptd 6292 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷⟶((𝑉 ClWWalksN 𝐸)‘𝑁)) |