| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2nn 12339 | . . 3
⊢ 2 ∈
ℕ | 
| 2 |  | eqid 2737 | . . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 3 |  | eqid 2737 | . . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 4 | 2, 3 | isclwwlknx 30055 | . . 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 1095 | . . . 4
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))) | 
| 7 |  | oveq1 7438 | . . . . . . . . . . . . 13
⊢
((♯‘𝑊) =
2 → ((♯‘𝑊)
− 1) = (2 − 1)) | 
| 8 |  | 2m1e1 12392 | . . . . . . . . . . . . 13
⊢ (2
− 1) = 1 | 
| 9 | 7, 8 | eqtrdi 2793 | . . . . . . . . . . . 12
⊢
((♯‘𝑊) =
2 → ((♯‘𝑊)
− 1) = 1) | 
| 10 | 9 | oveq2d 7447 | . . . . . . . . . . 11
⊢
((♯‘𝑊) =
2 → (0..^((♯‘𝑊) − 1)) = (0..^1)) | 
| 11 |  | fzo01 13786 | . . . . . . . . . . 11
⊢ (0..^1) =
{0} | 
| 12 | 10, 11 | eqtrdi 2793 | . . . . . . . . . 10
⊢
((♯‘𝑊) =
2 → (0..^((♯‘𝑊) − 1)) = {0}) | 
| 13 | 12 | adantr 480 | . . . . . . . . 9
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
(0..^((♯‘𝑊)
− 1)) = {0}) | 
| 14 | 13 | raleqdv 3326 | . . . . . . . 8
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ {0} {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 15 |  | c0ex 11255 | . . . . . . . . 9
⊢ 0 ∈
V | 
| 16 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑖 = 0 → (𝑊‘𝑖) = (𝑊‘0)) | 
| 17 |  | fv0p1e1 12389 | . . . . . . . . . . 11
⊢ (𝑖 = 0 → (𝑊‘(𝑖 + 1)) = (𝑊‘1)) | 
| 18 | 16, 17 | preq12d 4741 | . . . . . . . . . 10
⊢ (𝑖 = 0 → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘0), (𝑊‘1)}) | 
| 19 | 18 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑖 = 0 → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) | 
| 20 | 15, 19 | ralsn 4681 | . . . . . . . 8
⊢
(∀𝑖 ∈
{0} {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) | 
| 21 | 14, 20 | bitrdi 287 | . . . . . . 7
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) | 
| 22 |  | prcom 4732 | . . . . . . . . 9
⊢
{(lastS‘𝑊),
(𝑊‘0)} = {(𝑊‘0), (lastS‘𝑊)} | 
| 23 |  | lsw 14602 | . . . . . . . . . . 11
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) | 
| 24 | 9 | fveq2d 6910 | . . . . . . . . . . 11
⊢
((♯‘𝑊) =
2 → (𝑊‘((♯‘𝑊) − 1)) = (𝑊‘1)) | 
| 25 | 23, 24 | sylan9eqr 2799 | . . . . . . . . . 10
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
(lastS‘𝑊) = (𝑊‘1)) | 
| 26 | 25 | preq2d 4740 | . . . . . . . . 9
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
{(𝑊‘0),
(lastS‘𝑊)} = {(𝑊‘0), (𝑊‘1)}) | 
| 27 | 22, 26 | eqtrid 2789 | . . . . . . . 8
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
{(lastS‘𝑊), (𝑊‘0)} = {(𝑊‘0), (𝑊‘1)}) | 
| 28 | 27 | eleq1d 2826 | . . . . . . 7
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
({(lastS‘𝑊), (𝑊‘0)} ∈
(Edg‘𝐺) ↔
{(𝑊‘0), (𝑊‘1)} ∈
(Edg‘𝐺))) | 
| 29 | 21, 28 | anbi12d 632 | . . . . . 6
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
((∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ({(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) | 
| 30 |  | anidm 564 | . . . . . 6
⊢ (({(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) | 
| 31 | 29, 30 | bitrdi 287 | . . . . 5
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺)) →
((∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) | 
| 32 | 31 | pm5.32da 579 | . . . 4
⊢
((♯‘𝑊) =
2 → ((𝑊 ∈ Word
(Vtx‘𝐺) ∧
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) ↔ (𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) | 
| 33 | 6, 32 | bitrid 283 | . . 3
⊢
((♯‘𝑊) =
2 → ((𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) | 
| 34 | 33 | pm5.32ri 575 | . 2
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = 2) ↔ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = 2)) | 
| 35 |  | 3anass 1095 | . . 3
⊢
(((♯‘𝑊)
= 2 ∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ↔ ((♯‘𝑊) = 2 ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)))) | 
| 36 |  | ancom 460 | . . 3
⊢
(((♯‘𝑊)
= 2 ∧ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) ↔ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = 2)) | 
| 37 | 35, 36 | bitr2i 276 | . 2
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = 2) ↔
((♯‘𝑊) = 2
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) | 
| 38 | 5, 34, 37 | 3bitri 297 | 1
⊢ (𝑊 ∈ (2 ClWWalksN 𝐺) ↔ ((♯‘𝑊) = 2 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) |