Theorem rerest

Description: The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypotheses	tgioo2.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	rerest.2	⊢ 𝑅 = ( topGen ‘ ran (,) )
Assertion	rerest	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ↾t 𝐴 ) = ( 𝑅 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		tgioo2.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		rerest.2	⊢ 𝑅 = ( topGen ‘ ran (,) )
3	1	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( 𝐽 ↾t ℝ )
4	2 3	eqtri	⊢ 𝑅 = ( 𝐽 ↾t ℝ )
5	4	oveq1i	⊢ ( 𝑅 ↾t 𝐴 ) = ( ( 𝐽 ↾t ℝ ) ↾t 𝐴 )
6	1	cnfldtop	⊢ 𝐽 ∈ Top
7		reex	⊢ ℝ ∈ V
8		restabs	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ℝ ∧ ℝ ∈ V ) → ( ( 𝐽 ↾t ℝ ) ↾t 𝐴 ) = ( 𝐽 ↾t 𝐴 ) )
9	6 7 8	mp3an13	⊢ ( 𝐴 ⊆ ℝ → ( ( 𝐽 ↾t ℝ ) ↾t 𝐴 ) = ( 𝐽 ↾t 𝐴 ) )
10	5 9	syl5req	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ↾t 𝐴 ) = ( 𝑅 ↾t 𝐴 ) )