# Metamath Proof Explorer

## 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}{↾}_{𝑡}{A}={R}{↾}_{𝑡}{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}{↾}_{𝑡}ℝ$
4 2 3 eqtri ${⊢}{R}={J}{↾}_{𝑡}ℝ$
5 4 oveq1i ${⊢}{R}{↾}_{𝑡}{A}=\left({J}{↾}_{𝑡}ℝ\right){↾}_{𝑡}{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}{↾}_{𝑡}ℝ\right){↾}_{𝑡}{A}={J}{↾}_{𝑡}{A}$
9 6 7 8 mp3an13 ${⊢}{A}\subseteq ℝ\to \left({J}{↾}_{𝑡}ℝ\right){↾}_{𝑡}{A}={J}{↾}_{𝑡}{A}$
10 5 9 syl5req ${⊢}{A}\subseteq ℝ\to {J}{↾}_{𝑡}{A}={R}{↾}_{𝑡}{A}$