Step | Hyp | Ref
| Expression |
1 | | wwlknprop 26214 |
. . . . 5
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉))) |
2 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
3 | | iswwlkn 26212 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 + 1) ∈
ℕ0) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)))) |
4 | 2, 3 | syl3an3 1353 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)))) |
5 | | wwlkprop 26213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑊 ∈ (𝑉 WWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉)) |
6 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
7 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) ↔
((𝑁 + 1) + 1) =
(#‘𝑊)) |
8 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℂ) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝑁
∈ ℕ0) → (#‘𝑊) ∈ ℂ) |
10 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝑁
∈ ℕ0) → 1 ∈ ℂ) |
11 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
12 | 2, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝑁
∈ ℕ0) → (𝑁 + 1) ∈ ℂ) |
14 | | subadd2 10164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝑊) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝑁 + 1) ∈ ℂ) →
(((#‘𝑊) − 1) =
(𝑁 + 1) ↔ ((𝑁 + 1) + 1) = (#‘𝑊))) |
15 | 14 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝑊) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝑁 + 1) ∈ ℂ) → (((𝑁 + 1) + 1) = (#‘𝑊) ↔ ((#‘𝑊) − 1) = (𝑁 + 1))) |
16 | 9, 10, 13, 15 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝑁
∈ ℕ0) → (((𝑁 + 1) + 1) = (#‘𝑊) ↔ ((#‘𝑊) − 1) = (𝑁 + 1))) |
17 | 7, 16 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝑁
∈ ℕ0) → ((#‘𝑊) = ((𝑁 + 1) + 1) ↔ ((#‘𝑊) − 1) = (𝑁 + 1))) |
18 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝑊)
− 1) = (𝑁 + 1) ↔
(𝑁 + 1) = ((#‘𝑊) − 1)) |
19 | 18 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝑊)
− 1) = (𝑁 + 1) →
(𝑁 + 1) = ((#‘𝑊) − 1)) |
20 | 17, 19 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝑁
∈ ℕ0) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 + 1) = ((#‘𝑊) − 1))) |
21 | 20 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑊) ∈
ℕ0 → (𝑁 ∈ ℕ0 →
((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 + 1) = ((#‘𝑊) − 1)))) |
22 | 21 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) = ((#‘𝑊) − 1)))) |
23 | 6, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑊 ∈ Word 𝑉 → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) = ((#‘𝑊) − 1)))) |
24 | 23 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) = ((#‘𝑊) − 1)))) |
25 | 5, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊 ∈ (𝑉 WWalks 𝐸) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) = ((#‘𝑊) − 1)))) |
26 | 25 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑁 + 1) = ((#‘𝑊) − 1))) |
27 | 26 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 + 1) = ((#‘𝑊) − 1))) |
28 | 27 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 + 1) = ((#‘𝑊) − 1))) |
29 | 28 | impcom 445 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) = ((#‘𝑊) − 1)) |
30 | 29 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)) →
〈0, (𝑁 + 1)〉 =
〈0, ((#‘𝑊)
− 1)〉) |
31 | 30 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)) → (𝑊 substr 〈0, (𝑁 + 1)〉) = (𝑊 substr 〈0, ((#‘𝑊) −
1)〉)) |
32 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ (𝑉 WWalks 𝐸)) |
33 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
34 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℝ |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
36 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
37 | 35, 36 | addge02d 10495 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (0 ≤ 𝑁 ↔ 2
≤ (𝑁 +
2))) |
38 | 33, 37 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 2 ≤ (𝑁 +
2)) |
39 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
40 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
41 | 39, 40, 40 | addassd 9941 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + (1 +
1))) |
42 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 + 1) =
2 |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ (1 + 1) = 2) |
44 | 43 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + (1 + 1)) =
(𝑁 + 2)) |
45 | 41, 44 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + 2)) |
46 | 38, 45 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ 2 ≤ ((𝑁 + 1) +
1)) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 2 ≤
((𝑁 + 1) +
1)) |
48 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) → (2
≤ (#‘𝑊) ↔ 2
≤ ((𝑁 + 1) +
1))) |
49 | 48 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (2 ≤
(#‘𝑊) ↔ 2 ≤
((𝑁 + 1) +
1))) |
50 | 47, 49 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 2 ≤
(#‘𝑊)) |
51 | 32, 50 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ 2 ≤ (#‘𝑊))) |
52 | 51 | 3ad2antr3 1221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)) → (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ 2 ≤ (#‘𝑊))) |
53 | | wwlkm1edg 26263 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ (𝑉 WWalks 𝐸)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈
(𝑉 WWalks 𝐸)) |
55 | 31, 54 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸)) |
56 | 55 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸))) |
57 | 4, 56 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸))) |
58 | 57 | 3expia 1259 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸)))) |
59 | 58 | com23 84 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸)))) |
60 | 59 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸))) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸))) |
62 | 61 | imp 444 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸)) |
63 | | wwlknimp 26215 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
64 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word 𝑉) |
65 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
66 | 2, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
67 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
68 | 36, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
69 | 68 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
70 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)) ↔ ((𝑁 + 1) ∈ ℕ0
∧ ((𝑁 + 1) + 1) ∈
ℕ0 ∧ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
71 | 2, 66, 69, 70 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
73 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
(0...(#‘𝑊)) =
(0...((𝑁 + 1) +
1))) |
74 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (0...(#‘𝑊)) =
(0...((𝑁 + 1) +
1))) |
75 | 72, 74 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...(#‘𝑊))) |
76 | 75 | adantll 746 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈ (0...(#‘𝑊))) |
77 | 64, 76 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))) |
78 | 77 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
79 | 78 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
80 | 63, 79 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
81 | 80 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
82 | 81 | imp 444 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))) |
83 | | swrd0len 13274 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)) |
84 | 82, 83 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑊 substr 〈0,
(𝑁 + 1)〉)) = (𝑁 + 1)) |
85 | 62, 84 | jca 553 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1))) |
86 | | iswwlkn 26212 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 substr 〈0,
(𝑁 + 1)〉) ∈
((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)))) |
87 | 86 | 3expia 1259 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ ℕ0
→ ((𝑊 substr 〈0,
(𝑁 + 1)〉) ∈
((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1))))) |
88 | 87 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (𝑁 ∈ ℕ0 → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1))))) |
89 | 88 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) → (𝑁 ∈ ℕ0 → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1))))) |
90 | 89 | imp 444 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)))) |
91 | 85, 90 | mpbird 246 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ (𝑊‘0) = 𝑃) ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
92 | 91 | exp41 636 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑊‘0) = 𝑃 → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))))) |
93 | 92 | adantr 480 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑊‘0) = 𝑃 → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))))) |
94 | 1, 93 | mpcom 37 |
. . . 4
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑊‘0) = 𝑃 → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))) |
95 | | wwlkextprop.x |
. . . 4
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) |
96 | 94, 95 | eleq2s 2706 |
. . 3
⊢ (𝑊 ∈ 𝑋 → ((𝑊‘0) = 𝑃 → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))) |
97 | 96 | 3imp 1249 |
. 2
⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
98 | 95 | wwlkextproplem1 26269 |
. . . 4
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) |
99 | 98 | 3adant2 1073 |
. . 3
⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) |
100 | | simp2 1055 |
. . 3
⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊‘0) = 𝑃) |
101 | 99, 100 | eqtrd 2644 |
. 2
⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃) |
102 | | fveq1 6102 |
. . . 4
⊢ (𝑤 = (𝑊 substr 〈0, (𝑁 + 1)〉) → (𝑤‘0) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0)) |
103 | 102 | eqeq1d 2612 |
. . 3
⊢ (𝑤 = (𝑊 substr 〈0, (𝑁 + 1)〉) → ((𝑤‘0) = 𝑃 ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
104 | | wwlkextprop.y |
. . 3
⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} |
105 | 103, 104 | elrab2 3333 |
. 2
⊢ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌 ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
106 | 97, 101, 105 | sylanbrc 695 |
1
⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌) |