Step | Hyp | Ref
| Expression |
1 | | wlkcpr 26057 |
. . . . 5
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) ↔ (1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊)) |
2 | | wlkn0 26055 |
. . . . 5
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → (2nd ‘𝑊) ≠ ∅) |
3 | 1, 2 | sylbi 206 |
. . . 4
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → (2nd ‘𝑊) ≠ ∅) |
4 | | wlkelwrd 26058 |
. . . . 5
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → ((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉)) |
5 | | ffz0iswrd 13187 |
. . . . . 6
⊢
((2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉 → (2nd ‘𝑊) ∈ Word 𝑉) |
6 | 5 | adantl 481 |
. . . . 5
⊢
(((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉) → (2nd
‘𝑊) ∈ Word 𝑉) |
7 | 4, 6 | syl 17 |
. . . 4
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → (2nd ‘𝑊) ∈ Word 𝑉) |
8 | | edgwlk 26059 |
. . . . . 6
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → ∀𝑖 ∈ (0..^(#‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸) |
9 | | wlklenvm1 26060 |
. . . . . . . 8
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → (#‘(1st
‘𝑊)) =
((#‘(2nd ‘𝑊)) − 1)) |
10 | 9 | oveq2d 6565 |
. . . . . . 7
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → (0..^(#‘(1st
‘𝑊))) =
(0..^((#‘(2nd ‘𝑊)) − 1))) |
11 | 10 | raleqdv 3121 |
. . . . . 6
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → (∀𝑖 ∈ (0..^(#‘(1st
‘𝑊))){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸)) |
12 | 8, 11 | mpbid 221 |
. . . . 5
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸) |
13 | 1, 12 | sylbi 206 |
. . . 4
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸) |
14 | 3, 7, 13 | 3jca 1235 |
. . 3
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → ((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word 𝑉 ∧
∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸)) |
15 | 14 | ad2antrl 760 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → ((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸)) |
16 | | id 22 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
17 | | oveq2 6557 |
. . . . . . . . . . 11
⊢
((#‘(1st ‘𝑊)) = 𝑁 → (0...(#‘(1st
‘𝑊))) = (0...𝑁)) |
18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢
(((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (#‘(1st ‘𝑊)) = 𝑁) → (0...(#‘(1st
‘𝑊))) = (0...𝑁)) |
19 | 18 | feq2d 5944 |
. . . . . . . . 9
⊢
(((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (#‘(1st ‘𝑊)) = 𝑁) → ((2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉 ↔ (2nd
‘𝑊):(0...𝑁)⟶𝑉)) |
20 | 19 | biimpd 218 |
. . . . . . . 8
⊢
(((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (#‘(1st ‘𝑊)) = 𝑁) → ((2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉 → (2nd
‘𝑊):(0...𝑁)⟶𝑉)) |
21 | 20 | impancom 455 |
. . . . . . 7
⊢
(((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉) →
((#‘(1st ‘𝑊)) = 𝑁 → (2nd ‘𝑊):(0...𝑁)⟶𝑉)) |
22 | 21 | imp 444 |
. . . . . 6
⊢
((((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉) ∧ (#‘(1st
‘𝑊)) = 𝑁) → (2nd
‘𝑊):(0...𝑁)⟶𝑉) |
23 | | ffz0hash 13088 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (2nd ‘𝑊):(0...𝑁)⟶𝑉) → (#‘(2nd
‘𝑊)) = (𝑁 + 1)) |
24 | 16, 22, 23 | syl2anr 494 |
. . . . 5
⊢
(((((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉) ∧ (#‘(1st
‘𝑊)) = 𝑁) ∧ 𝑁 ∈ ℕ0) →
(#‘(2nd ‘𝑊)) = (𝑁 + 1)) |
25 | 24 | ex 449 |
. . . 4
⊢
((((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉) ∧ (#‘(1st
‘𝑊)) = 𝑁) → (𝑁 ∈ ℕ0 →
(#‘(2nd ‘𝑊)) = (𝑁 + 1))) |
26 | 4, 25 | sylan 487 |
. . 3
⊢ ((𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁) → (𝑁 ∈ ℕ0 →
(#‘(2nd ‘𝑊)) = (𝑁 + 1))) |
27 | 26 | impcom 445 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) →
(#‘(2nd ‘𝑊)) = (𝑁 + 1)) |
28 | | wlkbprop 26051 |
. . . . . . . 8
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → ((#‘(1st
‘𝑊)) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((1st
‘𝑊) ∈ V ∧
(2nd ‘𝑊)
∈ V))) |
29 | 28 | simp2d 1067 |
. . . . . . 7
⊢
((1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
30 | 1, 29 | sylbi 206 |
. . . . . 6
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
31 | | simpll 786 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ 𝑉 ∈
V) |
32 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝐸 ∈ V) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ 𝐸 ∈
V) |
34 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
35 | 31, 33, 34 | 3jca 1235 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (𝑉 ∈ V ∧
𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
36 | 35 | ex 449 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ ℕ0
→ (𝑉 ∈ V ∧
𝐸 ∈ V ∧ 𝑁 ∈
ℕ0))) |
37 | 30, 36 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → (𝑁 ∈ ℕ0 → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0))) |
38 | 37 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁) → (𝑁 ∈ ℕ0 → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0))) |
39 | 38 | impcom 445 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
40 | | iswwlkn 26212 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((2nd ‘𝑊) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((2nd ‘𝑊) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
41 | | iswwlk 26211 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) →
((2nd ‘𝑊)
∈ (𝑉 WWalks 𝐸) ↔ ((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸))) |
42 | 41 | 3adant3 1074 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((2nd ‘𝑊) ∈ (𝑉 WWalks 𝐸) ↔ ((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word 𝑉 ∧
∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸))) |
43 | 42 | anbi1d 737 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (((2nd ‘𝑊) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)) ↔ (((2nd
‘𝑊) ≠ ∅
∧ (2nd ‘𝑊) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(2nd
‘𝑊)) −
1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
44 | 40, 43 | bitrd 267 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((2nd ‘𝑊) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word 𝑉 ∧
∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
45 | 39, 44 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → ((2nd
‘𝑊) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (((2nd ‘𝑊) ≠ ∅ ∧
(2nd ‘𝑊)
∈ Word 𝑉 ∧
∀𝑖 ∈
(0..^((#‘(2nd ‘𝑊)) − 1)){((2nd ‘𝑊)‘𝑖), ((2nd ‘𝑊)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(2nd
‘𝑊)) = (𝑁 + 1)))) |
46 | 15, 27, 45 | mpbir2and 959 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → (2nd
‘𝑊) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |