Metamath Proof Explorer


Theorem msdcn

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, 5-Oct-2015)

Ref Expression
Hypotheses msdcn.x
|- X = ( Base ` M )
msdcn.d
|- D = ( dist ` M )
msdcn.j
|- J = ( TopOpen ` M )
msdcn.2
|- K = ( topGen ` ran (,) )
Assertion msdcn
|- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( ( J tX J ) Cn K ) )

Proof

Step Hyp Ref Expression
1 msdcn.x
 |-  X = ( Base ` M )
2 msdcn.d
 |-  D = ( dist ` M )
3 msdcn.j
 |-  J = ( TopOpen ` M )
4 msdcn.2
 |-  K = ( topGen ` ran (,) )
5 1 2 msmet2
 |-  ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) )
6 eqid
 |-  ( MetOpen ` ( D |` ( X X. X ) ) ) = ( MetOpen ` ( D |` ( X X. X ) ) )
7 6 4 metdcn2
 |-  ( ( D |` ( X X. X ) ) e. ( Met ` X ) -> ( D |` ( X X. X ) ) e. ( ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) Cn K ) )
8 5 7 syl
 |-  ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) Cn K ) )
9 2 reseq1i
 |-  ( D |` ( X X. X ) ) = ( ( dist ` M ) |` ( X X. X ) )
10 3 1 9 mstopn
 |-  ( M e. MetSp -> J = ( MetOpen ` ( D |` ( X X. X ) ) ) )
11 10 10 oveq12d
 |-  ( M e. MetSp -> ( J tX J ) = ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) )
12 11 oveq1d
 |-  ( M e. MetSp -> ( ( J tX J ) Cn K ) = ( ( ( MetOpen ` ( D |` ( X X. X ) ) ) tX ( MetOpen ` ( D |` ( X X. X ) ) ) ) Cn K ) )
13 8 12 eleqtrrd
 |-  ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( ( J tX J ) Cn K ) )