| Step | Hyp | Ref
| Expression |
| 1 | | eliun 4995 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁) ↔ ∃𝑥 ∈ 𝑉 𝑦 ∈ (𝑥(ClWWalksNOn‘𝐺)𝑁)) |
| 2 | | isclwwlknon 30110 |
. . . . 5
⊢ (𝑦 ∈ (𝑥(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥)) |
| 3 | 2 | rexbii 3094 |
. . . 4
⊢
(∃𝑥 ∈
𝑉 𝑦 ∈ (𝑥(ClWWalksNOn‘𝐺)𝑁) ↔ ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥)) |
| 4 | | simpl 482 |
. . . . . 6
⊢ ((𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥) → 𝑦 ∈ (𝑁 ClWWalksN 𝐺)) |
| 5 | 4 | rexlimivw 3151 |
. . . . 5
⊢
(∃𝑥 ∈
𝑉 (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥) → 𝑦 ∈ (𝑁 ClWWalksN 𝐺)) |
| 6 | | clwwlknun.v |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
| 7 | | eqid 2737 |
. . . . . . . . 9
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 8 | 6, 7 | clwwlknp 30056 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) |
| 9 | 8 | anim2i 617 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑦 ∈ (𝑁 ClWWalksN 𝐺)) → (𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺)))) |
| 10 | 7, 6 | usgrpredgv 29214 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧
{(lastS‘𝑦), (𝑦‘0)} ∈
(Edg‘𝐺)) →
((lastS‘𝑦) ∈
𝑉 ∧ (𝑦‘0) ∈ 𝑉)) |
| 11 | 10 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph →
({(lastS‘𝑦), (𝑦‘0)} ∈
(Edg‘𝐺) →
((lastS‘𝑦) ∈
𝑉 ∧ (𝑦‘0) ∈ 𝑉))) |
| 12 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((lastS‘𝑦)
∈ 𝑉 ∧ (𝑦‘0) ∈ 𝑉) → (𝑦‘0) ∈ 𝑉) |
| 13 | 11, 12 | syl6com 37 |
. . . . . . . . . . 11
⊢
({(lastS‘𝑦),
(𝑦‘0)} ∈
(Edg‘𝐺) → (𝐺 ∈ USGraph → (𝑦‘0) ∈ 𝑉)) |
| 14 | 13 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺)) → (𝐺 ∈ USGraph → (𝑦‘0) ∈ 𝑉)) |
| 15 | 14 | impcom 407 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) → (𝑦‘0) ∈ 𝑉) |
| 16 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → 𝑥 = (𝑦‘0)) |
| 17 | 16 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → (𝑦‘0) = 𝑥) |
| 18 | 17 | biantrud 531 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ↔ (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
| 19 | 18 | bicomd 223 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → ((𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥) ↔ 𝑦 ∈ (𝑁 ClWWalksN 𝐺))) |
| 20 | 15, 19 | rspcedv 3615 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) → (𝑦 ∈ (𝑁 ClWWalksN 𝐺) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
| 21 | 20 | adantld 490 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) → ((𝐺 ∈ USGraph ∧ 𝑦 ∈ (𝑁 ClWWalksN 𝐺)) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
| 22 | 9, 21 | mpcom 38 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑦 ∈ (𝑁 ClWWalksN 𝐺)) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥)) |
| 23 | 22 | ex 412 |
. . . . 5
⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝑁 ClWWalksN 𝐺) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
| 24 | 5, 23 | impbid2 226 |
. . . 4
⊢ (𝐺 ∈ USGraph →
(∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑦‘0) = 𝑥) ↔ 𝑦 ∈ (𝑁 ClWWalksN 𝐺))) |
| 25 | 3, 24 | bitrid 283 |
. . 3
⊢ (𝐺 ∈ USGraph →
(∃𝑥 ∈ 𝑉 𝑦 ∈ (𝑥(ClWWalksNOn‘𝐺)𝑁) ↔ 𝑦 ∈ (𝑁 ClWWalksN 𝐺))) |
| 26 | 1, 25 | bitr2id 284 |
. 2
⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝑁 ClWWalksN 𝐺) ↔ 𝑦 ∈ ∪
𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁))) |
| 27 | 26 | eqrdv 2735 |
1
⊢ (𝐺 ∈ USGraph → (𝑁 ClWWalksN 𝐺) = ∪
𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁)) |