This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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