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 𝐴 ) )