Metamath Proof Explorer

Theorem txtopon

Description: The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion txtopon 
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( R e. ( TopOn ` X ) -> R e. Top )
2 topontop 
 |-  ( S e. ( TopOn ` Y ) -> S e. Top )
3 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
4 1 2 3 syl2an 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. Top )
5 eqid 
 |-  ran ( u e. R , v e. S |-> ( u X. v ) ) = ran ( u e. R , v e. S |-> ( u X. v ) )
6 eqid 
 |-  U. R = U. R
7 eqid 
 |-  U. S = U. S
8 5 6 7 txuni2 
 |-  ( U. R X. U. S ) = U. ran ( u e. R , v e. S |-> ( u X. v ) )
9 toponuni 
 |-  ( R e. ( TopOn ` X ) -> X = U. R )
10 toponuni 
 |-  ( S e. ( TopOn ` Y ) -> Y = U. S )
11 xpeq12 
 |-  ( ( X = U. R /\ Y = U. S ) -> ( X X. Y ) = ( U. R X. U. S ) )
12 9 10 11 syl2an 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( X X. Y ) = ( U. R X. U. S ) )
13 5 txbasex 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V )
14 unitg 
 |-  ( ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V -> U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) = U. ran ( u e. R , v e. S |-> ( u X. v ) ) )
15 13 14 syl 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) = U. ran ( u e. R , v e. S |-> ( u X. v ) ) )
16 8 12 15 3eqtr4a 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( X X. Y ) = U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
17 5 txval 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
18 17 unieqd 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> U. ( R tX S ) = U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
19 16 18 eqtr4d 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( X X. Y ) = U. ( R tX S ) )
20 istopon 
 |-  ( ( R tX S ) e. ( TopOn ` ( X X. Y ) ) <-> ( ( R tX S ) e. Top /\ ( X X. Y ) = U. ( R tX S ) ) )
21 4 19 20 sylanbrc 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) )