| Step |
Hyp |
Ref |
Expression |
| 1 |
|
relcmpcmet.1 |
|- J = ( MetOpen ` D ) |
| 2 |
|
relcmpcmet.2 |
|- ( ph -> D e. ( Met ` X ) ) |
| 3 |
|
cmpcmet.3 |
|- ( ph -> J e. Comp ) |
| 4 |
|
1rp |
|- 1 e. RR+ |
| 5 |
4
|
a1i |
|- ( ph -> 1 e. RR+ ) |
| 6 |
3
|
adantr |
|- ( ( ph /\ x e. X ) -> J e. Comp ) |
| 7 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
| 8 |
2 7
|
syl |
|- ( ph -> D e. ( *Met ` X ) ) |
| 9 |
8
|
adantr |
|- ( ( ph /\ x e. X ) -> D e. ( *Met ` X ) ) |
| 10 |
1
|
mopntop |
|- ( D e. ( *Met ` X ) -> J e. Top ) |
| 11 |
9 10
|
syl |
|- ( ( ph /\ x e. X ) -> J e. Top ) |
| 12 |
|
simpr |
|- ( ( ph /\ x e. X ) -> x e. X ) |
| 13 |
|
rpxr |
|- ( 1 e. RR+ -> 1 e. RR* ) |
| 14 |
4 13
|
mp1i |
|- ( ( ph /\ x e. X ) -> 1 e. RR* ) |
| 15 |
|
blssm |
|- ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) C_ X ) |
| 16 |
9 12 14 15
|
syl3anc |
|- ( ( ph /\ x e. X ) -> ( x ( ball ` D ) 1 ) C_ X ) |
| 17 |
1
|
mopnuni |
|- ( D e. ( *Met ` X ) -> X = U. J ) |
| 18 |
9 17
|
syl |
|- ( ( ph /\ x e. X ) -> X = U. J ) |
| 19 |
16 18
|
sseqtrd |
|- ( ( ph /\ x e. X ) -> ( x ( ball ` D ) 1 ) C_ U. J ) |
| 20 |
|
eqid |
|- U. J = U. J |
| 21 |
20
|
clscld |
|- ( ( J e. Top /\ ( x ( ball ` D ) 1 ) C_ U. J ) -> ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` J ) ) |
| 22 |
11 19 21
|
syl2anc |
|- ( ( ph /\ x e. X ) -> ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` J ) ) |
| 23 |
|
cmpcld |
|- ( ( J e. Comp /\ ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` J ) ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp ) |
| 24 |
6 22 23
|
syl2anc |
|- ( ( ph /\ x e. X ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp ) |
| 25 |
1 2 5 24
|
relcmpcmet |
|- ( ph -> D e. ( CMet ` X ) ) |