Step | Hyp | Ref
| Expression |
1 | | wwlknredwwlkn 26254 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸))) |
2 | 1 | imp 444 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)) |
3 | | simpl 472 |
. . . . . . . . 9
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → (𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦) |
4 | 3 | adantl 481 |
. . . . . . . 8
⊢
(((((𝑊‘0) =
𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)) → (𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦) |
5 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑊 substr 〈0, (𝑁 + 1)〉) → (𝑦‘0) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0)) |
6 | 5 | eqcoms 2618 |
. . . . . . . . . . . . 13
⊢ ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 → (𝑦‘0) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0)) |
7 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) → (𝑦‘0) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0)) |
8 | | wwlknimp 26215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
9 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
10 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
11 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
12 | | lep1 10741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) ∈ ℝ →
(𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
14 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
15 | 14 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℤ) |
16 | | fznn 12278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 + 1) + 1) ∈ ℤ →
((𝑁 + 1) ∈
(1...((𝑁 + 1) + 1)) ↔
((𝑁 + 1) ∈ ℕ
∧ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)))) |
17 | 10, 15, 16 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) ∈
(1...((𝑁 + 1) + 1)) ↔
((𝑁 + 1) ∈ ℕ
∧ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)))) |
18 | 9, 13, 17 | mpbir2and 959 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(1...((𝑁 + 1) +
1))) |
19 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
(1...(#‘𝑊)) =
(1...((𝑁 + 1) +
1))) |
20 | 19 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ∈
(1...(#‘𝑊)) ↔
(𝑁 + 1) ∈ (1...((𝑁 + 1) + 1)))) |
21 | 18, 20 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(1...(#‘𝑊)))) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
23 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → 𝑊 ∈ Word 𝑉) |
24 | 22, 23 | jctild 564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))))) |
25 | 24 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))))) |
26 | 8, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))))) |
27 | 26 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
31 | | swrd0fv0 13292 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) |
33 | | simprll 798 |
. . . . . . . . . . . 12
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) → (𝑊‘0) = 𝑃) |
34 | 7, 32, 33 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) → (𝑦‘0) = 𝑃) |
35 | 34 | ex 449 |
. . . . . . . . . 10
⊢ ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 → ((((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → (𝑦‘0) = 𝑃)) |
36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → ((((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → (𝑦‘0) = 𝑃)) |
37 | 36 | impcom 445 |
. . . . . . . 8
⊢
(((((𝑊‘0) =
𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)) → (𝑦‘0) = 𝑃) |
38 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) |
39 | 38 | adantl 481 |
. . . . . . . 8
⊢
(((((𝑊‘0) =
𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)) → {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) |
40 | 4, 37, 39 | 3jca 1235 |
. . . . . . 7
⊢
(((((𝑊‘0) =
𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) ∧ ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)) → ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)) |
41 | 40 | ex 449 |
. . . . . 6
⊢ ((((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸))) |
42 | 41 | reximdva 3000 |
. . . . 5
⊢ (((𝑊‘0) = 𝑃 ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) → (∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸))) |
43 | 42 | ex 449 |
. . . 4
⊢ ((𝑊‘0) = 𝑃 → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)))) |
44 | 43 | com13 86 |
. . 3
⊢
(∃𝑦 ∈
((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑊‘0) = 𝑃 → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)))) |
45 | 2, 44 | mpcom 37 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑊‘0) = 𝑃 → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸))) |
46 | 27, 31 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) |
47 | 46 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (𝑊‘0) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0)) |
48 | 47 | adantl 481 |
. . . . . . 7
⊢ ((((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) → (𝑊‘0) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0)) |
49 | | fveq1 6102 |
. . . . . . . . 9
⊢ ((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑦‘0)) |
50 | 49 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑦‘0)) |
51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑦‘0)) |
52 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) → (𝑦‘0) = 𝑃) |
53 | 52 | adantr 480 |
. . . . . . 7
⊢ ((((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) → (𝑦‘0) = 𝑃) |
54 | 48, 51, 53 | 3eqtrd 2648 |
. . . . . 6
⊢ ((((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) → (𝑊‘0) = 𝑃) |
55 | 54 | ex 449 |
. . . . 5
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (𝑊‘0) = 𝑃)) |
56 | 55 | 3adant3 1074 |
. . . 4
⊢ (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (𝑊‘0) = 𝑃)) |
57 | 56 | com12 32 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → (𝑊‘0) = 𝑃)) |
58 | 57 | rexlimdvw 3016 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸) → (𝑊‘0) = 𝑃)) |
59 | 45, 58 | impbid 201 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑊‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸))) |