Metamath Proof Explorer

Theorem msdcn

Description: The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Hypotheses	msdcn.x	$⊢ X = {Base}_{M}$
		msdcn.d	$⊢ D = dist (M)$
		msdcn.j	$⊢ J = TopOpen (M)$
		msdcn.2	$⊢ K = topGen (ran (.))$
	Assertion	msdcn	$⊢ M \in MetSp \to {D ↾}_{(X \times X)} \in ((J \times_{t} J) Cn K)$

Proof

Step	Hyp	Ref	Expression
1		msdcn.x	$⊢ X = {Base}_{M}$
2		msdcn.d	$⊢ D = dist (M)$
3		msdcn.j	$⊢ J = TopOpen (M)$
4		msdcn.2	$⊢ K = topGen (ran (.))$
5	1 2	msmet2	$⊢ M \in MetSp \to {D ↾}_{(X \times X)} \in Met (X)$
6		eqid	$⊢ MetOpen ({D ↾}_{(X \times X)}) = MetOpen ({D ↾}_{(X \times X)})$
7	6 4	metdcn2	$⊢ {D ↾}_{(X \times X)} \in Met (X) \to {D ↾}_{(X \times X)} \in ((MetOpen ({D ↾}_{(X \times X)}) \times_{t} MetOpen ({D ↾}_{(X \times X)})) Cn K)$
8	5 7	syl	$⊢ M \in MetSp \to {D ↾}_{(X \times X)} \in ((MetOpen ({D ↾}_{(X \times X)}) \times_{t} MetOpen ({D ↾}_{(X \times X)})) Cn K)$
9	2	reseq1i	$⊢ {D ↾}_{(X \times X)} = {dist (M) ↾}_{(X \times X)}$
10	3 1 9	mstopn	$⊢ M \in MetSp \to J = MetOpen ({D ↾}_{(X \times X)})$
11	10 10	oveq12d	$⊢ M \in MetSp \to J \times_{t} J = MetOpen ({D ↾}_{(X \times X)}) \times_{t} MetOpen ({D ↾}_{(X \times X)})$
12	11	oveq1d	$⊢ M \in MetSp \to (J \times_{t} J) Cn K = (MetOpen ({D ↾}_{(X \times X)}) \times_{t} MetOpen ({D ↾}_{(X \times X)})) Cn K$
13	8 12	eleqtrrd	$⊢ M \in MetSp \to {D ↾}_{(X \times X)} \in ((J \times_{t} J) Cn K)$