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 e. Top
	txunii.2	|- S e. Top
	txunii.3	|- X = U. R
	txunii.4	|- Y = U. S
Assertion	txunii	|- ( X X. Y ) = U. ( R tX S )

Proof

Step	Hyp	Ref	Expression
1		txunii.1	|- R e. Top
2		txunii.2	|- S e. Top
3		txunii.3	|- X = U. R
4		txunii.4	|- Y = U. S
5	3 4	txuni	|- ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )
6	1 2 5	mp2an	|- ( X X. Y ) = U. ( R tX S )