Theorem xrrest

Description: The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Hypotheses	xrrest.1	$$⊢X=\mathrm{ordTop}\left(\le \right)$$
	xrrest.2	$$⊢R=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
Assertion	xrrest	$$⊢A\subseteq ℝ\to X{\upharpoonright }_{𝑡}A=R{\upharpoonright }_{𝑡}A$$

Proof

Step	Hyp	Ref	Expression
1		xrrest.1	$$⊢X=\mathrm{ordTop}\left(\le \right)$$
2		xrrest.2	$$⊢R=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3	1	oveq1i	$$⊢X{\upharpoonright }_{𝑡}ℝ=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
4	3	xrtgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=X{\upharpoonright }_{𝑡}ℝ$$
5	2 4	eqtri	$$⊢R=X{\upharpoonright }_{𝑡}ℝ$$
6	5	oveq1i	$$⊢R{\upharpoonright }_{𝑡}A=\left(X{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}A$$
7	1	fvexi	$$⊢X\in \mathrm{V}$$
8		reex	$$⊢ℝ\in \mathrm{V}$$
9		restabs	$$⊢\left(X\in \mathrm{V}\wedge A\subseteq ℝ\wedge ℝ\in \mathrm{V}\right)\to \left(X{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}A=X{\upharpoonright }_{𝑡}A$$
10	7 8 9	mp3an13	$$⊢A\subseteq ℝ\to \left(X{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}A=X{\upharpoonright }_{𝑡}A$$
11	6 10	eqtr2id	$$⊢A\subseteq ℝ\to X{\upharpoonright }_{𝑡}A=R{\upharpoonright }_{𝑡}A$$