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	|- J = ( TopOpen ` CCfld )
	xrrest2.2	|- X = ( ordTop ` <_ )
Assertion	xrrest2	|- ( A C_ RR -> ( J |`t A ) = ( X |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		xrrest2.1	|- J = ( TopOpen ` CCfld )
2		xrrest2.2	|- X = ( ordTop ` <_ )
3		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
4	1 3	rerest	|- ( A C_ RR -> ( J |`t A ) = ( ( topGen ` ran (,) ) |`t A ) )
5	2 3	xrrest	|- ( A C_ RR -> ( X |`t A ) = ( ( topGen ` ran (,) ) |`t A ) )
6	4 5	eqtr4d	|- ( A C_ RR -> ( J |`t A ) = ( X |`t A ) )