Theorem metdcn2

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)$$
	metdcn2.2	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
Assertion	metdcn2	$$⊢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		metdcn2.2	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		metxmet	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \mathrm{\infty Met}\left(X\right)$$
4		eqid	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{ordTop}\left(\le \right)$$
5	1 4	xmetdcn	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{ordTop}\left(\le \right)\right)$$
6	3 5	syl	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{ordTop}\left(\le \right)\right)$$
7		letopon	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
8		metf	$$⊢D\in \mathrm{Met}\left(X\right)\to D:X\times X⟶ℝ$$
9	8	frnd	$$⊢D\in \mathrm{Met}\left(X\right)\to \mathrm{ran}D\subseteq ℝ$$
10		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
11	10	a1i	$$⊢D\in \mathrm{Met}\left(X\right)\to ℝ\subseteq {ℝ}^{*}$$
12		cnrest2	$$⊢\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\wedge \mathrm{ran}D\subseteq ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to \left(D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{ordTop}\left(\le \right)\right)\leftrightarrow D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
13	7 9 11 12	mp3an2i	$$⊢D\in \mathrm{Met}\left(X\right)\to \left(D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{ordTop}\left(\le \right)\right)\leftrightarrow D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
14	6 13	mpbid	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ\right)\right)$$
15		eqid	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
16	15	xrtgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
17	2 16	eqtri	$$⊢K=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
18	17	oveq2i	$$⊢\left(J{\times }_{t}J\right)\mathrm{Cn}K=\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ\right)$$
19	14 18	eleqtrrdi	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}K\right)$$