Step | Hyp | Ref
| Expression |
1 | | llytop 22846 |
. 2
β’ (π½ β Locally π΄ β π½ β Top) |
2 | | llyi 22848 |
. . . . 5
β’ ((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β βπ’ β π½ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄)) |
3 | | simpl1 1192 |
. . . . . . . 8
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π½ β Locally π΄) |
4 | 3, 1 | syl 17 |
. . . . . . 7
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π½ β Top) |
5 | | simprl 770 |
. . . . . . 7
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π’ β π½) |
6 | | simprr2 1223 |
. . . . . . 7
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π¦ β π’) |
7 | | opnneip 22493 |
. . . . . . 7
β’ ((π½ β Top β§ π’ β π½ β§ π¦ β π’) β π’ β ((neiβπ½)β{π¦})) |
8 | 4, 5, 6, 7 | syl3anc 1372 |
. . . . . 6
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π’ β ((neiβπ½)β{π¦})) |
9 | | simprr1 1222 |
. . . . . . 7
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π’ β π₯) |
10 | | velpw 4569 |
. . . . . . 7
β’ (π’ β π« π₯ β π’ β π₯) |
11 | 9, 10 | sylibr 233 |
. . . . . 6
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π’ β π« π₯) |
12 | 8, 11 | elind 4158 |
. . . . 5
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β π’ β (((neiβπ½)β{π¦}) β© π« π₯)) |
13 | | simprr3 1224 |
. . . . 5
β’ (((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β§ (π’ β π½ β§ (π’ β π₯ β§ π¦ β π’ β§ (π½ βΎt π’) β π΄))) β (π½ βΎt π’) β π΄) |
14 | 2, 12, 13 | reximssdv 3166 |
. . . 4
β’ ((π½ β Locally π΄ β§ π₯ β π½ β§ π¦ β π₯) β βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄) |
15 | 14 | 3expb 1121 |
. . 3
β’ ((π½ β Locally π΄ β§ (π₯ β π½ β§ π¦ β π₯)) β βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄) |
16 | 15 | ralrimivva 3194 |
. 2
β’ (π½ β Locally π΄ β βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄) |
17 | | isnlly 22843 |
. 2
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
18 | 1, 16, 17 | sylanbrc 584 |
1
β’ (π½ β Locally π΄ β π½ β π-Locally π΄) |