This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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