Theorem xmstopn

Description: The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Hypotheses	isms.j	|- J = ( TopOpen ` K )
	isms.x	|- X = ( Base ` K )
	isms.d	|- D = ( ( dist ` K ) |` ( X X. X ) )
Assertion	xmstopn	|- ( K e. *MetSp -> J = ( MetOpen ` D ) )

Proof

Step	Hyp	Ref	Expression
1		isms.j	|- J = ( TopOpen ` K )
2		isms.x	|- X = ( Base ` K )
3		isms.d	|- D = ( ( dist ` K ) |` ( X X. X ) )
4	1 2 3	isxms	|- ( K e. *MetSp <-> ( K e. TopSp /\ J = ( MetOpen ` D ) ) )
5	4	simprbi	|- ( K e. *MetSp -> J = ( MetOpen ` D ) )