Metamath Proof Explorer


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 ) )