Theorem xmetdcn

Description: The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	xmetdcn2.1	|- J = ( MetOpen ` D )
	xmetdcn.2	|- K = ( ordTop ` <_ )
Assertion	xmetdcn	|- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		xmetdcn2.1	|- J = ( MetOpen ` D )
2		xmetdcn.2	|- K = ( ordTop ` <_ )
3		letopon	|- ( ordTop ` <_ ) e. ( TopOn ` RR* )
4	2 3	eqeltri	|- K e. ( TopOn ` RR* )
5		eqid	|- ( dist ` RR*s ) = ( dist ` RR*s )
6		eqid	|- ( MetOpen ` ( dist ` RR*s ) ) = ( MetOpen ` ( dist ` RR*s ) )
7	5 6	xrsmopn	|- ( ordTop ` <_ ) C_ ( MetOpen ` ( dist ` RR*s ) )
8	2 7	eqsstri	|- K C_ ( MetOpen ` ( dist ` RR*s ) )
9	5	xrsxmet	|- ( dist ` RR*s ) e. ( *Met ` RR* )
10	6	mopnuni	|- ( ( dist ` RR*s ) e. ( *Met ` RR* ) -> RR* = U. ( MetOpen ` ( dist ` RR*s ) ) )
11	9 10	ax-mp	|- RR* = U. ( MetOpen ` ( dist ` RR*s ) )
12	11	cnss2	|- ( ( K e. ( TopOn ` RR* ) /\ K C_ ( MetOpen ` ( dist ` RR*s ) ) ) -> ( ( J tX J ) Cn ( MetOpen ` ( dist ` RR*s ) ) ) C_ ( ( J tX J ) Cn K ) )
13	4 8 12	mp2an	|- ( ( J tX J ) Cn ( MetOpen ` ( dist ` RR*s ) ) ) C_ ( ( J tX J ) Cn K )
14	1 5 6	xmetdcn2	|- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn ( MetOpen ` ( dist ` RR*s ) ) ) )
15	13 14	sseldi	|- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) )