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

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