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 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 )
40 39 adantl 
 |-  ( ( 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 ) )