Step | Hyp | Ref
| Expression |
1 | | neeq1 2856 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑤 ≠ ∅ ↔ 𝑊 ≠ ∅)) |
2 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (#‘𝑤) = (#‘𝑊)) |
3 | 2 | oveq1d 6665 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((#‘𝑤) − 1) = ((#‘𝑊) − 1)) |
4 | 3 | oveq2d 6666 |
. . . . 5
⊢ (𝑤 = 𝑊 → (0..^((#‘𝑤) − 1)) = (0..^((#‘𝑊) − 1))) |
5 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑤‘𝑖) = (𝑊‘𝑖)) |
6 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑤‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
7 | 5, 6 | preq12d 4276 |
. . . . . 6
⊢ (𝑤 = 𝑊 → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}) |
8 | 7 | eleq1d 2686 |
. . . . 5
⊢ (𝑤 = 𝑊 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
9 | 4, 8 | raleqbidv 3152 |
. . . 4
⊢ (𝑤 = 𝑊 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
10 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ( lastS ‘𝑤) = ( lastS ‘𝑊)) |
11 | | fveq1 6190 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑤‘0) = (𝑊‘0)) |
12 | 10, 11 | preq12d 4276 |
. . . . 5
⊢ (𝑤 = 𝑊 → {( lastS ‘𝑤), (𝑤‘0)} = {( lastS ‘𝑊), (𝑊‘0)}) |
13 | 12 | eleq1d 2686 |
. . . 4
⊢ (𝑤 = 𝑊 → ({( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸 ↔ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) |
14 | 1, 9, 13 | 3anbi123d 1399 |
. . 3
⊢ (𝑤 = 𝑊 → ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸) ↔ (𝑊 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
15 | 14 | elrab 3363 |
. 2
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)} ↔ (𝑊 ∈ Word 𝑉 ∧ (𝑊 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
16 | | clwwlks.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
17 | | clwwlks.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
18 | 16, 17 | clwwlks 26879 |
. . 3
⊢
(ClWWalks‘𝐺) =
{𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)} |
19 | 18 | eleq2i 2693 |
. 2
⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ 𝑊 ∈ {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
20 | | 3anass 1042 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
21 | | anass 681 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ↔ (𝑊 ∈ Word 𝑉 ∧ (𝑊 ≠ ∅ ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)))) |
22 | | 3anass 1042 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ↔ (𝑊 ≠ ∅ ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
23 | 22 | bicomi 214 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ↔ (𝑊 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) |
24 | 23 | anbi2i 730 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 ≠ ∅ ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) ↔ (𝑊 ∈ Word 𝑉 ∧ (𝑊 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
25 | 20, 21, 24 | 3bitri 286 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ (𝑊 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸))) |
26 | 15, 19, 25 | 3bitr4i 292 |
1
⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) |