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

Metamath Proof Explorer

Theorem resubmet

Description: The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses resubmet.1 
|- R = ( topGen ` ran (,) )
resubmet.2 
|- J = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )
Assertion resubmet 
|- ( A C_ RR -> J = ( R |`t A ) )

Proof

Step Hyp Ref Expression
1 resubmet.1 
 |-  R = ( topGen ` ran (,) )
2 resubmet.2 
 |-  J = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )
3 xpss12 
 |-  ( ( A C_ RR /\ A C_ RR ) -> ( A X. A ) C_ ( RR X. RR ) )
4 3 anidms 
 |-  ( A C_ RR -> ( A X. A ) C_ ( RR X. RR ) )
5 4 resabs1d 
 |-  ( A C_ RR -> ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) = ( ( abs o. - ) |` ( A X. A ) ) )
6 5 fveq2d 
 |-  ( A C_ RR -> ( MetOpen ` ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) )
7 2 6 eqtr4id 
 |-  ( A C_ RR -> J = ( MetOpen ` ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) ) )
8 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
9 8 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
10 eqid 
 |-  ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) = ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) )
11 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
12 8 11 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
13 1 12 eqtri 
 |-  R = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
14 eqid 
 |-  ( MetOpen ` ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) )
15 10 13 14 metrest 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ A C_ RR ) -> ( R |`t A ) = ( MetOpen ` ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) ) )
16 9 15 mpan 
 |-  ( A C_ RR -> ( R |`t A ) = ( MetOpen ` ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( A X. A ) ) ) )
17 7 16 eqtr4d 
 |-  ( A C_ RR -> J = ( R |`t A ) )