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 × t J TopOn 2

Proof

Step Hyp Ref Expression
1 tpr2tp.0 J = topGen ran .
2 retopon topGen ran . TopOn
3 1 2 eqeltri J TopOn
4 txtopon J TopOn J TopOn J × t J TopOn 2
5 3 3 4 mp2an J × t J TopOn 2