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 )
29 28 adantr 
 |-  ( ( 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 1oelpr 
 |-  1o e. { (/) , 1o }
35 34 24 eleqtrri 
 |-  1o e. 2o
36 fvco2 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ 1o e. 2o ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) = ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) )
37 12 35 36 sylancl 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) = ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) )
38 fvpr1o 
 |-  ( S e. TopSp -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
39 38 adantl 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
40 39 fveq2d 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) = ( TopOpen ` S ) )
41 40 3 eqtr4di 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) = K )
42 37 41 eqtrd 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) = K )
43 42 opeq2d 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> <. 1o , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) >. = <. 1o , K >. )
44 33 43 preq12d 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> { <. (/) , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` (/) ) >. , <. 1o , ( ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ` 1o ) >. } = { <. (/) , J >. , <. 1o , K >. } )
45 21 44 eqtr3d 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) = { <. (/) , J >. , <. 1o , K >. } )
46 45 fveq2d 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( Xt_ ` ( TopOpen o. { <. (/) , R >. , <. 1o , S >. } ) ) = ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) )
47 14 46 eqtrd 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) )
48 47 oveq1d 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) qTop `' F ) = ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) qTop `' F ) )
49 simpl 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> R e. TopSp )
50 simpr 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> S e. TopSp )
51 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
52 1 5 6 49 50 7 51 8 xpsval 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> T = ( `' F "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
53 1 5 6 49 50 7 51 8 xpsrnbas 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ran F = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
54 7 xpsff1o2 
 |-  F : ( X X. Y ) -1-1-onto-> ran F
55 f1ocnv 
 |-  ( F : ( X X. Y ) -1-1-onto-> ran F -> `' F : ran F -1-1-onto-> ( X X. Y ) )
56 54 55 mp1i 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> `' F : ran F -1-1-onto-> ( X X. Y ) )
57 f1ofo 
 |-  ( `' F : ran F -1-1-onto-> ( X X. Y ) -> `' F : ran F -onto-> ( X X. Y ) )
58 56 57 syl 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> `' F : ran F -onto-> ( X X. Y ) )
59 ovexd 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V )
60 52 53 58 59 13 4 imastopn 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> O = ( ( TopOpen ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) qTop `' F ) )
61 5 2 istps 
 |-  ( R e. TopSp <-> J e. ( TopOn ` X ) )
62 49 61 sylib 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> J e. ( TopOn ` X ) )
63 6 3 istps 
 |-  ( S e. TopSp <-> K e. ( TopOn ` Y ) )
64 50 63 sylib 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> K e. ( TopOn ` Y ) )
65 7 62 64 xpstopnlem1 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> F e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )
66 hmeocnv 
 |-  ( F e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) -> `' F e. ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) Homeo ( J tX K ) ) )
67 hmeoqtop 
 |-  ( `' F e. ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) Homeo ( J tX K ) ) -> ( J tX K ) = ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) qTop `' F ) )
68 65 66 67 3syl 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> ( J tX K ) = ( ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) qTop `' F ) )
69 48 60 68 3eqtr4d 
 |-  ( ( R e. TopSp /\ S e. TopSp ) -> O = ( J tX K ) )