# Metamath Proof Explorer

## Theorem xpstps

Description: A binary product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis xpstps.t
`|- T = ( R Xs. S )`
Assertion xpstps
`|- ( ( R e. TopSp /\ S e. TopSp ) -> T e. TopSp )`

### Proof

Step Hyp Ref Expression
1 xpstps.t
` |-  T = ( R Xs. S )`
2 eqid
` |-  ( Base ` R ) = ( Base ` R )`
3 eqid
` |-  ( Base ` S ) = ( Base ` S )`
4 simpl
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> R e. TopSp )`
5 simpr
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> S e. TopSp )`
6 eqid
` |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )`
7 eqid
` |-  ( Scalar ` R ) = ( Scalar ` R )`
8 eqid
` |-  ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )`
9 1 2 3 4 5 6 7 8 xpsval
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> T = ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )`
10 1 2 3 4 5 6 7 8 xpsrnbas
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )`
11 6 xpsff1o2
` |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )`
12 11 a1i
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) )`
13 f1ocnv
` |-  ( ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) )`
14 f1ofo
` |-  ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( ( Base ` R ) X. ( Base ` S ) ) )`
15 12 13 14 3syl
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( ( Base ` R ) X. ( Base ` S ) ) )`
16 fvexd
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( Scalar ` R ) e. _V )`
17 2on
` |-  2o e. On`
18 17 a1i
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> 2o e. On )`
19 xpscf
` |-  ( { <. (/) , R >. , <. 1o , S >. } : 2o --> TopSp <-> ( R e. TopSp /\ S e. TopSp ) )`
20 19 biimpri
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> { <. (/) , R >. , <. 1o , S >. } : 2o --> TopSp )`
21 8 16 18 20 prdstps
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. TopSp )`
22 9 10 15 21 imastps
` |-  ( ( R e. TopSp /\ S e. TopSp ) -> T e. TopSp )`