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