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