| Step | Hyp | Ref
| Expression |
|---|
| 1 | | distop 22498 |
. . 3
β’ (π β π β π« π β Top) |
| 2 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π₯ β π β§ π’ = {π₯}) β π’ = {π₯}) |
| 3 | | snelpwi 5444 |
. . . . . . . . . . . . 13
β’ (π₯ β π β {π₯} β π« π) |
| 4 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π₯ β π β§ π’ = {π₯}) β {π₯} β π« π) |
| 5 | 2, 4 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π’ = {π₯}) β π’ β π« π) |
| 6 | 5 | rexlimiva 3148 |
. . . . . . . . . 10
β’
(βπ₯ β
π π’ = {π₯} β π’ β π« π) |
| 7 | 6 | abssi 4068 |
. . . . . . . . 9
β’ {π’ β£ βπ₯ β π π’ = {π₯}} β π« π |
| 8 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π’ = π£ β§ π₯ = π§) β π’ = π£) |
| 9 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π’ = π£ β§ π₯ = π§) β π₯ = π§) |
| 10 | 9 | sneqd 4641 |
. . . . . . . . . . . . . 14
β’ ((π’ = π£ β§ π₯ = π§) β {π₯} = {π§}) |
| 11 | 8, 10 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ ((π’ = π£ β§ π₯ = π§) β (π’ = {π₯} β π£ = {π§})) |
| 12 | 11 | cbvrexdva 3238 |
. . . . . . . . . . . 12
β’ (π’ = π£ β (βπ₯ β π π’ = {π₯} β βπ§ β π π£ = {π§})) |
| 13 | 12 | cbvabv 2806 |
. . . . . . . . . . 11
β’ {π’ β£ βπ₯ β π π’ = {π₯}} = {π£ β£ βπ§ β π π£ = {π§}} |
| 14 | 13 | dissnlocfin 23033 |
. . . . . . . . . 10
β’ (π β π β {π’ β£ βπ₯ β π π’ = {π₯}} β (LocFinβπ« π)) |
| 15 | | elpwg 4606 |
. . . . . . . . . 10
β’ ({π’ β£ βπ₯ β π π’ = {π₯}} β (LocFinβπ« π) β ({π’ β£ βπ₯ β π π’ = {π₯}} β π« π« π β {π’ β£ βπ₯ β π π’ = {π₯}} β π« π)) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . 9
β’ (π β π β ({π’ β£ βπ₯ β π π’ = {π₯}} β π« π« π β {π’ β£ βπ₯ β π π’ = {π₯}} β π« π)) |
| 17 | 7, 16 | mpbiri 258 |
. . . . . . . 8
β’ (π β π β {π’ β£ βπ₯ β π π’ = {π₯}} β π« π« π) |
| 18 | 17 | ad2antrr 725 |
. . . . . . 7
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β {π’ β£ βπ₯ β π π’ = {π₯}} β π« π« π) |
| 19 | 14 | ad2antrr 725 |
. . . . . . 7
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β {π’ β£ βπ₯ β π π’ = {π₯}} β (LocFinβπ« π)) |
| 20 | 18, 19 | elind 4195 |
. . . . . 6
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β {π’ β£ βπ₯ β π π’ = {π₯}} β (π« π« π β© (LocFinβπ«
π))) |
| 21 | | simpll 766 |
. . . . . . 7
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β π β π) |
| 22 | | simpr 486 |
. . . . . . . 8
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β π = βͺ π¦) |
| 23 | 22 | eqcomd 2739 |
. . . . . . 7
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β βͺ π¦ =
π) |
| 24 | 13 | dissnref 23032 |
. . . . . . 7
β’ ((π β π β§ βͺ π¦ = π) β {π’ β£ βπ₯ β π π’ = {π₯}}Refπ¦) |
| 25 | 21, 23, 24 | syl2anc 585 |
. . . . . 6
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β {π’ β£ βπ₯ β π π’ = {π₯}}Refπ¦) |
| 26 | | breq1 5152 |
. . . . . . 7
β’ (π§ = {π’ β£ βπ₯ β π π’ = {π₯}} β (π§Refπ¦ β {π’ β£ βπ₯ β π π’ = {π₯}}Refπ¦)) |
| 27 | 26 | rspcev 3613 |
. . . . . 6
β’ (({π’ β£ βπ₯ β π π’ = {π₯}} β (π« π« π β© (LocFinβπ«
π)) β§ {π’ β£ βπ₯ β π π’ = {π₯}}Refπ¦) β βπ§ β (π« π« π β© (LocFinβπ«
π))π§Refπ¦) |
| 28 | 20, 25, 27 | syl2anc 585 |
. . . . 5
β’ (((π β π β§ π¦ β π« π« π) β§ π = βͺ π¦) β βπ§ β (π« π«
π β©
(LocFinβπ« π))π§Refπ¦) |
| 29 | 28 | ex 414 |
. . . 4
β’ ((π β π β§ π¦ β π« π« π) β (π = βͺ π¦ β βπ§ β (π« π«
π β©
(LocFinβπ« π))π§Refπ¦)) |
| 30 | 29 | ralrimiva 3147 |
. . 3
β’ (π β π β βπ¦ β π« π« π(π = βͺ π¦ β βπ§ β (π« π«
π β©
(LocFinβπ« π))π§Refπ¦)) |
| 31 | | unipw 5451 |
. . . . 5
β’ βͺ π« π = π |
| 32 | 31 | eqcomi 2742 |
. . . 4
β’ π = βͺ
π« π |
| 33 | 32 | iscref 32824 |
. . 3
β’
(π« π β
CovHasRef(LocFinβπ« π) β (π« π β Top β§ βπ¦ β π« π« π(π = βͺ π¦ β βπ§ β (π« π«
π β©
(LocFinβπ« π))π§Refπ¦))) |
| 34 | 1, 30, 33 | sylanbrc 584 |
. 2
β’ (π β π β π« π β CovHasRef(LocFinβπ«
π)) |
| 35 | | ispcmp 32837 |
. 2
β’
(π« π β
Paracomp β π« π
β CovHasRef(LocFinβπ« π)) |
| 36 | 34, 35 | sylibr 233 |
1
β’ (π β π β π« π β Paracomp) |
