Theorem txtopi

Description: The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010)

	Ref	Expression
Hypotheses	txtopi.1	$$⊢R\in \mathrm{Top}$$
	txtopi.2	$$⊢S\in \mathrm{Top}$$
Assertion	txtopi	$$⊢R{\times }_{t}S\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		txtopi.1	$$⊢R\in \mathrm{Top}$$
2		txtopi.2	$$⊢S\in \mathrm{Top}$$
3		txtop	$$⊢\left(R\in \mathrm{Top}\wedge S\in \mathrm{Top}\right)\to R{\times }_{t}S\in \mathrm{Top}$$
4	1 2 3	mp2an	$$⊢R{\times }_{t}S\in \mathrm{Top}$$