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