Theorem xpstopn

Description: The topology on a binary product of topological spaces, as we have defined it (transferring the indexed product topology on functions on { (/) , 1o } to ( X X. Y ) by the canonical bijection), coincides with the usual topological product (generated by a base of rectangles). (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	xpstps.t	|- T = ( R Xs. S )
	xpstopn.j	|- J = ( TopOpen ` R )
	xpstopn.k	|- K = ( TopOpen ` S )
	xpstopn.o	|- O = ( TopOpen ` T )
Assertion	xpstopn	|- ( ( R e. TopSp /\ S e. TopSp ) -> O = ( J tX K ) )

Proof

Step	Hyp	Ref	Expression
1		xpstps.t	|- T = ( R Xs. S )
2		xpstopn.j	|- J = ( TopOpen ` R )
3		xpstopn.k	|- K = ( TopOpen ` S )
4		xpstopn.o	|- O = ( TopOpen ` T )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6		eqid	|- ( Base ` S ) = ( Base ` S )
7		eqid	|- ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )
8	1 2 3 4 5 6 7	xpstopnlem2	|- ( ( R e. TopSp /\ S e. TopSp ) -> O = ( J tX K ) )