Step | Hyp | Ref
| Expression |
1 | | eliun 4460 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ↔ ∃𝑥 ∈ 𝑉 𝑦 ∈ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥}) |
2 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
3 | 2 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑥 ↔ (𝑦‘0) = 𝑥)) |
4 | 3 | elrab 3331 |
. . . . 5
⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ↔ (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥)) |
5 | 4 | rexbii 3023 |
. . . 4
⊢
(∃𝑥 ∈
𝑉 𝑦 ∈ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ↔ ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥)) |
6 | | simpl 472 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥) → 𝑦 ∈ (𝑁 ClWWalkSN 𝐺)) |
7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ ((𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥) → 𝑦 ∈ (𝑁 ClWWalkSN 𝐺))) |
8 | 7 | rexlimdvw 3016 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ (∃𝑥 ∈
𝑉 (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥) → 𝑦 ∈ (𝑁 ClWWalkSN 𝐺))) |
9 | | clwwlksnun.v |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
10 | | eqid 2610 |
. . . . . . . . 9
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
11 | 9, 10 | clwwlknp 41195 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) → ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) |
12 | 11 | anim2i 591 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ 𝑦 ∈ (𝑁 ClWWalkSN 𝐺)) → ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0) ∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺)))) |
13 | 10, 9 | usgrpredgav 40424 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ {( lastS
‘𝑦), (𝑦‘0)} ∈
(Edg‘𝐺)) → ((
lastS ‘𝑦) ∈
𝑉 ∧ (𝑦‘0) ∈ 𝑉)) |
14 | 13 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ USGraph → ({( lastS
‘𝑦), (𝑦‘0)} ∈
(Edg‘𝐺) → ((
lastS ‘𝑦) ∈
𝑉 ∧ (𝑦‘0) ∈ 𝑉))) |
15 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((( lastS
‘𝑦) ∈ 𝑉 ∧ (𝑦‘0) ∈ 𝑉) → (𝑦‘0) ∈ 𝑉) |
16 | 14, 15 | syl6 34 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → ({( lastS
‘𝑦), (𝑦‘0)} ∈
(Edg‘𝐺) → (𝑦‘0) ∈ 𝑉)) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ ({( lastS ‘𝑦),
(𝑦‘0)} ∈
(Edg‘𝐺) → (𝑦‘0) ∈ 𝑉)) |
18 | 17 | com12 32 |
. . . . . . . . . . 11
⊢ ({( lastS
‘𝑦), (𝑦‘0)} ∈
(Edg‘𝐺) →
((𝐺 ∈ USGraph ∧
𝑁 ∈
ℕ0) → (𝑦‘0) ∈ 𝑉)) |
19 | 18 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺)) → ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0) → (𝑦‘0) ∈ 𝑉)) |
20 | 19 | impcom 445 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) → (𝑦‘0) ∈ 𝑉) |
21 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → 𝑥 = (𝑦‘0)) |
22 | 21 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → (𝑦‘0) = 𝑥) |
23 | 22 | biantrud 527 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ↔ (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
24 | 23 | bicomd 212 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) ∧ 𝑥 = (𝑦‘0)) → ((𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥) ↔ 𝑦 ∈ (𝑁 ClWWalkSN 𝐺))) |
25 | 20, 24 | rspcedv 3286 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) → (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
26 | 25 | adantld 482 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ (Edg‘𝐺))) → (((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0) ∧ 𝑦 ∈ (𝑁 ClWWalkSN 𝐺)) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
27 | 12, 26 | mpcom 37 |
. . . . . 6
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
∧ 𝑦 ∈ (𝑁 ClWWalkSN 𝐺)) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥)) |
28 | 27 | ex 449 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) → ∃𝑥 ∈ 𝑉 (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥))) |
29 | 8, 28 | impbid 201 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ (∃𝑥 ∈
𝑉 (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑦‘0) = 𝑥) ↔ 𝑦 ∈ (𝑁 ClWWalkSN 𝐺))) |
30 | 5, 29 | syl5bb 271 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ (∃𝑥 ∈
𝑉 𝑦 ∈ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ↔ 𝑦 ∈ (𝑁 ClWWalkSN 𝐺))) |
31 | 1, 30 | syl5rbb 272 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ (𝑦 ∈ (𝑁 ClWWalkSN 𝐺) ↔ 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥})) |
32 | 31 | eqrdv 2608 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ (𝑁 ClWWalkSN 𝐺) = ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥}) |