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

Metamath Proof Explorer

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 \times X)}$
Assertion	mstopn	$⊢ K \in MetSp \to 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 \times X)}$
4	1 2 3	isms2	$⊢ K \in MetSp \leftrightarrow (D \in Met (X) \land J = MetOpen (D))$
5	4	simprbi	$⊢ K \in MetSp \to J = MetOpen (D)$