Theorem tpr2uni

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=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
Assertion	tpr2uni	$$⊢\bigcup \left(J{\times }_{t}J\right)={ℝ}^2$$

Proof

Step	Hyp	Ref	Expression
1		tpr2tp.0	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2	1	tpr2tp	$$⊢J{\times }_{t}J\in \mathrm{TopOn}\left({ℝ}^2\right)$$
3	2	toponunii	$$⊢{ℝ}^2=\bigcup \left(J{\times }_{t}J\right)$$
4	3	eqcomi	$$⊢\bigcup \left(J{\times }_{t}J\right)={ℝ}^2$$