| Step | Hyp | Ref
| Expression |
| 1 | | df-clwwlk 30001 |
. . 3
⊢ ClWWalks
= (𝑔 ∈ V ↦
{𝑤 ∈ Word
(Vtx‘𝑔) ∣
(𝑤 ≠ ∅ ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
| 3 | | clwwlk.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) |
| 5 | | wrdeq 14574 |
. . . . 5
⊢
((Vtx‘𝑔) =
𝑉 → Word
(Vtx‘𝑔) = Word 𝑉) |
| 6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝑔 = 𝐺 → Word (Vtx‘𝑔) = Word 𝑉) |
| 7 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = (Edg‘𝐺)) |
| 8 | | clwwlk.e |
. . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) |
| 9 | 7, 8 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = 𝐸) |
| 10 | 9 | eleq2d 2827 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ↔ {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸)) |
| 11 | 10 | ralbidv 3178 |
. . . . 5
⊢ (𝑔 = 𝐺 → (∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ↔ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸)) |
| 12 | 9 | eleq2d 2827 |
. . . . 5
⊢ (𝑔 = 𝐺 → ({(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔) ↔ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
| 13 | 11, 12 | 3anbi23d 1441 |
. . . 4
⊢ (𝑔 = 𝐺 → ((𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)) ↔ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸))) |
| 14 | 6, 13 | rabeqbidv 3455 |
. . 3
⊢ (𝑔 = 𝐺 → {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))} = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
| 15 | | id 22 |
. . 3
⊢ (𝐺 ∈ V → 𝐺 ∈ V) |
| 16 | 3 | fvexi 6920 |
. . . . 5
⊢ 𝑉 ∈ V |
| 17 | 16 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ V → 𝑉 ∈ V) |
| 18 | | wrdexg 14562 |
. . . 4
⊢ (𝑉 ∈ V → Word 𝑉 ∈ V) |
| 19 | | rabexg 5337 |
. . . 4
⊢ (Word
𝑉 ∈ V → {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)} ∈ V) |
| 20 | 17, 18, 19 | 3syl 18 |
. . 3
⊢ (𝐺 ∈ V → {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)} ∈ V) |
| 21 | 1, 14, 15, 20 | fvmptd3 7039 |
. 2
⊢ (𝐺 ∈ V →
(ClWWalks‘𝐺) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
| 22 | | fvprc 6898 |
. . 3
⊢ (¬
𝐺 ∈ V →
(ClWWalks‘𝐺) =
∅) |
| 23 | | noel 4338 |
. . . . . . . 8
⊢ ¬
{(lastS‘𝑤), (𝑤‘0)} ∈
∅ |
| 24 | | fvprc 6898 |
. . . . . . . . . 10
⊢ (¬
𝐺 ∈ V →
(Edg‘𝐺) =
∅) |
| 25 | 8, 24 | eqtrid 2789 |
. . . . . . . . 9
⊢ (¬
𝐺 ∈ V → 𝐸 = ∅) |
| 26 | 25 | eleq2d 2827 |
. . . . . . . 8
⊢ (¬
𝐺 ∈ V →
({(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸 ↔ {(lastS‘𝑤), (𝑤‘0)} ∈ ∅)) |
| 27 | 23, 26 | mtbiri 327 |
. . . . . . 7
⊢ (¬
𝐺 ∈ V → ¬
{(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸) |
| 28 | 27 | adantr 480 |
. . . . . 6
⊢ ((¬
𝐺 ∈ V ∧ 𝑤 ∈ Word 𝑉) → ¬ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸) |
| 29 | 28 | intn3an3d 1483 |
. . . . 5
⊢ ((¬
𝐺 ∈ V ∧ 𝑤 ∈ Word 𝑉) → ¬ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
| 30 | 29 | ralrimiva 3146 |
. . . 4
⊢ (¬
𝐺 ∈ V →
∀𝑤 ∈ Word 𝑉 ¬ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
| 31 | | rabeq0 4388 |
. . . 4
⊢ ({𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)} = ∅ ↔ ∀𝑤 ∈ Word 𝑉 ¬ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)) |
| 32 | 30, 31 | sylibr 234 |
. . 3
⊢ (¬
𝐺 ∈ V → {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)} = ∅) |
| 33 | 22, 32 | eqtr4d 2780 |
. 2
⊢ (¬
𝐺 ∈ V →
(ClWWalks‘𝐺) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)}) |
| 34 | 21, 33 | pm2.61i 182 |
1
⊢
(ClWWalks‘𝐺) =
{𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)} |