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

Metamath Proof Explorer

Theorem txtop

Description: The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion txtop 
|- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( u e. R , v e. S |-> ( u X. v ) ) = ran ( u e. R , v e. S |-> ( u X. v ) )
2 1 txval 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
3 topbas 
 |-  ( R e. Top -> R e. TopBases )
4 topbas 
 |-  ( S e. Top -> S e. TopBases )
5 1 txbas 
 |-  ( ( R e. TopBases /\ S e. TopBases ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) e. TopBases )
6 3 4 5 syl2an 
 |-  ( ( R e. Top /\ S e. Top ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) e. TopBases )
7 tgcl 
 |-  ( ran ( u e. R , v e. S |-> ( u X. v ) ) e. TopBases -> ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) e. Top )
8 6 7 syl 
 |-  ( ( R e. Top /\ S e. Top ) -> ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) e. Top )
9 2 8 eqeltrd 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )