# Metamath Proof Explorer

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