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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	xrrest2.2	⊢ 𝑋 = ( ordTop ‘ ≤ )
Assertion	xrrest2	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ↾t 𝐴 ) = ( 𝑋 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xrrest2.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		xrrest2.2	⊢ 𝑋 = ( ordTop ‘ ≤ )
3		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
4	1 3	rerest	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) )
5	2 3	xrrest	⊢ ( 𝐴 ⊆ ℝ → ( 𝑋 ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) )
6	4 5	eqtr4d	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ↾t 𝐴 ) = ( 𝑋 ↾t 𝐴 ) )