Metamath Proof Explorer


Theorem tpr2tp

Description: The usual topology on ( RR X. RR ) is the product topology of the usual topology on RR . (Contributed by Thierry Arnoux, 21-Sep-2017)

Ref Expression
Hypothesis tpr2tp.0
|- J = ( topGen ` ran (,) )
Assertion tpr2tp
|- ( J tX J ) e. ( TopOn ` ( RR X. RR ) )

Proof

Step Hyp Ref Expression
1 tpr2tp.0
 |-  J = ( topGen ` ran (,) )
2 retopon
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
3 1 2 eqeltri
 |-  J e. ( TopOn ` RR )
4 txtopon
 |-  ( ( J e. ( TopOn ` RR ) /\ J e. ( TopOn ` RR ) ) -> ( J tX J ) e. ( TopOn ` ( RR X. RR ) ) )
5 3 3 4 mp2an
 |-  ( J tX J ) e. ( TopOn ` ( RR X. RR ) )