Step | Hyp | Ref
| Expression |
1 | | 0nn0 11184 |
. . 3
⊢ 0 ∈
ℕ0 |
2 | | wwlkn 26210 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 0 ∈ ℕ0) →
((𝑉 WWalksN 𝐸)‘0) = {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (0 + 1)}) |
3 | 1, 2 | mp3an3 1405 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 WWalksN 𝐸)‘0) = {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (0 + 1)}) |
4 | | 0p1e1 11009 |
. . . . . 6
⊢ (0 + 1) =
1 |
5 | 4 | eqeq2i 2622 |
. . . . 5
⊢
((#‘𝑤) = (0 +
1) ↔ (#‘𝑤) =
1) |
6 | 5 | anbi2i 726 |
. . . 4
⊢ ((𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (0 + 1)) ↔ (𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = 1)) |
7 | | iswwlk 26211 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
9 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → 𝑤 ∈ Word 𝑉) |
10 | | ax-1ne0 9884 |
. . . . . . . . . . . . 13
⊢ 1 ≠
0 |
11 | | pm13.181 2864 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑤) = 1
∧ 1 ≠ 0) → (#‘𝑤) ≠ 0) |
12 | 10, 11 | mpan2 703 |
. . . . . . . . . . . 12
⊢
((#‘𝑤) = 1
→ (#‘𝑤) ≠
0) |
13 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑤 ∈ V |
14 | | hasheq0 13015 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ V → ((#‘𝑤) = 0 ↔ 𝑤 = ∅)) |
15 | 13, 14 | mp1i 13 |
. . . . . . . . . . . . 13
⊢
((#‘𝑤) = 1
→ ((#‘𝑤) = 0
↔ 𝑤 =
∅)) |
16 | 15 | necon3bid 2826 |
. . . . . . . . . . . 12
⊢
((#‘𝑤) = 1
→ ((#‘𝑤) ≠ 0
↔ 𝑤 ≠
∅)) |
17 | 12, 16 | mpbid 221 |
. . . . . . . . . . 11
⊢
((#‘𝑤) = 1
→ 𝑤 ≠
∅) |
18 | 17 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) ∧ 𝑤 ∈ Word 𝑉) → 𝑤 ≠ ∅) |
19 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) ∧ 𝑤 ∈ Word 𝑉) → 𝑤 ∈ Word 𝑉) |
20 | | ral0 4028 |
. . . . . . . . . . . 12
⊢
∀𝑖 ∈
∅ {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 |
21 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 1
→ ((#‘𝑤) −
1) = (1 − 1)) |
22 | | 1m1e0 10966 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
23 | 21, 22 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 1
→ ((#‘𝑤) −
1) = 0) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑤) = 1
→ (0..^((#‘𝑤)
− 1)) = (0..^0)) |
25 | | fzo0 12361 |
. . . . . . . . . . . . . 14
⊢ (0..^0) =
∅ |
26 | 24, 25 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢
((#‘𝑤) = 1
→ (0..^((#‘𝑤)
− 1)) = ∅) |
27 | 26 | raleqdv 3121 |
. . . . . . . . . . . 12
⊢
((#‘𝑤) = 1
→ (∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ ∅ {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
28 | 20, 27 | mpbiri 247 |
. . . . . . . . . . 11
⊢
((#‘𝑤) = 1
→ ∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) |
29 | 28 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) ∧ 𝑤 ∈ Word 𝑉) → ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) |
30 | 18, 19, 29 | 3jca 1235 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) ∧ 𝑤 ∈ Word 𝑉) → (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
31 | 30 | ex 449 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) → (𝑤 ∈ Word 𝑉 → (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))) |
32 | 9, 31 | impbid2 215 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ↔ 𝑤 ∈ Word 𝑉)) |
33 | 8, 32 | bitrd 267 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (#‘𝑤) = 1) → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ 𝑤 ∈ Word 𝑉)) |
34 | 33 | ex 449 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((#‘𝑤) = 1 → (𝑤 ∈ (𝑉 WWalks 𝐸) ↔ 𝑤 ∈ Word 𝑉))) |
35 | 34 | pm5.32rd 670 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = 1) ↔ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1))) |
36 | 6, 35 | syl5bb 271 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑤 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑤) = (0 + 1)) ↔ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1))) |
37 | 36 | rabbidva2 3162 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (0 + 1)} = {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1}) |
38 | 3, 37 | eqtrd 2644 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 WWalksN 𝐸)‘0) = {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1}) |