| Step |
Hyp |
Ref |
Expression |
| 1 |
|
relcmpcmet.1 |
β’ π½ = ( MetOpen β π· ) |
| 2 |
|
relcmpcmet.2 |
β’ ( π β π· β ( Met β π ) ) |
| 3 |
|
relcmpcmet.3 |
β’ ( π β π
β β+ ) |
| 4 |
|
relcmpcmet.4 |
β’ ( ( π β§ π₯ β π ) β ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β Comp ) |
| 5 |
|
metxmet |
β’ ( π· β ( Met β π ) β π· β ( βMet β π ) ) |
| 6 |
2 5
|
syl |
β’ ( π β π· β ( βMet β π ) ) |
| 7 |
6
|
adantr |
β’ ( ( π β§ π β ( CauFil β π· ) ) β π· β ( βMet β π ) ) |
| 8 |
|
simpr |
β’ ( ( π β§ π β ( CauFil β π· ) ) β π β ( CauFil β π· ) ) |
| 9 |
3
|
adantr |
β’ ( ( π β§ π β ( CauFil β π· ) ) β π
β β+ ) |
| 10 |
|
cfil3i |
β’ ( ( π· β ( βMet β π ) β§ π β ( CauFil β π· ) β§ π
β β+ ) β β π₯ β π ( π₯ ( ball β π· ) π
) β π ) |
| 11 |
7 8 9 10
|
syl3anc |
β’ ( ( π β§ π β ( CauFil β π· ) ) β β π₯ β π ( π₯ ( ball β π· ) π
) β π ) |
| 12 |
6
|
ad2antrr |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π· β ( βMet β π ) ) |
| 13 |
1
|
mopntopon |
β’ ( π· β ( βMet β π ) β π½ β ( TopOn β π ) ) |
| 14 |
12 13
|
syl |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π½ β ( TopOn β π ) ) |
| 15 |
|
cfilfil |
β’ ( ( π· β ( βMet β π ) β§ π β ( CauFil β π· ) ) β π β ( Fil β π ) ) |
| 16 |
6 15
|
sylan |
β’ ( ( π β§ π β ( CauFil β π· ) ) β π β ( Fil β π ) ) |
| 17 |
16
|
adantr |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π β ( Fil β π ) ) |
| 18 |
|
simprr |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π₯ ( ball β π· ) π
) β π ) |
| 19 |
|
topontop |
β’ ( π½ β ( TopOn β π ) β π½ β Top ) |
| 20 |
14 19
|
syl |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π½ β Top ) |
| 21 |
|
simprl |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π₯ β π ) |
| 22 |
3
|
rpxrd |
β’ ( π β π
β β* ) |
| 23 |
22
|
ad2antrr |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π
β β* ) |
| 24 |
|
blssm |
β’ ( ( π· β ( βMet β π ) β§ π₯ β π β§ π
β β* ) β ( π₯ ( ball β π· ) π
) β π ) |
| 25 |
12 21 23 24
|
syl3anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π₯ ( ball β π· ) π
) β π ) |
| 26 |
|
toponuni |
β’ ( π½ β ( TopOn β π ) β π = βͺ π½ ) |
| 27 |
14 26
|
syl |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π = βͺ π½ ) |
| 28 |
25 27
|
sseqtrd |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π₯ ( ball β π· ) π
) β βͺ π½ ) |
| 29 |
|
eqid |
β’ βͺ π½ = βͺ π½ |
| 30 |
29
|
clsss3 |
β’ ( ( π½ β Top β§ ( π₯ ( ball β π· ) π
) β βͺ π½ ) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β βͺ π½ ) |
| 31 |
20 28 30
|
syl2anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β βͺ π½ ) |
| 32 |
31 27
|
sseqtrrd |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π ) |
| 33 |
29
|
sscls |
β’ ( ( π½ β Top β§ ( π₯ ( ball β π· ) π
) β βͺ π½ ) β ( π₯ ( ball β π· ) π
) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) |
| 34 |
20 28 33
|
syl2anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π₯ ( ball β π· ) π
) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) |
| 35 |
|
filss |
β’ ( ( π β ( Fil β π ) β§ ( ( π₯ ( ball β π· ) π
) β π β§ ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π β§ ( π₯ ( ball β π· ) π
) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π ) |
| 36 |
17 18 32 34 35
|
syl13anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π ) |
| 37 |
|
fclsrest |
β’ ( ( π½ β ( TopOn β π ) β§ π β ( Fil β π ) β§ ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π ) β ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) fClus ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) = ( ( π½ fClus π ) β© ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) |
| 38 |
14 17 36 37
|
syl3anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) fClus ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) = ( ( π½ fClus π ) β© ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) |
| 39 |
|
inss1 |
β’ ( ( π½ fClus π ) β© ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( π½ fClus π ) |
| 40 |
|
eqid |
β’ dom dom π· = dom dom π· |
| 41 |
1 40
|
cfilfcls |
β’ ( π β ( CauFil β π· ) β ( π½ fClus π ) = ( π½ fLim π ) ) |
| 42 |
41
|
ad2antlr |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π½ fClus π ) = ( π½ fLim π ) ) |
| 43 |
39 42
|
sseqtrid |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( π½ fClus π ) β© ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( π½ fLim π ) ) |
| 44 |
38 43
|
eqsstrd |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) fClus ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) β ( π½ fLim π ) ) |
| 45 |
4
|
ad2ant2r |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β Comp ) |
| 46 |
|
filfbas |
β’ ( π β ( Fil β π ) β π β ( fBas β π ) ) |
| 47 |
17 46
|
syl |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β π β ( fBas β π ) ) |
| 48 |
|
fbncp |
β’ ( ( π β ( fBas β π ) β§ ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π ) β Β¬ ( π β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β π ) |
| 49 |
47 36 48
|
syl2anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β Β¬ ( π β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β π ) |
| 50 |
|
trfil3 |
β’ ( ( π β ( Fil β π ) β§ ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π ) β ( ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( Fil β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β Β¬ ( π β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β π ) ) |
| 51 |
17 32 50
|
syl2anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( Fil β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β Β¬ ( π β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β π ) ) |
| 52 |
49 51
|
mpbird |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( Fil β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) |
| 53 |
|
resttopon |
β’ ( ( π½ β ( TopOn β π ) β§ ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) β π ) β ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( TopOn β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) |
| 54 |
14 32 53
|
syl2anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( TopOn β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) |
| 55 |
|
toponuni |
β’ ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( TopOn β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) = βͺ ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) |
| 56 |
54 55
|
syl |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) = βͺ ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) |
| 57 |
56
|
fveq2d |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( Fil β ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) = ( Fil β βͺ ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) ) |
| 58 |
52 57
|
eleqtrd |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( Fil β βͺ ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) ) |
| 59 |
|
eqid |
β’ βͺ ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) = βͺ ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) |
| 60 |
59
|
fclscmpi |
β’ ( ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β Comp β§ ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) β ( Fil β βͺ ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) ) β ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) fClus ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) β β
) |
| 61 |
45 58 60
|
syl2anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) fClus ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) β β
) |
| 62 |
|
ssn0 |
β’ ( ( ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) fClus ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) β ( π½ fLim π ) β§ ( ( π½ βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) fClus ( π βΎt ( ( cls β π½ ) β ( π₯ ( ball β π· ) π
) ) ) ) β β
) β ( π½ fLim π ) β β
) |
| 63 |
44 61 62
|
syl2anc |
β’ ( ( ( π β§ π β ( CauFil β π· ) ) β§ ( π₯ β π β§ ( π₯ ( ball β π· ) π
) β π ) ) β ( π½ fLim π ) β β
) |
| 64 |
11 63
|
rexlimddv |
β’ ( ( π β§ π β ( CauFil β π· ) ) β ( π½ fLim π ) β β
) |
| 65 |
64
|
ralrimiva |
β’ ( π β β π β ( CauFil β π· ) ( π½ fLim π ) β β
) |
| 66 |
1
|
iscmet |
β’ ( π· β ( CMet β π ) β ( π· β ( Met β π ) β§ β π β ( CauFil β π· ) ( π½ fLim π ) β β
) ) |
| 67 |
2 65 66
|
sylanbrc |
β’ ( π β π· β ( CMet β π ) ) |