Theorem xrrest

Description: The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Hypotheses	xrrest.1	⊢ 𝑋 = ( ordTop ‘ ≤ )
	xrrest.2	⊢ 𝑅 = ( topGen ‘ ran (,) )
Assertion	xrrest	⊢ ( 𝐴 ⊆ ℝ → ( 𝑋 ↾t 𝐴 ) = ( 𝑅 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xrrest.1	⊢ 𝑋 = ( ordTop ‘ ≤ )
2		xrrest.2	⊢ 𝑅 = ( topGen ‘ ran (,) )
3	1	oveq1i	⊢ ( 𝑋 ↾t ℝ ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
4	3	xrtgioo	⊢ ( topGen ‘ ran (,) ) = ( 𝑋 ↾t ℝ )
5	2 4	eqtri	⊢ 𝑅 = ( 𝑋 ↾t ℝ )
6	5	oveq1i	⊢ ( 𝑅 ↾t 𝐴 ) = ( ( 𝑋 ↾t ℝ ) ↾t 𝐴 )
7	1	fvexi	⊢ 𝑋 ∈ V
8		reex	⊢ ℝ ∈ V
9		restabs	⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ⊆ ℝ ∧ ℝ ∈ V ) → ( ( 𝑋 ↾t ℝ ) ↾t 𝐴 ) = ( 𝑋 ↾t 𝐴 ) )
10	7 8 9	mp3an13	⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑋 ↾t ℝ ) ↾t 𝐴 ) = ( 𝑋 ↾t 𝐴 ) )
11	6 10	eqtr2id	⊢ ( 𝐴 ⊆ ℝ → ( 𝑋 ↾t 𝐴 ) = ( 𝑅 ↾t 𝐴 ) )