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 )