Metamath Proof Explorer

Theorem metdcn2

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 )
metdcn2.2 
|- K = ( topGen ` ran (,) )
Assertion metdcn2 
|- ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn K ) )

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 
 |-  J = ( MetOpen ` D )
2 metdcn2.2 
 |-  K = ( topGen ` ran (,) )
3 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
4 eqid 
 |-  ( ordTop ` <_ ) = ( ordTop ` <_ )
5 1 4 xmetdcn 
 |-  ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn ( ordTop ` <_ ) ) )
6 3 5 syl 
 |-  ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn ( ordTop ` <_ ) ) )
7 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
8 metf 
 |-  ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )
9 8 frnd 
 |-  ( D e. ( Met ` X ) -> ran D C_ RR )
10 ressxr 
 |-  RR C_ RR*
11 10 a1i 
 |-  ( D e. ( Met ` X ) -> RR C_ RR* )
12 cnrest2 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ran D C_ RR /\ RR C_ RR* ) -> ( D e. ( ( J tX J ) Cn ( ordTop ` <_ ) ) <-> D e. ( ( J tX J ) Cn ( ( ordTop ` <_ ) |`t RR ) ) ) )
13 7 9 11 12 mp3an2i 
 |-  ( D e. ( Met ` X ) -> ( D e. ( ( J tX J ) Cn ( ordTop ` <_ ) ) <-> D e. ( ( J tX J ) Cn ( ( ordTop ` <_ ) |`t RR ) ) ) )
14 6 13 mpbid 
 |-  ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn ( ( ordTop ` <_ ) |`t RR ) ) )
15 eqid 
 |-  ( ( ordTop ` <_ ) |`t RR ) = ( ( ordTop ` <_ ) |`t RR )
16 15 xrtgioo 
 |-  ( topGen ` ran (,) ) = ( ( ordTop ` <_ ) |`t RR )
17 2 16 eqtri 
 |-  K = ( ( ordTop ` <_ ) |`t RR )
18 17 oveq2i 
 |-  ( ( J tX J ) Cn K ) = ( ( J tX J ) Cn ( ( ordTop ` <_ ) |`t RR ) )
19 14 18 eleqtrrdi 
 |-  ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn K ) )