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 \times_{t} J \in TopOn (ℝ^{2})$

Proof

Step	Hyp	Ref	Expression
1		tpr2tp.0	$⊢ J = topGen (ran (.))$
2		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
3	1 2	eqeltri	$⊢ J \in TopOn (ℝ)$
4		txtopon	$⊢ (J \in TopOn (ℝ) \land J \in TopOn (ℝ)) \to J \times_{t} J \in TopOn (ℝ^{2})$
5	3 3 4	mp2an	$⊢ J \times_{t} J \in TopOn (ℝ^{2})$