Step | Hyp | Ref
| Expression |
1 | | numclwwlk3lem2.h |
. . . 4
β’ π» = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) |
2 | 1 | numclwwlkovh0 29358 |
. . 3
β’ ((π β π β§ π β (β€β₯β2))
β (ππ»π) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π}) |
3 | | numclwwlk3lem2.c |
. . . 4
β’ πΆ = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
4 | 3 | 2clwwlk 29333 |
. . 3
β’ ((π β π β§ π β (β€β₯β2))
β (ππΆπ) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) |
5 | 2, 4 | uneq12d 4129 |
. 2
β’ ((π β π β§ π β (β€β₯β2))
β ((ππ»π) βͺ (ππΆπ)) = ({π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} βͺ {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π})) |
6 | | unrab 4270 |
. . 3
β’ ({π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} βͺ {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ ((π€β(π β 2)) β π β¨ (π€β(π β 2)) = π)} |
7 | | exmidne 2954 |
. . . . . 6
β’ ((π€β(π β 2)) = π β¨ (π€β(π β 2)) β π) |
8 | | orcom 869 |
. . . . . 6
β’ (((π€β(π β 2)) β π β¨ (π€β(π β 2)) = π) β ((π€β(π β 2)) = π β¨ (π€β(π β 2)) β π)) |
9 | 7, 8 | mpbir 230 |
. . . . 5
β’ ((π€β(π β 2)) β π β¨ (π€β(π β 2)) = π) |
10 | 9 | a1i 11 |
. . . 4
β’ (π€ β (π(ClWWalksNOnβπΊ)π) β ((π€β(π β 2)) β π β¨ (π€β(π β 2)) = π)) |
11 | 10 | rabeqc 3422 |
. . 3
β’ {π€ β (π(ClWWalksNOnβπΊ)π) β£ ((π€β(π β 2)) β π β¨ (π€β(π β 2)) = π)} = (π(ClWWalksNOnβπΊ)π) |
12 | 6, 11 | eqtri 2765 |
. 2
β’ ({π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} βͺ {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) = (π(ClWWalksNOnβπΊ)π) |
13 | 5, 12 | eqtr2di 2794 |
1
β’ ((π β π β§ π β (β€β₯β2))
β (π(ClWWalksNOnβπΊ)π) = ((ππ»π) βͺ (ππΆπ))) |