Theorem metdcn

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, 4-Sep-2015)

	Ref	Expression
Hypotheses	xmetdcn2.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	metdcn.2	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	metdcn	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		xmetdcn2.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
2		metdcn.2	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=K{\upharpoonright }_{𝑡}ℝ$$
4	3	oveq2i	$$⊢\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\left(J{\times }_{t}J\right)\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)$$
5	2	cnfldtop	$$⊢K\in \mathrm{Top}$$
6		cnrest2r	$$⊢K\in \mathrm{Top}\to \left(J{\times }_{t}J\right)\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq \left(J{\times }_{t}J\right)\mathrm{Cn}K$$
7	5 6	ax-mp	$$⊢\left(J{\times }_{t}J\right)\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq \left(J{\times }_{t}J\right)\mathrm{Cn}K$$
8	4 7	eqsstri	$$⊢\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\subseteq \left(J{\times }_{t}J\right)\mathrm{Cn}K$$
9		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
10	1 9	metdcn2	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
11	8 10	sselid	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}K\right)$$