| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mopni.1 |
β’ π½ = ( MetOpen β π· ) |
| 2 |
|
ineq1 |
β’ ( π₯ = ( π ( ball β π· ) π
) β ( π₯ β© ( π β { π } ) ) = ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) ) |
| 3 |
2
|
neeq1d |
β’ ( π₯ = ( π ( ball β π· ) π
) β ( ( π₯ β© ( π β { π } ) ) β β
β ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) β β
) ) |
| 4 |
|
simpl3 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π β ( ( limPt β π½ ) β π ) ) |
| 5 |
|
simpl1 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π· β ( βMet β π ) ) |
| 6 |
1
|
mopntop |
β’ ( π· β ( βMet β π ) β π½ β Top ) |
| 7 |
5 6
|
syl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π½ β Top ) |
| 8 |
|
simpl2 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π β π ) |
| 9 |
1
|
mopnuni |
β’ ( π· β ( βMet β π ) β π = βͺ π½ ) |
| 10 |
5 9
|
syl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π = βͺ π½ ) |
| 11 |
8 10
|
sseqtrd |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π β βͺ π½ ) |
| 12 |
|
eqid |
β’ βͺ π½ = βͺ π½ |
| 13 |
12
|
lpss |
β’ ( ( π½ β Top β§ π β βͺ π½ ) β ( ( limPt β π½ ) β π ) β βͺ π½ ) |
| 14 |
7 11 13
|
syl2anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β ( ( limPt β π½ ) β π ) β βͺ π½ ) |
| 15 |
14 4
|
sseldd |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π β βͺ π½ ) |
| 16 |
12
|
islp2 |
β’ ( ( π½ β Top β§ π β βͺ π½ β§ π β βͺ π½ ) β ( π β ( ( limPt β π½ ) β π ) β β π₯ β ( ( nei β π½ ) β { π } ) ( π₯ β© ( π β { π } ) ) β β
) ) |
| 17 |
7 11 15 16
|
syl3anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β ( π β ( ( limPt β π½ ) β π ) β β π₯ β ( ( nei β π½ ) β { π } ) ( π₯ β© ( π β { π } ) ) β β
) ) |
| 18 |
4 17
|
mpbid |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β β π₯ β ( ( nei β π½ ) β { π } ) ( π₯ β© ( π β { π } ) ) β β
) |
| 19 |
15 10
|
eleqtrrd |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π β π ) |
| 20 |
|
simpr |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β π
β β+ ) |
| 21 |
1
|
blnei |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β+ ) β ( π ( ball β π· ) π
) β ( ( nei β π½ ) β { π } ) ) |
| 22 |
5 19 20 21
|
syl3anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β ( π ( ball β π· ) π
) β ( ( nei β π½ ) β { π } ) ) |
| 23 |
3 18 22
|
rspcdva |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) β β
) |
| 24 |
|
elin |
β’ ( π₯ β ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) β ( π₯ β ( π ( ball β π· ) π
) β§ π₯ β ( π β { π } ) ) ) |
| 25 |
|
eldifi |
β’ ( π₯ β ( π β { π } ) β π₯ β π ) |
| 26 |
25
|
anim2i |
β’ ( ( π₯ β ( π ( ball β π· ) π
) β§ π₯ β ( π β { π } ) ) β ( π₯ β ( π ( ball β π· ) π
) β§ π₯ β π ) ) |
| 27 |
26
|
ancomd |
β’ ( ( π₯ β ( π ( ball β π· ) π
) β§ π₯ β ( π β { π } ) ) β ( π₯ β π β§ π₯ β ( π ( ball β π· ) π
) ) ) |
| 28 |
24 27
|
sylbi |
β’ ( π₯ β ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) β ( π₯ β π β§ π₯ β ( π ( ball β π· ) π
) ) ) |
| 29 |
28
|
eximi |
β’ ( β π₯ π₯ β ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) β β π₯ ( π₯ β π β§ π₯ β ( π ( ball β π· ) π
) ) ) |
| 30 |
|
n0 |
β’ ( ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) β β
β β π₯ π₯ β ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) ) |
| 31 |
|
df-rex |
β’ ( β π₯ β π π₯ β ( π ( ball β π· ) π
) β β π₯ ( π₯ β π β§ π₯ β ( π ( ball β π· ) π
) ) ) |
| 32 |
29 30 31
|
3imtr4i |
β’ ( ( ( π ( ball β π· ) π
) β© ( π β { π } ) ) β β
β β π₯ β π π₯ β ( π ( ball β π· ) π
) ) |
| 33 |
23 32
|
syl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π β ( ( limPt β π½ ) β π ) ) β§ π
β β+ ) β β π₯ β π π₯ β ( π ( ball β π· ) π
) ) |