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

Metamath Proof Explorer

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 = ordTop ⁡ ≤
xrrest.2 ⊢ R = topGen ⁡ ran ⁡ .
Assertion xrrest ⊢ A ⊆ ℝ → X ↾ 𝑡 A = R ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 xrrest.1 ⊢ X = ordTop ⁡ ≤
2 xrrest.2 ⊢ R = topGen ⁡ ran ⁡ .
3 1 oveq1i ⊢ X ↾ 𝑡 ℝ = ordTop ⁡ ≤ ↾ 𝑡 ℝ
4 3 xrtgioo ⊢ topGen ⁡ ran ⁡ . = X ↾ 𝑡 ℝ
5 2 4 eqtri ⊢ R = X ↾ 𝑡 ℝ
6 5 oveq1i ⊢ R ↾ 𝑡 A = X ↾ 𝑡 ℝ ↾ 𝑡 A
7 1 fvexi ⊢ X ∈ V
8 reex ⊢ ℝ ∈ V
9 restabs ⊢ X ∈ V ∧ A ⊆ ℝ ∧ ℝ ∈ V → X ↾ 𝑡 ℝ ↾ 𝑡 A = X ↾ 𝑡 A
10 7 8 9 mp3an13 ⊢ A ⊆ ℝ → X ↾ 𝑡 ℝ ↾ 𝑡 A = X ↾ 𝑡 A
11 6 10 eqtr2id ⊢ A ⊆ ℝ → X ↾ 𝑡 A = R ↾ 𝑡 A