Step | Hyp | Ref
| Expression |
1 | | numclwwlk.c |
. . . . . . . . . 10
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
2 | 1 | numclwwlkfvc 26604 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
3 | 2 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑦 ∈ (𝐶‘𝑁) ↔ 𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
4 | 3 | biimpac 502 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝐶‘𝑁) ∧ 𝑁 ∈ ℕ0) → 𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
5 | 4 | adantll 746 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ ℕ0) → 𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
6 | | clwwlknimp 26304 |
. . . . . . . 8
⊢ (𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ ran 𝐸)) |
7 | | usgraedgrnv 25906 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ ran 𝐸) → (( lastS ‘𝑦) ∈ 𝑉 ∧ (𝑦‘0) ∈ 𝑉)) |
8 | 7 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ ran 𝐸) → (𝑦‘0) ∈ 𝑉) |
9 | 8 | ancoms 468 |
. . . . . . . . . . 11
⊢ (({(
lastS ‘𝑦), (𝑦‘0)} ∈ ran 𝐸 ∧ 𝑉 USGrph 𝐸) → (𝑦‘0) ∈ 𝑉) |
10 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐶‘𝑁) → 𝑦 ∈ (𝐶‘𝑁)) |
11 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐶‘𝑁) → (𝑦‘0) = (𝑦‘0)) |
12 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
13 | 12 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑦 → ((𝑤‘0) = (𝑦‘0) ↔ (𝑦‘0) = (𝑦‘0))) |
14 | 13 | elrab 3331 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = (𝑦‘0)} ↔ (𝑦 ∈ (𝐶‘𝑁) ∧ (𝑦‘0) = (𝑦‘0))) |
15 | 10, 11, 14 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐶‘𝑁) → 𝑦 ∈ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = (𝑦‘0)}) |
16 | | eqeq2 2621 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦‘0) → ((𝑤‘0) = 𝑥 ↔ (𝑤‘0) = (𝑦‘0))) |
17 | 16 | rabbidv 3164 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦‘0) → {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥} = {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = (𝑦‘0)}) |
18 | 17 | eliuni 4462 |
. . . . . . . . . . 11
⊢ (((𝑦‘0) ∈ 𝑉 ∧ 𝑦 ∈ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = (𝑦‘0)}) → 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥}) |
19 | 9, 15, 18 | syl2an 493 |
. . . . . . . . . 10
⊢ ((({(
lastS ‘𝑦), (𝑦‘0)} ∈ ran 𝐸 ∧ 𝑉 USGrph 𝐸) ∧ 𝑦 ∈ (𝐶‘𝑁)) → 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥}) |
20 | 19 | expl 646 |
. . . . . . . . 9
⊢ ({( lastS
‘𝑦), (𝑦‘0)} ∈ ran 𝐸 → ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ (𝐶‘𝑁)) → 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥})) |
21 | 20 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑦), (𝑦‘0)} ∈ ran 𝐸) → ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ (𝐶‘𝑁)) → 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥})) |
22 | 6, 21 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ (𝐶‘𝑁)) → 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥})) |
23 | 22 | adantrd 483 |
. . . . . 6
⊢ (𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ ℕ0) → 𝑦 ∈ ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥})) |
24 | 5, 23 | mpcom 37 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ ℕ0) → 𝑦 ∈ ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥}) |
25 | 24 | ex 449 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ (𝐶‘𝑁)) → (𝑁 ∈ ℕ0 → 𝑦 ∈ ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥})) |
26 | 25 | impancom 455 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ (𝐶‘𝑁) → 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥})) |
27 | | eliun 4460 |
. . . 4
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥} ↔ ∃𝑥 ∈ 𝑉 𝑦 ∈ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥}) |
28 | | elrabi 3328 |
. . . . 5
⊢ (𝑦 ∈ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥} → 𝑦 ∈ (𝐶‘𝑁)) |
29 | 28 | rexlimivw 3011 |
. . . 4
⊢
(∃𝑥 ∈
𝑉 𝑦 ∈ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥} → 𝑦 ∈ (𝐶‘𝑁)) |
30 | 27, 29 | sylbi 206 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥} → 𝑦 ∈ (𝐶‘𝑁)) |
31 | 26, 30 | impbid1 214 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ (𝐶‘𝑁) ↔ 𝑦 ∈ ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥})) |
32 | 31 | eqrdv 2608 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → (𝐶‘𝑁) = ∪
𝑥 ∈ 𝑉 {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑥}) |