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 )