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

Metamath Proof Explorer

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 \times X)}$
Assertion	xmstopn	$⊢ 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	isxms	$⊢ K \in ∞MetSp \leftrightarrow (K \in TopSp \land J = MetOpen (D))$
5	4	simprbi	$⊢ K \in ∞MetSp \to J = MetOpen (D)$