Theorem metdscn2

Description: The function F which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015)

	Ref	Expression
Hypotheses	metdscn.f	$$⊢F=\left(x\in X⟼sup\left(\mathrm{ran}\left(y\in S⟼xDy\right),{ℝ}^{*},<\right)\right)$$
	metdscn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	metdscn2.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	metdscn2	$$⊢\left(D\in \mathrm{Met}\left(X\right)\wedge S\subseteq X\wedge S\ne \varnothing \right)\to F\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$$⊢F=\left(x\in X⟼sup\left(\mathrm{ran}\left(y\in S⟼xDy\right),{ℝ}^{*},<\right)\right)$$
2		metdscn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
3		metdscn2.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4		eqid	$$⊢\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
5	4	xrsdsre	$$⊢{\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
6	4	xrsxmet	$$⊢\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\in \mathrm{\infty Met}\left({ℝ}^{*}\right)$$
7		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
8		eqid	$$⊢{\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\upharpoonright }_{{ℝ}^2}={\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\upharpoonright }_{{ℝ}^2}$$
9		eqid	$$⊢\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)=\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)$$
10		eqid	$$⊢\mathrm{MetOpen}\left({\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\upharpoonright }_{{ℝ}^2}\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\upharpoonright }_{{ℝ}^2}\right)$$
11	8 9 10	metrest	$$⊢\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\in \mathrm{\infty Met}\left({ℝ}^{*}\right)\wedge ℝ\subseteq {ℝ}^{*}\right)\to \mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ=\mathrm{MetOpen}\left({\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\upharpoonright }_{{ℝ}^2}\right)$$
12	6 7 11	mp2an	$$⊢\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ=\mathrm{MetOpen}\left({\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\upharpoonright }_{{ℝ}^2}\right)$$
13	5 12	tgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ$$
14	3	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=K{\upharpoonright }_{𝑡}ℝ$$
15	13 14	eqtr3i	$$⊢\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ=K{\upharpoonright }_{𝑡}ℝ$$
16	15	oveq2i	$$⊢J\mathrm{Cn}\left(\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ\right)=J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)$$
17	3	cnfldtop	$$⊢K\in \mathrm{Top}$$
18		cnrest2r	$$⊢K\in \mathrm{Top}\to J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq J\mathrm{Cn}K$$
19	17 18	ax-mp	$$⊢J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq J\mathrm{Cn}K$$
20	16 19	eqsstri	$$⊢J\mathrm{Cn}\left(\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ\right)\subseteq J\mathrm{Cn}K$$
21		metxmet	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \mathrm{\infty Met}\left(X\right)$$
22	1 2 4 9	metdscn	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge S\subseteq X\right)\to F\in \left(J\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)$$
23	21 22	sylan	$$⊢\left(D\in \mathrm{Met}\left(X\right)\wedge S\subseteq X\right)\to F\in \left(J\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)$$
24	23	3adant3	$$⊢\left(D\in \mathrm{Met}\left(X\right)\wedge S\subseteq X\wedge S\ne \varnothing \right)\to F\in \left(J\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)$$
25	1	metdsre	$$⊢\left(D\in \mathrm{Met}\left(X\right)\wedge S\subseteq X\wedge S\ne \varnothing \right)\to F:X⟶ℝ$$
26		frn	$$⊢F:X⟶ℝ\to \mathrm{ran}F\subseteq ℝ$$
27	9	mopntopon	$$⊢\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\in \mathrm{\infty Met}\left({ℝ}^{*}\right)\to \mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
28	6 27	ax-mp	$$⊢\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
29		cnrest2	$$⊢\left(\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\wedge \mathrm{ran}F\subseteq ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to \left(F\in \left(J\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)\leftrightarrow F\in \left(J\mathrm{Cn}\left(\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
30	28 7 29	mp3an13	$$⊢\mathrm{ran}F\subseteq ℝ\to \left(F\in \left(J\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)\leftrightarrow F\in \left(J\mathrm{Cn}\left(\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
31	25 26 30	3syl	$$⊢\left(D\in \mathrm{Met}\left(X\right)\wedge S\subseteq X\wedge S\ne \varnothing \right)\to \left(F\in \left(J\mathrm{Cn}\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right)\right)\leftrightarrow F\in \left(J\mathrm{Cn}\left(\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
32	24 31	mpbid	$$⊢\left(D\in \mathrm{Met}\left(X\right)\wedge S\subseteq X\wedge S\ne \varnothing \right)\to F\in \left(J\mathrm{Cn}\left(\mathrm{MetOpen}\left(\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)\right){\upharpoonright }_{𝑡}ℝ\right)\right)$$
33	20 32	sseldi	$$⊢\left(D\in \mathrm{Met}\left(X\right)\wedge S\subseteq X\wedge S\ne \varnothing \right)\to F\in \left(J\mathrm{Cn}K\right)$$