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

Metamath Proof Explorer

Theorem metdcn

Description: The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xmetdcn2.1 
|- J = ( MetOpen ` D )
metdcn.2 
|- K = ( TopOpen ` CCfld )
Assertion metdcn 
|- ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn K ) )

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 
 |-  J = ( MetOpen ` D )
2 metdcn.2 
 |-  K = ( TopOpen ` CCfld )
3 2 tgioo2 
 |-  ( topGen ` ran (,) ) = ( K |`t RR )
4 3 oveq2i 
 |-  ( ( J tX J ) Cn ( topGen ` ran (,) ) ) = ( ( J tX J ) Cn ( K |`t RR ) )
5 2 cnfldtop 
 |-  K e. Top
6 cnrest2r 
 |-  ( K e. Top -> ( ( J tX J ) Cn ( K |`t RR ) ) C_ ( ( J tX J ) Cn K ) )
7 5 6 ax-mp 
 |-  ( ( J tX J ) Cn ( K |`t RR ) ) C_ ( ( J tX J ) Cn K )
8 4 7 eqsstri 
 |-  ( ( J tX J ) Cn ( topGen ` ran (,) ) ) C_ ( ( J tX J ) Cn K )
9 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
10 1 9 metdcn2 
 |-  ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn ( topGen ` ran (,) ) ) )
11 8 10 sselid 
 |-  ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn K ) )