# Metamath Proof Explorer

## Theorem txhmeo

Description: Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses txhmeo.1
`|- X = U. J`
txhmeo.2
`|- Y = U. K`
txhmeo.3
`|- ( ph -> F e. ( J Homeo L ) )`
txhmeo.4
`|- ( ph -> G e. ( K Homeo M ) )`
Assertion txhmeo
`|- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )`

### Proof

Step Hyp Ref Expression
1 txhmeo.1
` |-  X = U. J`
2 txhmeo.2
` |-  Y = U. K`
3 txhmeo.3
` |-  ( ph -> F e. ( J Homeo L ) )`
4 txhmeo.4
` |-  ( ph -> G e. ( K Homeo M ) )`
5 hmeocn
` |-  ( F e. ( J Homeo L ) -> F e. ( J Cn L ) )`
6 3 5 syl
` |-  ( ph -> F e. ( J Cn L ) )`
7 cntop1
` |-  ( F e. ( J Cn L ) -> J e. Top )`
8 6 7 syl
` |-  ( ph -> J e. Top )`
9 1 toptopon
` |-  ( J e. Top <-> J e. ( TopOn ` X ) )`
10 8 9 sylib
` |-  ( ph -> J e. ( TopOn ` X ) )`
11 hmeocn
` |-  ( G e. ( K Homeo M ) -> G e. ( K Cn M ) )`
12 4 11 syl
` |-  ( ph -> G e. ( K Cn M ) )`
13 cntop1
` |-  ( G e. ( K Cn M ) -> K e. Top )`
14 12 13 syl
` |-  ( ph -> K e. Top )`
15 2 toptopon
` |-  ( K e. Top <-> K e. ( TopOn ` Y ) )`
16 14 15 sylib
` |-  ( ph -> K e. ( TopOn ` Y ) )`
17 10 16 cnmpt1st
` |-  ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )`
18 10 16 17 6 cnmpt21f
` |-  ( ph -> ( x e. X , y e. Y |-> ( F ` x ) ) e. ( ( J tX K ) Cn L ) )`
19 10 16 cnmpt2nd
` |-  ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )`
20 10 16 19 12 cnmpt21f
` |-  ( ph -> ( x e. X , y e. Y |-> ( G ` y ) ) e. ( ( J tX K ) Cn M ) )`
21 10 16 18 20 cnmpt2t
` |-  ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )`
22 vex
` |-  x e. _V`
23 vex
` |-  y e. _V`
24 22 23 op1std
` |-  ( u = <. x , y >. -> ( 1st ` u ) = x )`
25 24 fveq2d
` |-  ( u = <. x , y >. -> ( F ` ( 1st ` u ) ) = ( F ` x ) )`
26 22 23 op2ndd
` |-  ( u = <. x , y >. -> ( 2nd ` u ) = y )`
27 26 fveq2d
` |-  ( u = <. x , y >. -> ( G ` ( 2nd ` u ) ) = ( G ` y ) )`
28 25 27 opeq12d
` |-  ( u = <. x , y >. -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. = <. ( F ` x ) , ( G ` y ) >. )`
29 28 mpompt
` |-  ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. ) = ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. )`
30 29 eqcomi
` |-  ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. )`
31 eqid
` |-  U. L = U. L`
32 1 31 cnf
` |-  ( F e. ( J Cn L ) -> F : X --> U. L )`
33 6 32 syl
` |-  ( ph -> F : X --> U. L )`
34 xp1st
` |-  ( u e. ( X X. Y ) -> ( 1st ` u ) e. X )`
35 ffvelrn
` |-  ( ( F : X --> U. L /\ ( 1st ` u ) e. X ) -> ( F ` ( 1st ` u ) ) e. U. L )`
36 33 34 35 syl2an
` |-  ( ( ph /\ u e. ( X X. Y ) ) -> ( F ` ( 1st ` u ) ) e. U. L )`
37 eqid
` |-  U. M = U. M`
38 2 37 cnf
` |-  ( G e. ( K Cn M ) -> G : Y --> U. M )`
39 12 38 syl
` |-  ( ph -> G : Y --> U. M )`
40 xp2nd
` |-  ( u e. ( X X. Y ) -> ( 2nd ` u ) e. Y )`
41 ffvelrn
` |-  ( ( G : Y --> U. M /\ ( 2nd ` u ) e. Y ) -> ( G ` ( 2nd ` u ) ) e. U. M )`
42 39 40 41 syl2an
` |-  ( ( ph /\ u e. ( X X. Y ) ) -> ( G ` ( 2nd ` u ) ) e. U. M )`
43 36 42 opelxpd
` |-  ( ( ph /\ u e. ( X X. Y ) ) -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. e. ( U. L X. U. M ) )`
44 1 31 hmeof1o
` |-  ( F e. ( J Homeo L ) -> F : X -1-1-onto-> U. L )`
45 3 44 syl
` |-  ( ph -> F : X -1-1-onto-> U. L )`
46 f1ocnv
` |-  ( F : X -1-1-onto-> U. L -> `' F : U. L -1-1-onto-> X )`
47 f1of
` |-  ( `' F : U. L -1-1-onto-> X -> `' F : U. L --> X )`
48 45 46 47 3syl
` |-  ( ph -> `' F : U. L --> X )`
49 xp1st
` |-  ( v e. ( U. L X. U. M ) -> ( 1st ` v ) e. U. L )`
50 ffvelrn
` |-  ( ( `' F : U. L --> X /\ ( 1st ` v ) e. U. L ) -> ( `' F ` ( 1st ` v ) ) e. X )`
51 48 49 50 syl2an
` |-  ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' F ` ( 1st ` v ) ) e. X )`
52 2 37 hmeof1o
` |-  ( G e. ( K Homeo M ) -> G : Y -1-1-onto-> U. M )`
53 4 52 syl
` |-  ( ph -> G : Y -1-1-onto-> U. M )`
54 f1ocnv
` |-  ( G : Y -1-1-onto-> U. M -> `' G : U. M -1-1-onto-> Y )`
55 f1of
` |-  ( `' G : U. M -1-1-onto-> Y -> `' G : U. M --> Y )`
56 53 54 55 3syl
` |-  ( ph -> `' G : U. M --> Y )`
57 xp2nd
` |-  ( v e. ( U. L X. U. M ) -> ( 2nd ` v ) e. U. M )`
58 ffvelrn
` |-  ( ( `' G : U. M --> Y /\ ( 2nd ` v ) e. U. M ) -> ( `' G ` ( 2nd ` v ) ) e. Y )`
59 56 57 58 syl2an
` |-  ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' G ` ( 2nd ` v ) ) e. Y )`
60 51 59 opelxpd
` |-  ( ( ph /\ v e. ( U. L X. U. M ) ) -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. e. ( X X. Y ) )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> F : X -1-1-onto-> U. L )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` u ) e. X )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` v ) e. U. L )`
64 f1ocnvfvb
` |-  ( ( F : X -1-1-onto-> U. L /\ ( 1st ` u ) e. X /\ ( 1st ` v ) e. U. L ) -> ( ( F ` ( 1st ` u ) ) = ( 1st ` v ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) ) )`
65 61 62 63 64 syl3anc
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( F ` ( 1st ` u ) ) = ( 1st ` v ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) ) )`
66 eqcom
` |-  ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( F ` ( 1st ` u ) ) = ( 1st ` v ) )`
67 eqcom
` |-  ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) )`
68 65 66 67 3bitr4g
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) ) )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> G : Y -1-1-onto-> U. M )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` u ) e. Y )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` v ) e. U. M )`
72 f1ocnvfvb
` |-  ( ( G : Y -1-1-onto-> U. M /\ ( 2nd ` u ) e. Y /\ ( 2nd ` v ) e. U. M ) -> ( ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) ) )`
73 69 70 71 72 syl3anc
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) ) )`
74 eqcom
` |-  ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) )`
75 eqcom
` |-  ( ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) )`
76 73 74 75 3bitr4g
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) )`
77 68 76 anbi12d
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )`
78 eqop
` |-  ( v e. ( U. L X. U. M ) -> ( v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. <-> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) ) )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. <-> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) ) )`
80 eqop
` |-  ( u e. ( X X. Y ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )`
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )`
82 77 79 81 3bitr4rd
` |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. ) )`
83 30 43 60 82 f1ocnv2d
` |-  ( ph -> ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) : ( X X. Y ) -1-1-onto-> ( U. L X. U. M ) /\ `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) ) )`
84 83 simprd
` |-  ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) )`
85 vex
` |-  z e. _V`
86 vex
` |-  w e. _V`
87 85 86 op1std
` |-  ( v = <. z , w >. -> ( 1st ` v ) = z )`
88 87 fveq2d
` |-  ( v = <. z , w >. -> ( `' F ` ( 1st ` v ) ) = ( `' F ` z ) )`
89 85 86 op2ndd
` |-  ( v = <. z , w >. -> ( 2nd ` v ) = w )`
90 89 fveq2d
` |-  ( v = <. z , w >. -> ( `' G ` ( 2nd ` v ) ) = ( `' G ` w ) )`
91 88 90 opeq12d
` |-  ( v = <. z , w >. -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. = <. ( `' F ` z ) , ( `' G ` w ) >. )`
92 91 mpompt
` |-  ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) = ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. )`
93 84 92 eqtrdi
` |-  ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) )`
94 cntop2
` |-  ( F e. ( J Cn L ) -> L e. Top )`
95 6 94 syl
` |-  ( ph -> L e. Top )`
96 31 toptopon
` |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )`
97 95 96 sylib
` |-  ( ph -> L e. ( TopOn ` U. L ) )`
98 cntop2
` |-  ( G e. ( K Cn M ) -> M e. Top )`
99 12 98 syl
` |-  ( ph -> M e. Top )`
100 37 toptopon
` |-  ( M e. Top <-> M e. ( TopOn ` U. M ) )`
101 99 100 sylib
` |-  ( ph -> M e. ( TopOn ` U. M ) )`
102 97 101 cnmpt1st
` |-  ( ph -> ( z e. U. L , w e. U. M |-> z ) e. ( ( L tX M ) Cn L ) )`
103 hmeocnvcn
` |-  ( F e. ( J Homeo L ) -> `' F e. ( L Cn J ) )`
104 3 103 syl
` |-  ( ph -> `' F e. ( L Cn J ) )`
105 97 101 102 104 cnmpt21f
` |-  ( ph -> ( z e. U. L , w e. U. M |-> ( `' F ` z ) ) e. ( ( L tX M ) Cn J ) )`
106 97 101 cnmpt2nd
` |-  ( ph -> ( z e. U. L , w e. U. M |-> w ) e. ( ( L tX M ) Cn M ) )`
107 hmeocnvcn
` |-  ( G e. ( K Homeo M ) -> `' G e. ( M Cn K ) )`
108 4 107 syl
` |-  ( ph -> `' G e. ( M Cn K ) )`
109 97 101 106 108 cnmpt21f
` |-  ( ph -> ( z e. U. L , w e. U. M |-> ( `' G ` w ) ) e. ( ( L tX M ) Cn K ) )`
110 97 101 105 109 cnmpt2t
` |-  ( ph -> ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )`
111 93 110 eqeltrd
` |-  ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )`
112 ishmeo
` |-  ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) <-> ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) /\ `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) ) )`
113 21 111 112 sylanbrc
` |-  ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )`