Theorem xmetdcn

Description: The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	xmetdcn2.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	xmetdcn.2	$$⊢K=\mathrm{ordTop}\left(\le \right)$$
Assertion	xmetdcn	$$⊢D\in \mathrm{\infty 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		xmetdcn.2	$$⊢K=\mathrm{ordTop}\left(\le \right)$$
3		letopon	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
4	2 3	eqeltri	$$⊢K\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
5		eqid	$$⊢\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
6		eqid	$$⊢\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)=\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)$$
7	5 6	xrsmopn	$$⊢\mathrm{ordTop}\left(\le \right)\subseteq \mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)$$
8	2 7	eqsstri	$$⊢K\subseteq \mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)$$
9	5	xrsxmet	$$⊢\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\in \mathrm{\infty Met}\left({ℝ}^{*}\right)$$
10	6	mopnuni	$$⊢\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\in \mathrm{\infty Met}\left({ℝ}^{*}\right)\to {ℝ}^{*}=\bigcup \mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)$$
11	9 10	ax-mp	$$⊢{ℝ}^{*}=\bigcup \mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)$$
12	11	cnss2	$$⊢\left(K\in \mathrm{TopOn}\left({ℝ}^{*}\right)\wedge K\subseteq \mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)\to \left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\subseteq \left(J{\times }_{t}J\right)\mathrm{Cn}K$$
13	4 8 12	mp2an	$$⊢\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\subseteq \left(J{\times }_{t}J\right)\mathrm{Cn}K$$
14	1 5 6	xmetdcn2	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)$$
15	13 14	sselid	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}K\right)$$