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

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 ⊢ 𝑅 = ( topGen ‘ ran (,) )
resubmet.2 ⊢ 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) )
Assertion resubmet ( 𝐴 ⊆ ℝ → 𝐽 = ( 𝑅 ↾t 𝐴 ) )

Proof

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