Theorem rerest

Description: The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypotheses	tgioo2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	rerest.2	$$⊢R=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
Assertion	rerest	$$⊢A\subseteq ℝ\to J{\upharpoonright }_{𝑡}A=R{\upharpoonright }_{𝑡}A$$

Proof

Step	Hyp	Ref	Expression
1		tgioo2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		rerest.2	$$⊢R=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3	1	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J{\upharpoonright }_{𝑡}ℝ$$
4	2 3	eqtri	$$⊢R=J{\upharpoonright }_{𝑡}ℝ$$
5	4	oveq1i	$$⊢R{\upharpoonright }_{𝑡}A=\left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}A$$
6	1	cnfldtop	$$⊢J\in \mathrm{Top}$$
7		reex	$$⊢ℝ\in \mathrm{V}$$
8		restabs	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq ℝ\wedge ℝ\in \mathrm{V}\right)\to \left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}A$$
9	6 7 8	mp3an13	$$⊢A\subseteq ℝ\to \left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}A$$
10	5 9	eqtr2id	$$⊢A\subseteq ℝ\to J{\upharpoonright }_{𝑡}A=R{\upharpoonright }_{𝑡}A$$