Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | 2nn0 11186 |
. . . . 5
⊢ 2 ∈
ℕ0 |
3 | | isclwwlkn 26297 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 2 ∈
ℕ0) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘2) ↔ (𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 2))) |
4 | 2, 3 | mp3an3 1405 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘2) ↔ (𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 2))) |
5 | | isclwwlk 26296 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
6 | 5 | anbi1d 737 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 2) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2))) |
7 | 4, 6 | bitrd 267 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘2) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2))) |
8 | 1, 7 | syl 17 |
. 2
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘2) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2))) |
9 | | 3anass 1035 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
10 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) = 2
→ ((#‘𝑊) −
1) = (2 − 1)) |
11 | 10 | oveq2d 6565 |
. . . . . . . . . . 11
⊢
((#‘𝑊) = 2
→ (0..^((#‘𝑊)
− 1)) = (0..^(2 − 1))) |
12 | 11 | raleqdv 3121 |
. . . . . . . . . 10
⊢
((#‘𝑊) = 2
→ (∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(2 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
13 | 12 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(2 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
14 | | 2m1e1 11012 |
. . . . . . . . . . . . 13
⊢ (2
− 1) = 1 |
15 | 14 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢ (0..^(2
− 1)) = (0..^1) |
16 | | fzo01 12417 |
. . . . . . . . . . . 12
⊢ (0..^1) =
{0} |
17 | 15, 16 | eqtri 2632 |
. . . . . . . . . . 11
⊢ (0..^(2
− 1)) = {0} |
18 | 17 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → (0..^(2 − 1)) =
{0}) |
19 | 18 | raleqdv 3121 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^(2 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ {0} {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
20 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
21 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → (𝑊‘𝑖) = (𝑊‘0)) |
22 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
23 | | 0p1e1 11009 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
24 | 22, 23 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 0 → (𝑖 + 1) = 1) |
25 | 24 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → (𝑊‘(𝑖 + 1)) = (𝑊‘1)) |
26 | 21, 25 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ (𝑖 = 0 → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘0), (𝑊‘1)}) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑖 = 0 → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)) |
28 | 27 | ralsng 4165 |
. . . . . . . . . 10
⊢ (0 ∈
V → (∀𝑖 ∈
{0} {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)) |
29 | 20, 28 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → (∀𝑖 ∈ {0} {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)) |
30 | 13, 19, 29 | 3bitrd 293 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)) |
31 | 30 | anbi1d 737 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ↔ ({(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
32 | | lsw 13204 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
34 | 10 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ((#‘𝑊) − 1) = (2 −
1)) |
35 | 34, 14 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ((#‘𝑊) − 1) = 1) |
36 | 35 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘((#‘𝑊) − 1)) = (𝑊‘1)) |
37 | 33, 36 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘1) = ( lastS ‘𝑊)) |
38 | 37 | preq2d 4219 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → {(𝑊‘0), (𝑊‘1)} = {(𝑊‘0), ( lastS ‘𝑊)}) |
39 | | prcom 4211 |
. . . . . . . . . . 11
⊢ {(𝑊‘0), ( lastS ‘𝑊)} = {( lastS ‘𝑊), (𝑊‘0)} |
40 | 38, 39 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → {(𝑊‘0), (𝑊‘1)} = {( lastS ‘𝑊), (𝑊‘0)}) |
41 | 40 | eleq1d 2672 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ({(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) |
42 | 41 | biimpd 218 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ({(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸 → {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) |
43 | 42 | pm4.71d 664 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ({(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸 ↔ ({(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
44 | 31, 43 | bitr4d 270 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) ∧ 𝑊 ∈ Word 𝑉) → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ↔ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)) |
45 | 44 | pm5.32da 671 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) → ((𝑊 ∈ Word 𝑉 ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) ↔ (𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸))) |
46 | 9, 45 | syl5bb 271 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑊) = 2) → ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸))) |
47 | 46 | ex 449 |
. . 3
⊢ (𝑉 USGrph 𝐸 → ((#‘𝑊) = 2 → ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)))) |
48 | 47 | pm5.32rd 670 |
. 2
⊢ (𝑉 USGrph 𝐸 → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2) ↔ ((𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2))) |
49 | | 3anass 1035 |
. . . 4
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸) ↔ ((#‘𝑊) = 2 ∧ (𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸))) |
50 | | ancom 465 |
. . . 4
⊢
(((#‘𝑊) = 2
∧ (𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)) ↔ ((𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2)) |
51 | 49, 50 | bitr2i 264 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2) ↔ ((#‘𝑊) = 2 ∧ 𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸)) |
52 | 51 | a1i 11 |
. 2
⊢ (𝑉 USGrph 𝐸 → (((𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸) ∧ (#‘𝑊) = 2) ↔ ((#‘𝑊) = 2 ∧ 𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸))) |
53 | 8, 48, 52 | 3bitrd 293 |
1
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘2) ↔ ((#‘𝑊) = 2 ∧ 𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸))) |