Step | Hyp | Ref
| Expression |
1 | | df-clwwlks 26877 |
. . . 4
⊢ ClWWalks
= (𝑔 ∈ V ↦
{𝑤 ∈ Word
(Vtx‘𝑔) ∣
(𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐺 ∈ V → ClWWalks =
(𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})) |
3 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
4 | | clwwlks.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
5 | 3, 4 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) |
6 | | wrdeq 13327 |
. . . . . 6
⊢
((Vtx‘𝑔) =
𝑉 → Word
(Vtx‘𝑔) = Word 𝑉) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝑔 = 𝐺 → Word (Vtx‘𝑔) = Word 𝑉) |
8 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = (Edg‘𝐺)) |
9 | | clwwlks.e |
. . . . . . . . 9
⊢ 𝐸 = (Edg‘𝐺) |
10 | 8, 9 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = 𝐸) |
11 | 10 | eleq2d 2687 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ↔ {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸)) |
12 | 11 | ralbidv 2986 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ↔ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸)) |
13 | 10 | eleq2d 2687 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ({( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔) ↔ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
14 | 12, 13 | 3anbi23d 1402 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)) ↔ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸))) |
15 | 7, 14 | rabeqbidv 3195 |
. . . 4
⊢ (𝑔 = 𝐺 → {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))} = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
16 | 15 | adantl 482 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝑔 = 𝐺) → {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))} = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
17 | | id 22 |
. . 3
⊢ (𝐺 ∈ V → 𝐺 ∈ V) |
18 | | fvex 6201 |
. . . . . 6
⊢
(Vtx‘𝐺) ∈
V |
19 | 4, 18 | eqeltri 2697 |
. . . . 5
⊢ 𝑉 ∈ V |
20 | 19 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ V → 𝑉 ∈ V) |
21 | | wrdexg 13315 |
. . . 4
⊢ (𝑉 ∈ V → Word 𝑉 ∈ V) |
22 | | rabexg 4812 |
. . . 4
⊢ (Word
𝑉 ∈ V → {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)} ∈ V) |
23 | 20, 21, 22 | 3syl 18 |
. . 3
⊢ (𝐺 ∈ V → {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)} ∈ V) |
24 | 2, 16, 17, 23 | fvmptd 6288 |
. 2
⊢ (𝐺 ∈ V →
(ClWWalks‘𝐺) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
25 | | fvprc 6185 |
. . 3
⊢ (¬
𝐺 ∈ V →
(ClWWalks‘𝐺) =
∅) |
26 | | noel 3919 |
. . . . . . . 8
⊢ ¬ {(
lastS ‘𝑤), (𝑤‘0)} ∈
∅ |
27 | | fvprc 6185 |
. . . . . . . . . 10
⊢ (¬
𝐺 ∈ V →
(Edg‘𝐺) =
∅) |
28 | 9, 27 | syl5eq 2668 |
. . . . . . . . 9
⊢ (¬
𝐺 ∈ V → 𝐸 = ∅) |
29 | 28 | eleq2d 2687 |
. . . . . . . 8
⊢ (¬
𝐺 ∈ V → ({( lastS
‘𝑤), (𝑤‘0)} ∈ 𝐸 ↔ {( lastS ‘𝑤), (𝑤‘0)} ∈ ∅)) |
30 | 26, 29 | mtbiri 317 |
. . . . . . 7
⊢ (¬
𝐺 ∈ V → ¬ {(
lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸) |
31 | 30 | adantr 481 |
. . . . . 6
⊢ ((¬
𝐺 ∈ V ∧ 𝑤 ∈ Word 𝑉) → ¬ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸) |
32 | 31 | intn3an3d 1444 |
. . . . 5
⊢ ((¬
𝐺 ∈ V ∧ 𝑤 ∈ Word 𝑉) → ¬ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
33 | 32 | ralrimiva 2966 |
. . . 4
⊢ (¬
𝐺 ∈ V →
∀𝑤 ∈ Word 𝑉 ¬ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
34 | | rabeq0 3957 |
. . . 4
⊢ ({𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)} = ∅ ↔ ∀𝑤 ∈ Word 𝑉 ¬ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
35 | 33, 34 | sylibr 224 |
. . 3
⊢ (¬
𝐺 ∈ V → {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)} = ∅) |
36 | 25, 35 | eqtr4d 2659 |
. 2
⊢ (¬
𝐺 ∈ V →
(ClWWalks‘𝐺) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
37 | 24, 36 | pm2.61i 176 |
1
⊢
(ClWWalks‘𝐺) =
{𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ 𝐸)} |