Step |
Hyp |
Ref |
Expression |
1 |
|
xmetdcn2.1 |
|- J = ( MetOpen ` D ) |
2 |
|
xmetdcn.2 |
|- K = ( ordTop ` <_ ) |
3 |
|
letopon |
|- ( ordTop ` <_ ) e. ( TopOn ` RR* ) |
4 |
2 3
|
eqeltri |
|- K e. ( TopOn ` RR* ) |
5 |
|
eqid |
|- ( dist ` RR*s ) = ( dist ` RR*s ) |
6 |
|
eqid |
|- ( MetOpen ` ( dist ` RR*s ) ) = ( MetOpen ` ( dist ` RR*s ) ) |
7 |
5 6
|
xrsmopn |
|- ( ordTop ` <_ ) C_ ( MetOpen ` ( dist ` RR*s ) ) |
8 |
2 7
|
eqsstri |
|- K C_ ( MetOpen ` ( dist ` RR*s ) ) |
9 |
5
|
xrsxmet |
|- ( dist ` RR*s ) e. ( *Met ` RR* ) |
10 |
6
|
mopnuni |
|- ( ( dist ` RR*s ) e. ( *Met ` RR* ) -> RR* = U. ( MetOpen ` ( dist ` RR*s ) ) ) |
11 |
9 10
|
ax-mp |
|- RR* = U. ( MetOpen ` ( dist ` RR*s ) ) |
12 |
11
|
cnss2 |
|- ( ( K e. ( TopOn ` RR* ) /\ K C_ ( MetOpen ` ( dist ` RR*s ) ) ) -> ( ( J tX J ) Cn ( MetOpen ` ( dist ` RR*s ) ) ) C_ ( ( J tX J ) Cn K ) ) |
13 |
4 8 12
|
mp2an |
|- ( ( J tX J ) Cn ( MetOpen ` ( dist ` RR*s ) ) ) C_ ( ( J tX J ) Cn K ) |
14 |
1 5 6
|
xmetdcn2 |
|- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn ( MetOpen ` ( dist ` RR*s ) ) ) ) |
15 |
13 14
|
sselid |
|- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) ) |