This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = TopOpen ⁡ ℂ fld
rerest.2 ⊢ R = topGen ⁡ ran ⁡ .
Assertion rerest ⊢ A ⊆ ℝ → J ↾ 𝑡 A = R ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 tgioo2.1 ⊢ J = TopOpen ⁡ ℂ fld
2 rerest.2 ⊢ R = topGen ⁡ ran ⁡ .
3 1 tgioo2 ⊢ topGen ⁡ ran ⁡ . = J ↾ 𝑡 ℝ
4 2 3 eqtri ⊢ R = J ↾ 𝑡 ℝ
5 4 oveq1i ⊢ R ↾ 𝑡 A = J ↾ 𝑡 ℝ ↾ 𝑡 A
6 1 cnfldtop ⊢ J ∈ Top
7 reex ⊢ ℝ ∈ V
8 restabs ⊢ J ∈ Top ∧ A ⊆ ℝ ∧ ℝ ∈ V → J ↾ 𝑡 ℝ ↾ 𝑡 A = J ↾ 𝑡 A
9 6 7 8 mp3an13 ⊢ A ⊆ ℝ → J ↾ 𝑡 ℝ ↾ 𝑡 A = J ↾ 𝑡 A
10 5 9 eqtr2id ⊢ A ⊆ ℝ → J ↾ 𝑡 A = R ↾ 𝑡 A