Theorem mstopn

Description: The topology component of a 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	mstopn	|- ( 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	isms2	|- ( K e. MetSp <-> ( D e. ( Met ` X ) /\ J = ( MetOpen ` D ) ) )
5	4	simprbi	|- ( K e. MetSp -> J = ( MetOpen ` D ) )