Theorem xrrest2

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

	Ref	Expression
Hypotheses	xrrest2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	xrrest2.2	$$⊢X=\mathrm{ordTop}\left(\le \right)$$
Assertion	xrrest2	$$⊢A\subseteq ℝ\to J{\upharpoonright }_{𝑡}A=X{\upharpoonright }_{𝑡}A$$

Proof

Step	Hyp	Ref	Expression
1		xrrest2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		xrrest2.2	$$⊢X=\mathrm{ordTop}\left(\le \right)$$
3		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4	1 3	rerest	$$⊢A\subseteq ℝ\to J{\upharpoonright }_{𝑡}A=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}A$$
5	2 3	xrrest	$$⊢A\subseteq ℝ\to X{\upharpoonright }_{𝑡}A=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}A$$
6	4 5	eqtr4d	$$⊢A\subseteq ℝ\to J{\upharpoonright }_{𝑡}A=X{\upharpoonright }_{𝑡}A$$