Theorem txuni

Description: The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		txuni.1	$$⊢X=\bigcup R$$
2		txuni.2	$$⊢Y=\bigcup S$$
3	1	toptopon	$$⊢R\in \mathrm{Top}\leftrightarrow R\in \mathrm{TopOn}\left(X\right)$$
4	2	toptopon	$$⊢S\in \mathrm{Top}\leftrightarrow S\in \mathrm{TopOn}\left(Y\right)$$
5		txtopon	$$⊢\left(R\in \mathrm{TopOn}\left(X\right)\wedge S\in \mathrm{TopOn}\left(Y\right)\right)\to R{\times }_{t}S\in \mathrm{TopOn}\left(X\times Y\right)$$
6	3 4 5	syl2anb	$$⊢\left(R\in \mathrm{Top}\wedge S\in \mathrm{Top}\right)\to R{\times }_{t}S\in \mathrm{TopOn}\left(X\times Y\right)$$
7		toponuni	$$⊢R{\times }_{t}S\in \mathrm{TopOn}\left(X\times Y\right)\to X\times Y=\bigcup \left(R{\times }_{t}S\right)$$
8	6 7	syl	$$⊢\left(R\in \mathrm{Top}\wedge S\in \mathrm{Top}\right)\to X\times Y=\bigcup \left(R{\times }_{t}S\right)$$