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 β π· ) π
) ) |