Step | Hyp | Ref
| Expression |
1 | | 2nn 11185 |
. . 3
⊢ 2 ∈
ℕ |
2 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2622 |
. . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
4 | 2, 3 | isclwwlksnx 26889 |
. . 3
⊢ (2 ∈
ℕ → (𝑊 ∈ (2
ClWWalksN 𝐺) ↔ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = 2))) |
5 | 1, 4 | ax-mp 5 |
. 2
⊢ (𝑊 ∈ (2 ClWWalksN 𝐺) ↔ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = 2)) |
6 | | 3anass 1042 |
. . . 4
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
7 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) = 2
→ ((#‘𝑊) −
1) = (2 − 1)) |
8 | | 2m1e1 11135 |
. . . . . . . . . . . . 13
⊢ (2
− 1) = 1 |
9 | 7, 8 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) = 2
→ ((#‘𝑊) −
1) = 1) |
10 | 9 | oveq2d 6666 |
. . . . . . . . . . 11
⊢
((#‘𝑊) = 2
→ (0..^((#‘𝑊)
− 1)) = (0..^1)) |
11 | | fzo01 12550 |
. . . . . . . . . . 11
⊢ (0..^1) =
{0} |
12 | 10, 11 | syl6eq 2672 |
. . . . . . . . . 10
⊢
((#‘𝑊) = 2
→ (0..^((#‘𝑊)
− 1)) = {0}) |
13 | 12 | adantr 481 |
. . . . . . . . 9
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
(0..^((#‘𝑊) −
1)) = {0}) |
14 | 13 | raleqdv 3144 |
. . . . . . . 8
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ {0} {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
15 | | c0ex 10034 |
. . . . . . . . 9
⊢ 0 ∈
V |
16 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 0 → (𝑊‘𝑖) = (𝑊‘0)) |
17 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
18 | | 0p1e1 11132 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
19 | 17, 18 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑖 = 0 → (𝑖 + 1) = 1) |
20 | 19 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑖 = 0 → (𝑊‘(𝑖 + 1)) = (𝑊‘1)) |
21 | 16, 20 | preq12d 4276 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘0), (𝑊‘1)}) |
22 | 21 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑖 = 0 → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) |
23 | 15, 22 | ralsn 4222 |
. . . . . . . 8
⊢
(∀𝑖 ∈
{0} {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) |
24 | 14, 23 | syl6bb 276 |
. . . . . . 7
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) |
25 | | prcom 4267 |
. . . . . . . . 9
⊢ {( lastS
‘𝑊), (𝑊‘0)} = {(𝑊‘0), ( lastS ‘𝑊)} |
26 | | lsw 13351 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
27 | 9 | fveq2d 6195 |
. . . . . . . . . . 11
⊢
((#‘𝑊) = 2
→ (𝑊‘((#‘𝑊) − 1)) = (𝑊‘1)) |
28 | 26, 27 | sylan9eqr 2678 |
. . . . . . . . . 10
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) → (
lastS ‘𝑊) = (𝑊‘1)) |
29 | 28 | preq2d 4275 |
. . . . . . . . 9
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
{(𝑊‘0), ( lastS
‘𝑊)} = {(𝑊‘0), (𝑊‘1)}) |
30 | 25, 29 | syl5eq 2668 |
. . . . . . . 8
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) → {(
lastS ‘𝑊), (𝑊‘0)} = {(𝑊‘0), (𝑊‘1)}) |
31 | 30 | eleq1d 2686 |
. . . . . . 7
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) → ({(
lastS ‘𝑊), (𝑊‘0)} ∈
(Edg‘𝐺) ↔
{(𝑊‘0), (𝑊‘1)} ∈
(Edg‘𝐺))) |
32 | 24, 31 | anbi12d 747 |
. . . . . 6
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
((∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ({(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) |
33 | | anidm 676 |
. . . . . 6
⊢ (({(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) |
34 | 32, 33 | syl6bb 276 |
. . . . 5
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
((∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) |
35 | 34 | pm5.32da 673 |
. . . 4
⊢
((#‘𝑊) = 2
→ ((𝑊 ∈ Word
(Vtx‘𝐺) ∧
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) ↔ (𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) |
36 | 6, 35 | syl5bb 272 |
. . 3
⊢
((#‘𝑊) = 2
→ ((𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) |
37 | 36 | pm5.32ri 670 |
. 2
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = 2) ↔ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = 2)) |
38 | | 3anass 1042 |
. . 3
⊢
(((#‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ↔ ((#‘𝑊) = 2 ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) |
39 | | ancom 466 |
. . 3
⊢
(((#‘𝑊) = 2
∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) ↔ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = 2)) |
40 | 38, 39 | bitr2i 265 |
. 2
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = 2) ↔ ((#‘𝑊) = 2 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) |
41 | 5, 37, 40 | 3bitri 286 |
1
⊢ (𝑊 ∈ (2 ClWWalksN 𝐺) ↔ ((#‘𝑊) = 2 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) |