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	|- X = ( ordTop ` <_ )
	xrrest.2	|- R = ( topGen ` ran (,) )
Assertion	xrrest	|- ( A C_ RR -> ( X |`t A ) = ( R |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		xrrest.1	|- X = ( ordTop ` <_ )
2		xrrest.2	|- R = ( topGen ` ran (,) )
3	1	oveq1i	|- ( X |`t RR ) = ( ( ordTop ` <_ ) |`t RR )
4	3	xrtgioo	|- ( topGen ` ran (,) ) = ( X |`t RR )
5	2 4	eqtri	|- R = ( X |`t RR )
6	5	oveq1i	|- ( R |`t A ) = ( ( X |`t RR ) |`t A )
7	1	fvexi	|- X e. _V
8		reex	|- RR e. _V
9		restabs	|- ( ( X e. _V /\ A C_ RR /\ RR e. _V ) -> ( ( X |`t RR ) |`t A ) = ( X |`t A ) )
10	7 8 9	mp3an13	|- ( A C_ RR -> ( ( X |`t RR ) |`t A ) = ( X |`t A ) )
11	6 10	eqtr2id	|- ( A C_ RR -> ( X |`t A ) = ( R |`t A ) )