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

Metamath Proof Explorer

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 = TopOpen ⁡ ℂ fld
xrrest2.2 ⊢ X = ordTop ⁡ ≤
Assertion xrrest2 ⊢ A ⊆ ℝ → J ↾ 𝑡 A = X ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 xrrest2.1 ⊢ J = TopOpen ⁡ ℂ fld
2 xrrest2.2 ⊢ X = ordTop ⁡ ≤
3 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
4 1 3 rerest ⊢ A ⊆ ℝ → J ↾ 𝑡 A = topGen ⁡ ran ⁡ . ↾ 𝑡 A
5 2 3 xrrest ⊢ A ⊆ ℝ → X ↾ 𝑡 A = topGen ⁡ ran ⁡ . ↾ 𝑡 A
6 4 5 eqtr4d ⊢ A ⊆ ℝ → J ↾ 𝑡 A = X ↾ 𝑡 A