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 = U. R
	txuni.2	|- Y = U. S
Assertion	txuni	|- ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )

Proof

Step	Hyp	Ref	Expression
1		txuni.1	|- X = U. R
2		txuni.2	|- Y = U. S
3	1	toptopon	|- ( R e. Top <-> R e. ( TopOn ` X ) )
4	2	toptopon	|- ( S e. Top <-> S e. ( TopOn ` Y ) )
5		txtopon	|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) )
6	3 4 5	syl2anb	|- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) )
7		toponuni	|- ( ( R tX S ) e. ( TopOn ` ( X X. Y ) ) -> ( X X. Y ) = U. ( R tX S ) )
8	6 7	syl	|- ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )