Theorem resubmet

Description: The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypotheses	resubmet.1	$$⊢R=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	resubmet.2	$$⊢J=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
Assertion	resubmet	$$⊢A\subseteq ℝ\to J=R{\upharpoonright }_{𝑡}A$$

Proof

Step	Hyp	Ref	Expression
1		resubmet.1	$$⊢R=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		resubmet.2	$$⊢J=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
3		xpss12	$$⊢\left(A\subseteq ℝ\wedge A\subseteq ℝ\right)\to A\times A\subseteq {ℝ}^2$$
4	3	anidms	$$⊢A\subseteq ℝ\to A\times A\subseteq {ℝ}^2$$
5	4	resabs1d	$$⊢A\subseteq ℝ\to {\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}$$
6	5	fveq2d	$$⊢A\subseteq ℝ\to \mathrm{MetOpen}\left({\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
7	2 6	eqtr4id	$$⊢A\subseteq ℝ\to J=\mathrm{MetOpen}\left({\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
8		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
9	8	rexmet	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{\infty Met}\left(ℝ\right)$$
10		eqid	$$⊢{\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}={\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}$$
11		eqid	$$⊢\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
12	8 11	tgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
13	1 12	eqtri	$$⊢R=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
14		eqid	$$⊢\mathrm{MetOpen}\left({\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}\right)=\mathrm{MetOpen}\left({\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
15	10 13 14	metrest	$$⊢\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{\infty Met}\left(ℝ\right)\wedge A\subseteq ℝ\right)\to R{\upharpoonright }_{𝑡}A=\mathrm{MetOpen}\left({\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
16	9 15	mpan	$$⊢A\subseteq ℝ\to R{\upharpoonright }_{𝑡}A=\mathrm{MetOpen}\left({\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
17	7 16	eqtr4d	$$⊢A\subseteq ℝ\to J=R{\upharpoonright }_{𝑡}A$$