Metamath Proof Explorer


Theorem xmetdcn

Description: The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xmetdcn2.1
|- J = ( MetOpen ` D )
xmetdcn.2
|- K = ( ordTop ` <_ )
Assertion xmetdcn
|- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) )

Proof

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 ) )