Step |
Hyp |
Ref |
Expression |
1 |
|
msdcn.x |
|- X = ( Base ` M ) |
2 |
|
msdcn.d |
|- D = ( dist ` M ) |
3 |
|
msdcn.j |
|- J = ( TopOpen ` M ) |
4 |
|
msdcn.2 |
|- K = ( topGen ` ran (,) ) |
5 |
1 2
|
msmet2 |
|- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) ) |
6 |
|
eqid |
|- ( MetOpen ` ( D |` ( X X. X ) ) ) = ( MetOpen ` ( D |` ( X X. X ) ) ) |
7 |
6 4
|
metdcn2 |
|- ( ( D |` ( X X. X ) ) e. ( Met ` X ) -> ( D |` ( X X. X ) ) e. ( ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) Cn K ) ) |
8 |
5 7
|
syl |
|- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) Cn K ) ) |
9 |
2
|
reseq1i |
|- ( D |` ( X X. X ) ) = ( ( dist ` M ) |` ( X X. X ) ) |
10 |
3 1 9
|
mstopn |
|- ( M e. MetSp -> J = ( MetOpen ` ( D |` ( X X. X ) ) ) ) |
11 |
10 10
|
oveq12d |
|- ( M e. MetSp -> ( J tX J ) = ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) ) |
12 |
11
|
oveq1d |
|- ( M e. MetSp -> ( ( J tX J ) Cn K ) = ( ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) Cn K ) ) |
13 |
8 12
|
eleqtrrd |
|- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( ( J tX J ) Cn K ) ) |