Step | Hyp | Ref
| Expression |
1 | | cmptop 22762 |
. 2
β’ (π½ β Comp β π½ β Top) |
2 | | cmpcref 32488 |
. . . . . 6
β’ Comp =
CovHasRefFin |
3 | 2 | eleq2i 2826 |
. . . . 5
β’ (π½ β Comp β π½ β
CovHasRefFin) |
4 | | eqid 2733 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
5 | 4 | iscref 32482 |
. . . . 5
β’ (π½ β CovHasRefFin β
(π½ β Top β§
βπ¦ β π«
π½(βͺ π½ =
βͺ π¦ β βπ§ β (π« π½ β© Fin)π§Refπ¦))) |
6 | 3, 5 | bitri 275 |
. . . 4
β’ (π½ β Comp β (π½ β Top β§ βπ¦ β π« π½(βͺ
π½ = βͺ π¦
β βπ§ β
(π« π½ β©
Fin)π§Refπ¦))) |
7 | 6 | simprbi 498 |
. . 3
β’ (π½ β Comp β
βπ¦ β π«
π½(βͺ π½ =
βͺ π¦ β βπ§ β (π« π½ β© Fin)π§Refπ¦)) |
8 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β π§ β (π« π½ β© Fin)) |
9 | | elin 3927 |
. . . . . . . . . . . 12
β’ (π§ β (π« π½ β© Fin) β (π§ β π« π½ β§ π§ β Fin)) |
10 | 8, 9 | sylib 217 |
. . . . . . . . . . 11
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β (π§ β π« π½ β§ π§ β Fin)) |
11 | 10 | simpld 496 |
. . . . . . . . . 10
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β π§ β π« π½) |
12 | 1 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β π½ β Top) |
13 | 10 | simprd 497 |
. . . . . . . . . . 11
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β π§ β Fin) |
14 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β βͺ π½ = βͺ
π¦) |
15 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β π§Refπ¦) |
16 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ βͺ π§ =
βͺ π§ |
17 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ βͺ π¦ =
βͺ π¦ |
18 | 16, 17 | refbas 22877 |
. . . . . . . . . . . . 13
β’ (π§Refπ¦ β βͺ π¦ = βͺ
π§) |
19 | 15, 18 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β βͺ π¦ = βͺ
π§) |
20 | 14, 19 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β βͺ π½ = βͺ
π§) |
21 | 4, 16 | finlocfin 22887 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π§ β Fin β§ βͺ π½ =
βͺ π§) β π§ β (LocFinβπ½)) |
22 | 12, 13, 20, 21 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β π§ β (LocFinβπ½)) |
23 | 11, 22 | elind 4155 |
. . . . . . . . 9
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β π§ β (π« π½ β© (LocFinβπ½))) |
24 | 23, 15 | jca 513 |
. . . . . . . 8
β’ ((((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β§ (π§ β (π« π½ β© Fin) β§ π§Refπ¦)) β (π§ β (π« π½ β© (LocFinβπ½)) β§ π§Refπ¦)) |
25 | 24 | ex 414 |
. . . . . . 7
β’ (((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β ((π§ β (π« π½ β© Fin) β§ π§Refπ¦) β (π§ β (π« π½ β© (LocFinβπ½)) β§ π§Refπ¦))) |
26 | 25 | reximdv2 3158 |
. . . . . 6
β’ (((π½ β Comp β§ π¦ β π« π½) β§ βͺ π½ =
βͺ π¦) β (βπ§ β (π« π½ β© Fin)π§Refπ¦ β βπ§ β (π« π½ β© (LocFinβπ½))π§Refπ¦)) |
27 | 26 | ex 414 |
. . . . 5
β’ ((π½ β Comp β§ π¦ β π« π½) β (βͺ π½ =
βͺ π¦ β (βπ§ β (π« π½ β© Fin)π§Refπ¦ β βπ§ β (π« π½ β© (LocFinβπ½))π§Refπ¦))) |
28 | 27 | a2d 29 |
. . . 4
β’ ((π½ β Comp β§ π¦ β π« π½) β ((βͺ π½ =
βͺ π¦ β βπ§ β (π« π½ β© Fin)π§Refπ¦) β (βͺ π½ = βͺ
π¦ β βπ§ β (π« π½ β© (LocFinβπ½))π§Refπ¦))) |
29 | 28 | ralimdva 3161 |
. . 3
β’ (π½ β Comp β
(βπ¦ β π«
π½(βͺ π½ =
βͺ π¦ β βπ§ β (π« π½ β© Fin)π§Refπ¦) β βπ¦ β π« π½(βͺ π½ = βͺ
π¦ β βπ§ β (π« π½ β© (LocFinβπ½))π§Refπ¦))) |
30 | 7, 29 | mpd 15 |
. 2
β’ (π½ β Comp β
βπ¦ β π«
π½(βͺ π½ =
βͺ π¦ β βπ§ β (π« π½ β© (LocFinβπ½))π§Refπ¦)) |
31 | | ispcmp 32495 |
. . 3
β’ (π½ β Paracomp β π½ β
CovHasRef(LocFinβπ½)) |
32 | 4 | iscref 32482 |
. . 3
β’ (π½ β
CovHasRef(LocFinβπ½)
β (π½ β Top β§
βπ¦ β π«
π½(βͺ π½ =
βͺ π¦ β βπ§ β (π« π½ β© (LocFinβπ½))π§Refπ¦))) |
33 | 31, 32 | bitri 275 |
. 2
β’ (π½ β Paracomp β (π½ β Top β§ βπ¦ β π« π½(βͺ
π½ = βͺ π¦
β βπ§ β
(π« π½ β©
(LocFinβπ½))π§Refπ¦))) |
34 | 1, 30, 33 | sylanbrc 584 |
1
β’ (π½ β Comp β π½ β
Paracomp) |