Step | Hyp | Ref
| Expression |
1 | | wwlkextbij.d |
. 2
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} |
2 | | 3anass 1035 |
. . . . . 6
⊢
(((#‘𝑤) =
(𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ((#‘𝑤) = (𝑁 + 2) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
3 | 2 | anbi2i 726 |
. . . . 5
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = (𝑁 + 2) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
4 | | anass 679 |
. . . . 5
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = (𝑁 + 2) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
5 | 3, 4 | bitr4i 266 |
. . . 4
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) ↔ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
6 | | wwlknprop 26214 |
. . . . . . . . . 10
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉))) |
7 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → 𝑁 ∈
ℕ0) |
8 | | simpl 472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) → 𝑤 ∈ Word 𝑉) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → 𝑤 ∈ Word 𝑉) |
10 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
11 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
13 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
14 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
2 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 0 < 2) |
16 | 10, 12, 13, 15 | addgegt0d 10480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
2)) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → 0 < (𝑁 + 2)) |
18 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑤) =
(𝑁 + 2) → (0 <
(#‘𝑤) ↔ 0 <
(𝑁 + 2))) |
19 | 18 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → (0 < (#‘𝑤) ↔ 0 < (𝑁 + 2))) |
20 | 17, 19 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → 0 < (#‘𝑤)) |
21 | | hashgt0n0 13017 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Word 𝑉 ∧ 0 < (#‘𝑤)) → 𝑤 ≠ ∅) |
22 | 9, 20, 21 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → 𝑤 ≠ ∅) |
23 | | lswcl 13208 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Word 𝑉 ∧ 𝑤 ≠ ∅) → ( lastS ‘𝑤) ∈ 𝑉) |
24 | 9, 22, 23 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → ( lastS ‘𝑤) ∈ 𝑉) |
25 | 24 | adantrr 749 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → ( lastS ‘𝑤) ∈ 𝑉) |
26 | | swrdcl 13271 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ Word 𝑉 → (𝑤 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉) |
27 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 = (𝑤 substr 〈0, (𝑁 + 1)〉) → (𝑊 ∈ Word 𝑉 ↔ (𝑤 substr 〈0, (𝑁 + 1)〉) ∈ Word 𝑉)) |
28 | 26, 27 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 = (𝑤 substr 〈0, (𝑁 + 1)〉) → (𝑤 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉)) |
29 | 28 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 → (𝑤 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) → (𝑤 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉)) |
31 | 30 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ Word 𝑉 → (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) → 𝑊 ∈ Word 𝑉)) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) → (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) → 𝑊 ∈ Word 𝑉)) |
33 | 32 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → 𝑊 ∈ Word 𝑉) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → 𝑊 ∈ Word 𝑉) |
35 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 = (𝑤 substr 〈0, (𝑁 + 1)〉) → (𝑊 ++ 〈“( lastS ‘𝑤)”〉) = ((𝑤 substr 〈0, (𝑁 + 1)〉) ++ 〈“(
lastS ‘𝑤)”〉)) |
36 | 35 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 → (𝑊 ++ 〈“( lastS ‘𝑤)”〉) = ((𝑤 substr 〈0, (𝑁 + 1)〉) ++ 〈“(
lastS ‘𝑤)”〉)) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) → (𝑊 ++ 〈“( lastS ‘𝑤)”〉) = ((𝑤 substr 〈0, (𝑁 + 1)〉) ++ 〈“(
lastS ‘𝑤)”〉)) |
38 | 37 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → (𝑊 ++ 〈“( lastS ‘𝑤)”〉) = ((𝑤 substr 〈0, (𝑁 + 1)〉) ++ 〈“(
lastS ‘𝑤)”〉)) |
39 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑤) =
(𝑁 + 2) →
((#‘𝑤) − 1) =
((𝑁 + 2) −
1)) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) → ((#‘𝑤) − 1) = ((𝑁 + 2) − 1)) |
41 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
42 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℂ) |
43 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
44 | 41, 42, 43 | addsubassd 10291 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 2) − 1)
= (𝑁 + (2 −
1))) |
45 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2
− 1) = 1 |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (2 − 1) = 1) |
47 | 46 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + (2 − 1))
= (𝑁 + 1)) |
48 | 44, 47 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 2) − 1)
= (𝑁 + 1)) |
49 | 40, 48 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → ((#‘𝑤) − 1) = (𝑁 + 1)) |
50 | 49 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → 〈0, ((#‘𝑤) − 1)〉 = 〈0,
(𝑁 +
1)〉) |
51 | 50 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → (𝑤 substr 〈0, ((#‘𝑤) − 1)〉) = (𝑤 substr 〈0, (𝑁 + 1)〉)) |
52 | 51 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) =
((𝑤 substr 〈0, (𝑁 + 1)〉) ++ 〈“(
lastS ‘𝑤)”〉)) |
53 | | swrdccatwrd 13320 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word 𝑉 ∧ 𝑤 ≠ ∅) → ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) =
𝑤) |
54 | 9, 22, 53 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → ((𝑤 substr 〈0, ((#‘𝑤) − 1)〉) ++ 〈“( lastS
‘𝑤)”〉) =
𝑤) |
55 | 52, 54 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2))) → ((𝑤 substr 〈0, (𝑁 + 1)〉) ++ 〈“( lastS
‘𝑤)”〉) =
𝑤) |
56 | 55 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → ((𝑤 substr 〈0, (𝑁 + 1)〉) ++ 〈“( lastS
‘𝑤)”〉) =
𝑤) |
57 | 38, 56 | eqtr2d 2645 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → 𝑤 = (𝑊 ++ 〈“( lastS ‘𝑤)”〉)) |
58 | | simprrr 801 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) |
59 | | wwlknextbi 26253 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ ( lastS ‘𝑤)
∈ 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑤 = (𝑊 ++ 〈“( lastS ‘𝑤)”〉) ∧ {( lastS
‘𝑊), ( lastS
‘𝑤)} ∈ ran 𝐸)) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |
60 | 7, 25, 34, 57, 58, 59 | syl23anc 1325 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |
61 | 60 | exbiri 650 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
62 | 61 | com23 84 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
63 | 62 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
64 | 63 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
65 | 6, 64 | mpcom 37 |
. . . . . . . . 9
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) |
66 | 65 | expcomd 453 |
. . . . . . . 8
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) → ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) → 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
67 | 66 | imp 444 |
. . . . . . 7
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) → 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) |
68 | | wwlknimp 26215 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
69 | 41, 43, 43 | addassd 9941 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + (1 +
1))) |
70 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 + 1) =
2 |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (1 + 1) = 2) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + (1 + 1)) =
(𝑁 + 2)) |
73 | 69, 72 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + 2)) |
74 | 73 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ ((#‘𝑤) =
((𝑁 + 1) + 1) ↔
(#‘𝑤) = (𝑁 + 2))) |
75 | 74 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ ((#‘𝑤) =
((𝑁 + 1) + 1) →
(#‘𝑤) = (𝑁 + 2))) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → ((#‘𝑤) = ((𝑁 + 1) + 1) → (#‘𝑤) = (𝑁 + 2))) |
77 | 76 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) =
((𝑁 + 1) + 1) →
((𝑁 ∈
ℕ0 ∧ 𝑊
∈ Word 𝑉) →
(#‘𝑤) = (𝑁 + 2))) |
78 | 77 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((𝑁 + 1) + 1)) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉) → (#‘𝑤) = (𝑁 + 2))) |
79 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((𝑁 + 1) + 1)) → 𝑤 ∈ Word 𝑉) |
80 | 78, 79 | jctild 564 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((𝑁 + 1) + 1)) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)))) |
81 | 80 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)))) |
82 | 68, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)))) |
83 | 82 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)))) |
84 | 83 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)))) |
85 | 6, 84 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)))) |
86 | 85 | adantr 480 |
. . . . . . 7
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)))) |
87 | 67, 86 | impbid 201 |
. . . . . 6
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) → ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ↔ 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) |
88 | 87 | ex 449 |
. . . . 5
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) → ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ↔ 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))))) |
89 | 88 | pm5.32rd 670 |
. . . 4
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 2)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) ↔ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
90 | 5, 89 | syl5bb 271 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) ↔ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
91 | 90 | rabbidva2 3162 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
92 | 1, 91 | syl5eq 2656 |
1
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |