Theorem txunii

Description: The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010)

	Ref	Expression
Hypotheses	txunii.1	$$⊢R\in \mathrm{Top}$$
	txunii.2	$$⊢S\in \mathrm{Top}$$
	txunii.3	$$⊢X=\bigcup R$$
	txunii.4	$$⊢Y=\bigcup S$$
Assertion	txunii	$$⊢X\times Y=\bigcup \left(R{\times }_{t}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		txunii.1	$$⊢R\in \mathrm{Top}$$
2		txunii.2	$$⊢S\in \mathrm{Top}$$
3		txunii.3	$$⊢X=\bigcup R$$
4		txunii.4	$$⊢Y=\bigcup S$$
5	3 4	txuni	$$⊢\left(R\in \mathrm{Top}\wedge S\in \mathrm{Top}\right)\to X\times Y=\bigcup \left(R{\times }_{t}S\right)$$
6	1 2 5	mp2an	$$⊢X\times Y=\bigcup \left(R{\times }_{t}S\right)$$