Metamath Proof Explorer


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 fld
xrrest2.2 X = ordTop
Assertion xrrest2 A J 𝑡 A = X 𝑡 A

Proof

Step Hyp Ref Expression
1 xrrest2.1 J = TopOpen fld
2 xrrest2.2 X = ordTop
3 eqid topGen ran . = topGen ran .
4 1 3 rerest A J 𝑡 A = topGen ran . 𝑡 A
5 2 3 xrrest A X 𝑡 A = topGen ran . 𝑡 A
6 4 5 eqtr4d A J 𝑡 A = X 𝑡 A