| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mopni.1 |
β’ π½ = ( MetOpen β π· ) |
| 2 |
1
|
mopntop |
β’ ( π· β ( βMet β π ) β π½ β Top ) |
| 3 |
2
|
3ad2ant1 |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β+ ) β π½ β Top ) |
| 4 |
|
rpxr |
β’ ( π
β β+ β π
β β* ) |
| 5 |
1
|
blopn |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π ( ball β π· ) π
) β π½ ) |
| 6 |
4 5
|
syl3an3 |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β+ ) β ( π ( ball β π· ) π
) β π½ ) |
| 7 |
|
blcntr |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β+ ) β π β ( π ( ball β π· ) π
) ) |
| 8 |
|
opnneip |
β’ ( ( π½ β Top β§ ( π ( ball β π· ) π
) β π½ β§ π β ( π ( ball β π· ) π
) ) β ( π ( ball β π· ) π
) β ( ( nei β π½ ) β { π } ) ) |
| 9 |
3 6 7 8
|
syl3anc |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β+ ) β ( π ( ball β π· ) π
) β ( ( nei β π½ ) β { π } ) ) |