Metamath Proof Explorer

Theorem resubmet

Description: The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses resubmet.1 ⊢ R = topGen ⁡ ran ⁡ .
resubmet.2 ⊢ J = MetOpen ⁡ abs ∘ − ↾ A × A
Assertion resubmet ⊢ A ⊆ ℝ → J = R ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 resubmet.1 ⊢ R = topGen ⁡ ran ⁡ .
2 resubmet.2 ⊢ J = MetOpen ⁡ abs ∘ − ↾ A × A
3 xpss12 ⊢ A ⊆ ℝ ∧ A ⊆ ℝ → A × A ⊆ ℝ 2
4 3 anidms ⊢ A ⊆ ℝ → A × A ⊆ ℝ 2
5 4 resabs1d ⊢ A ⊆ ℝ → abs ∘ − ↾ ℝ 2 ↾ A × A = abs ∘ − ↾ A × A
6 5 fveq2d ⊢ A ⊆ ℝ → MetOpen ⁡ abs ∘ − ↾ ℝ 2 ↾ A × A = MetOpen ⁡ abs ∘ − ↾ A × A
7 2 6 eqtr4id ⊢ A ⊆ ℝ → J = MetOpen ⁡ abs ∘ − ↾ ℝ 2 ↾ A × A
8 eqid ⊢ abs ∘ − ↾ ℝ 2 = abs ∘ − ↾ ℝ 2
9 8 rexmet ⊢ abs ∘ − ↾ ℝ 2 ∈ ∞Met ⁡ ℝ
10 eqid ⊢ abs ∘ − ↾ ℝ 2 ↾ A × A = abs ∘ − ↾ ℝ 2 ↾ A × A
11 eqid ⊢ MetOpen ⁡ abs ∘ − ↾ ℝ 2 = MetOpen ⁡ abs ∘ − ↾ ℝ 2
12 8 11 tgioo ⊢ topGen ⁡ ran ⁡ . = MetOpen ⁡ abs ∘ − ↾ ℝ 2
13 1 12 eqtri ⊢ R = MetOpen ⁡ abs ∘ − ↾ ℝ 2
14 eqid ⊢ MetOpen ⁡ abs ∘ − ↾ ℝ 2 ↾ A × A = MetOpen ⁡ abs ∘ − ↾ ℝ 2 ↾ A × A
15 10 13 14 metrest ⊢ abs ∘ − ↾ ℝ 2 ∈ ∞Met ⁡ ℝ ∧ A ⊆ ℝ → R ↾ 𝑡 A = MetOpen ⁡ abs ∘ − ↾ ℝ 2 ↾ A × A
16 9 15 mpan ⊢ A ⊆ ℝ → R ↾ 𝑡 A = MetOpen ⁡ abs ∘ − ↾ ℝ 2 ↾ A × A
17 7 16 eqtr4d ⊢ A ⊆ ℝ → J = R ↾ 𝑡 A