This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )