# Metamath Proof Explorer

## Theorem xpstopnlem2

Description: Lemma for xpstopn . (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 )
xpstopnlem.x
|- X = ( Base ` R )
xpstopnlem.y
|- Y = ( Base ` S )
xpstopnlem.f
|- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
Assertion xpstopnlem2
|- ( ( 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 xpstopnlem.x
|-  X = ( Base ` R )
6 xpstopnlem.y
|-  Y = ( Base ` S )
7 xpstopnlem.f
|-  F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
8 eqid
|-  ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
9 fvexd
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( Scalar ` R ) e. _V )
10 2on
|-  2o e. On
11 10 a1i
|-  ( ( R e. TopSp /\ S e. TopSp ) -> 2o e. On )
12 fnpr2o
|-  ( ( R e. TopSp /\ S e. TopSp ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
13 eqid
|-  ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
14 8 9 11 12 13 prdstopn
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Xt_ ` ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ) )
15 topnfn
|-  TopOpen Fn _V
16 dffn2
|-  ( { <. (/) , R >. , <. 1o , S >. } Fn 2o <-> { <. (/) , R >. , <. 1o , S >. } : 2o --> _V )
17 12 16 sylib
|-  ( ( R e. TopSp /\ S e. TopSp ) -> { <. (/) , R >. , <. 1o , S >. } : 2o --> _V )
18 fnfco
|-  ( ( TopOpen Fn _V /\ { <. (/) , R >. , <. 1o , S >. } : 2o --> _V ) -> ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) Fn 2o )
19 15 17 18 sylancr
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) Fn 2o )
20 xpsfeq
|-  ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) Fn 2o -> { <. (/) , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) >. , <. 1o , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) >. } = ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) )
21 19 20 syl
|-  ( ( R e. TopSp /\ S e. TopSp ) -> { <. (/) , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) >. , <. 1o , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) >. } = ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) )
22 0ex
|-  (/) e. _V
23 22 prid1
|-  (/) e. { (/) , 1o }
24 df2o3
|-  2o = { (/) , 1o }
25 23 24 eleqtrri
|-  (/) e. 2o
26 fvco2
|-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ (/) e. 2o ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) = ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) )
27 12 25 26 sylancl
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) = ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) )
28 fvpr0o
|-  ( R e. TopSp -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R )
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R )
30 29 fveq2d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) = ( TopOpen ` R ) )
31 30 2 eqtr4di
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) = J )
32 27 31 eqtrd
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) = J )
33 32 opeq2d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> <. (/) , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) >. = <. (/) , J >. )
34 1oex
|-  1o e. _V
35 34 prid2
|-  1o e. { (/) , 1o }
36 35 24 eleqtrri
|-  1o e. 2o
37 fvco2
|-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ 1o e. 2o ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) = ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) )
38 12 36 37 sylancl
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) = ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) )
39 fvpr1o
|-  ( S e. TopSp -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
41 40 fveq2d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) = ( TopOpen ` S ) )
42 41 3 eqtr4di
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) = K )
43 38 42 eqtrd
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) = K )
44 43 opeq2d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> <. 1o , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) >. = <. 1o , K >. )
45 33 44 preq12d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> { <. (/) , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) >. , <. 1o , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) >. } = { <. (/) , J >. , <. 1o , K >. } )
46 21 45 eqtr3d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) = { <. (/) , J >. , <. 1o , K >. } )
47 46 fveq2d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( Xt_ ` ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ) = ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) )
48 14 47 eqtrd
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) )
49 48 oveq1d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) qTop `' F ) = ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) qTop `' F ) )
50 simpl
|-  ( ( R e. TopSp /\ S e. TopSp ) -> R e. TopSp )
51 simpr
|-  ( ( R e. TopSp /\ S e. TopSp ) -> S e. TopSp )
52 eqid
|-  ( Scalar ` R ) = ( Scalar ` R )
53 1 5 6 50 51 7 52 8 xpsval
|-  ( ( R e. TopSp /\ S e. TopSp ) -> T = ( `' F "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
54 1 5 6 50 51 7 52 8 xpsrnbas
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ran F = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
55 7 xpsff1o2
|-  F : ( X X. Y ) -1-1-onto-> ran F
56 f1ocnv
|-  ( F : ( X X. Y ) -1-1-onto-> ran F -> `' F : ran F -1-1-onto-> ( X X. Y ) )
57 55 56 mp1i
|-  ( ( R e. TopSp /\ S e. TopSp ) -> `' F : ran F -1-1-onto-> ( X X. Y ) )
58 f1ofo
|-  ( `' F : ran F -1-1-onto-> ( X X. Y ) -> `' F : ran F -onto-> ( X X. Y ) )
59 57 58 syl
|-  ( ( R e. TopSp /\ S e. TopSp ) -> `' F : ran F -onto-> ( X X. Y ) )
60 ovexd
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V )
61 53 54 59 60 13 4 imastopn
|-  ( ( R e. TopSp /\ S e. TopSp ) -> O = ( ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) qTop `' F ) )
62 5 2 istps
|-  ( R e. TopSp <-> J e. ( TopOn ` X ) )
63 50 62 sylib
|-  ( ( R e. TopSp /\ S e. TopSp ) -> J e. ( TopOn ` X ) )
64 6 3 istps
|-  ( S e. TopSp <-> K e. ( TopOn ` Y ) )
65 51 64 sylib
|-  ( ( R e. TopSp /\ S e. TopSp ) -> K e. ( TopOn ` Y ) )
66 7 63 65 xpstopnlem1
|-  ( ( R e. TopSp /\ S e. TopSp ) -> F e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )
67 hmeocnv
|-  ( F e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) -> `' F e. ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) Homeo ( J tX K ) ) )
68 hmeoqtop
|-  ( `' F e. ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) Homeo ( J tX K ) ) -> ( J tX K ) = ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) qTop `' F ) )
69 66 67 68 3syl
|-  ( ( R e. TopSp /\ S e. TopSp ) -> ( J tX K ) = ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) qTop `' F ) )
70 49 61 69 3eqtr4d
|-  ( ( R e. TopSp /\ S e. TopSp ) -> O = ( J tX K ) )