ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  txhmeo Unicode version

Theorem txhmeo 13113
Description: Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
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
Ref Expression
txhmeo  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |-> 
<. ( F `  x
) ,  ( G `
 y ) >.
)  e.  ( ( J  tX  K )
Homeo ( L  tX  M
) ) )
Distinct variable groups:    x, y, F   
x, J, y    x, K, y    ph, x, y   
x, G, y    x, L, y    x, X, y   
x, Y, y    x, M, y

Proof of Theorem txhmeo
Dummy variables  v  u  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txhmeo.3 . . . . . 6  |-  ( ph  ->  F  e.  ( J
Homeo L ) )
2 hmeocn 13099 . . . . . 6  |-  ( F  e.  ( J Homeo L )  ->  F  e.  ( J  Cn  L
) )
31, 2syl 14 . . . . 5  |-  ( ph  ->  F  e.  ( J  Cn  L ) )
4 cntop1 12995 . . . . 5  |-  ( F  e.  ( J  Cn  L )  ->  J  e.  Top )
53, 4syl 14 . . . 4  |-  ( ph  ->  J  e.  Top )
6 txhmeo.1 . . . . 5  |-  X  = 
U. J
76toptopon 12810 . . . 4  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
85, 7sylib 121 . . 3  |-  ( ph  ->  J  e.  (TopOn `  X ) )
9 txhmeo.4 . . . . . 6  |-  ( ph  ->  G  e.  ( K
Homeo M ) )
10 hmeocn 13099 . . . . . 6  |-  ( G  e.  ( K Homeo M )  ->  G  e.  ( K  Cn  M
) )
119, 10syl 14 . . . . 5  |-  ( ph  ->  G  e.  ( K  Cn  M ) )
12 cntop1 12995 . . . . 5  |-  ( G  e.  ( K  Cn  M )  ->  K  e.  Top )
1311, 12syl 14 . . . 4  |-  ( ph  ->  K  e.  Top )
14 txhmeo.2 . . . . 5  |-  Y  = 
U. K
1514toptopon 12810 . . . 4  |-  ( K  e.  Top  <->  K  e.  (TopOn `  Y ) )
1613, 15sylib 121 . . 3  |-  ( ph  ->  K  e.  (TopOn `  Y ) )
178, 16cnmpt1st 13082 . . . 4  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  x )  e.  ( ( J  tX  K
)  Cn  J ) )
188, 16, 17, 3cnmpt21f 13086 . . 3  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  ( F `  x
) )  e.  ( ( J  tX  K
)  Cn  L ) )
198, 16cnmpt2nd 13083 . . . 4  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  y )  e.  ( ( J  tX  K
)  Cn  K ) )
208, 16, 19, 11cnmpt21f 13086 . . 3  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  ( G `  y
) )  e.  ( ( J  tX  K
)  Cn  M ) )
218, 16, 18, 20cnmpt2t 13087 . 2  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |-> 
<. ( F `  x
) ,  ( G `
 y ) >.
)  e.  ( ( J  tX  K )  Cn  ( L  tX  M ) ) )
22 vex 2733 . . . . . . . . . . 11  |-  x  e. 
_V
23 vex 2733 . . . . . . . . . . 11  |-  y  e. 
_V
2422, 23op1std 6127 . . . . . . . . . 10  |-  ( u  =  <. x ,  y
>.  ->  ( 1st `  u
)  =  x )
2524fveq2d 5500 . . . . . . . . 9  |-  ( u  =  <. x ,  y
>.  ->  ( F `  ( 1st `  u ) )  =  ( F `
 x ) )
2622, 23op2ndd 6128 . . . . . . . . . 10  |-  ( u  =  <. x ,  y
>.  ->  ( 2nd `  u
)  =  y )
2726fveq2d 5500 . . . . . . . . 9  |-  ( u  =  <. x ,  y
>.  ->  ( G `  ( 2nd `  u ) )  =  ( G `
 y ) )
2825, 27opeq12d 3773 . . . . . . . 8  |-  ( u  =  <. x ,  y
>.  ->  <. ( F `  ( 1st `  u ) ) ,  ( G `
 ( 2nd `  u
) ) >.  =  <. ( F `  x ) ,  ( G `  y ) >. )
2928mpompt 5945 . . . . . . 7  |-  ( u  e.  ( X  X.  Y )  |->  <. ( F `  ( 1st `  u ) ) ,  ( G `  ( 2nd `  u ) )
>. )  =  (
x  e.  X , 
y  e.  Y  |->  <.
( F `  x
) ,  ( G `
 y ) >.
)
3029eqcomi 2174 . . . . . 6  |-  ( x  e.  X ,  y  e.  Y  |->  <. ( F `  x ) ,  ( G `  y ) >. )  =  ( u  e.  ( X  X.  Y
)  |->  <. ( F `  ( 1st `  u ) ) ,  ( G `
 ( 2nd `  u
) ) >. )
31 eqid 2170 . . . . . . . . . 10  |-  U. L  =  U. L
326, 31cnf 12998 . . . . . . . . 9  |-  ( F  e.  ( J  Cn  L )  ->  F : X --> U. L )
333, 32syl 14 . . . . . . . 8  |-  ( ph  ->  F : X --> U. L
)
34 xp1st 6144 . . . . . . . 8  |-  ( u  e.  ( X  X.  Y )  ->  ( 1st `  u )  e.  X )
35 ffvelrn 5629 . . . . . . . 8  |-  ( ( F : X --> U. L  /\  ( 1st `  u
)  e.  X )  ->  ( F `  ( 1st `  u ) )  e.  U. L
)
3633, 34, 35syl2an 287 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( X  X.  Y
) )  ->  ( F `  ( 1st `  u ) )  e. 
U. L )
37 eqid 2170 . . . . . . . . . 10  |-  U. M  =  U. M
3814, 37cnf 12998 . . . . . . . . 9  |-  ( G  e.  ( K  Cn  M )  ->  G : Y --> U. M )
3911, 38syl 14 . . . . . . . 8  |-  ( ph  ->  G : Y --> U. M
)
40 xp2nd 6145 . . . . . . . 8  |-  ( u  e.  ( X  X.  Y )  ->  ( 2nd `  u )  e.  Y )
41 ffvelrn 5629 . . . . . . . 8  |-  ( ( G : Y --> U. M  /\  ( 2nd `  u
)  e.  Y )  ->  ( G `  ( 2nd `  u ) )  e.  U. M
)
4239, 40, 41syl2an 287 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( X  X.  Y
) )  ->  ( G `  ( 2nd `  u ) )  e. 
U. M )
4336, 42opelxpd 4644 . . . . . 6  |-  ( (
ph  /\  u  e.  ( X  X.  Y
) )  ->  <. ( F `  ( 1st `  u ) ) ,  ( G `  ( 2nd `  u ) )
>.  e.  ( U. L  X.  U. M ) )
446, 31hmeof1o 13103 . . . . . . . . . 10  |-  ( F  e.  ( J Homeo L )  ->  F : X
-1-1-onto-> U. L )
451, 44syl 14 . . . . . . . . 9  |-  ( ph  ->  F : X -1-1-onto-> U. L
)
46 f1ocnv 5455 . . . . . . . . 9  |-  ( F : X -1-1-onto-> U. L  ->  `' F : U. L -1-1-onto-> X )
47 f1of 5442 . . . . . . . . 9  |-  ( `' F : U. L -1-1-onto-> X  ->  `' F : U. L --> X )
4845, 46, 473syl 17 . . . . . . . 8  |-  ( ph  ->  `' F : U. L --> X )
49 xp1st 6144 . . . . . . . 8  |-  ( v  e.  ( U. L  X.  U. M )  -> 
( 1st `  v
)  e.  U. L
)
50 ffvelrn 5629 . . . . . . . 8  |-  ( ( `' F : U. L --> X  /\  ( 1st `  v
)  e.  U. L
)  ->  ( `' F `  ( 1st `  v ) )  e.  X )
5148, 49, 50syl2an 287 . . . . . . 7  |-  ( (
ph  /\  v  e.  ( U. L  X.  U. M ) )  -> 
( `' F `  ( 1st `  v ) )  e.  X )
5214, 37hmeof1o 13103 . . . . . . . . . 10  |-  ( G  e.  ( K Homeo M )  ->  G : Y
-1-1-onto-> U. M )
539, 52syl 14 . . . . . . . . 9  |-  ( ph  ->  G : Y -1-1-onto-> U. M
)
54 f1ocnv 5455 . . . . . . . . 9  |-  ( G : Y -1-1-onto-> U. M  ->  `' G : U. M -1-1-onto-> Y )
55 f1of 5442 . . . . . . . . 9  |-  ( `' G : U. M -1-1-onto-> Y  ->  `' G : U. M --> Y )
5653, 54, 553syl 17 . . . . . . . 8  |-  ( ph  ->  `' G : U. M --> Y )
57 xp2nd 6145 . . . . . . . 8  |-  ( v  e.  ( U. L  X.  U. M )  -> 
( 2nd `  v
)  e.  U. M
)
58 ffvelrn 5629 . . . . . . . 8  |-  ( ( `' G : U. M --> Y  /\  ( 2nd `  v
)  e.  U. M
)  ->  ( `' G `  ( 2nd `  v ) )  e.  Y )
5956, 57, 58syl2an 287 . . . . . . 7  |-  ( (
ph  /\  v  e.  ( U. L  X.  U. M ) )  -> 
( `' G `  ( 2nd `  v ) )  e.  Y )
6051, 59opelxpd 4644 . . . . . 6  |-  ( (
ph  /\  v  e.  ( U. L  X.  U. M ) )  ->  <. ( `' F `  ( 1st `  v ) ) ,  ( `' G `  ( 2nd `  v ) ) >.  e.  ( X  X.  Y
) )
6145adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  F : X -1-1-onto-> U. L )
6234ad2antrl 487 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  ( 1st `  u
)  e.  X )
6349ad2antll 488 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  ( 1st `  v
)  e.  U. L
)
64 f1ocnvfvb 5759 . . . . . . . . . 10  |-  ( ( 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 ) ) )
6561, 62, 63, 64syl3anc 1233 . . . . . . . . 9  |-  ( (
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 2172 . . . . . . . . 9  |-  ( ( 1st `  v )  =  ( F `  ( 1st `  u ) )  <->  ( F `  ( 1st `  u ) )  =  ( 1st `  v ) )
67 eqcom 2172 . . . . . . . . 9  |-  ( ( 1st `  u )  =  ( `' F `  ( 1st `  v
) )  <->  ( `' F `  ( 1st `  v ) )  =  ( 1st `  u
) )
6865, 66, 673bitr4g 222 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  ( ( 1st `  v )  =  ( F `  ( 1st `  u ) )  <->  ( 1st `  u )  =  ( `' F `  ( 1st `  v ) ) ) )
6953adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  G : Y -1-1-onto-> U. M )
7040ad2antrl 487 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  ( 2nd `  u
)  e.  Y )
7157ad2antll 488 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  ( 2nd `  v
)  e.  U. M
)
72 f1ocnvfvb 5759 . . . . . . . . . 10  |-  ( ( 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 ) ) )
7369, 70, 71, 72syl3anc 1233 . . . . . . . . 9  |-  ( (
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 2172 . . . . . . . . 9  |-  ( ( 2nd `  v )  =  ( G `  ( 2nd `  u ) )  <->  ( G `  ( 2nd `  u ) )  =  ( 2nd `  v ) )
75 eqcom 2172 . . . . . . . . 9  |-  ( ( 2nd `  u )  =  ( `' G `  ( 2nd `  v
) )  <->  ( `' G `  ( 2nd `  v ) )  =  ( 2nd `  u
) )
7673, 74, 753bitr4g 222 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  ( X  X.  Y
)  /\  v  e.  ( U. L  X.  U. M ) ) )  ->  ( ( 2nd `  v )  =  ( G `  ( 2nd `  u ) )  <->  ( 2nd `  u )  =  ( `' G `  ( 2nd `  v ) ) ) )
7768, 76anbi12d 470 . . . . . . 7  |-  ( (
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 6156 . . . . . . . 8  |-  ( v  e.  ( U. L  X.  U. M )  -> 
( v  =  <. ( F `  ( 1st `  u ) ) ,  ( G `  ( 2nd `  u ) )
>. 
<->  ( ( 1st `  v
)  =  ( F `
 ( 1st `  u
) )  /\  ( 2nd `  v )  =  ( G `  ( 2nd `  u ) ) ) ) )
7978ad2antll 488 . . . . . . 7  |-  ( (
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 6156 . . . . . . . 8  |-  ( u  e.  ( X  X.  Y )  ->  (
u  =  <. ( `' F `  ( 1st `  v ) ) ,  ( `' G `  ( 2nd `  v ) ) >.  <->  ( ( 1st `  u )  =  ( `' F `  ( 1st `  v ) )  /\  ( 2nd `  u )  =  ( `' G `  ( 2nd `  v
) ) ) ) )
8180ad2antrl 487 . . . . . . 7  |-  ( (
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
) ) ) ) )
8277, 79, 813bitr4rd 220 . . . . . 6  |-  ( (
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
) ) >. )
)
8330, 43, 60, 82f1ocnv2d 6053 . . . . 5  |-  ( 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 ) ) >. ) ) )
8483simprd 113 . . . 4  |-  ( 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 2733 . . . . . . . 8  |-  z  e. 
_V
86 vex 2733 . . . . . . . 8  |-  w  e. 
_V
8785, 86op1std 6127 . . . . . . 7  |-  ( v  =  <. z ,  w >.  ->  ( 1st `  v
)  =  z )
8887fveq2d 5500 . . . . . 6  |-  ( v  =  <. z ,  w >.  ->  ( `' F `  ( 1st `  v
) )  =  ( `' F `  z ) )
8985, 86op2ndd 6128 . . . . . . 7  |-  ( v  =  <. z ,  w >.  ->  ( 2nd `  v
)  =  w )
9089fveq2d 5500 . . . . . 6  |-  ( v  =  <. z ,  w >.  ->  ( `' G `  ( 2nd `  v
) )  =  ( `' G `  w ) )
9188, 90opeq12d 3773 . . . . 5  |-  ( v  =  <. z ,  w >.  ->  <. ( `' F `  ( 1st `  v
) ) ,  ( `' G `  ( 2nd `  v ) ) >.  =  <. ( `' F `  z ) ,  ( `' G `  w )
>. )
9291mpompt 5945 . . . 4  |-  ( 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 )
>. )
9384, 92eqtrdi 2219 . . 3  |-  ( 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 12996 . . . . . 6  |-  ( F  e.  ( J  Cn  L )  ->  L  e.  Top )
953, 94syl 14 . . . . 5  |-  ( ph  ->  L  e.  Top )
9631toptopon 12810 . . . . 5  |-  ( L  e.  Top  <->  L  e.  (TopOn `  U. L ) )
9795, 96sylib 121 . . . 4  |-  ( ph  ->  L  e.  (TopOn `  U. L ) )
98 cntop2 12996 . . . . . 6  |-  ( G  e.  ( K  Cn  M )  ->  M  e.  Top )
9911, 98syl 14 . . . . 5  |-  ( ph  ->  M  e.  Top )
10037toptopon 12810 . . . . 5  |-  ( M  e.  Top  <->  M  e.  (TopOn `  U. M ) )
10199, 100sylib 121 . . . 4  |-  ( ph  ->  M  e.  (TopOn `  U. M ) )
10297, 101cnmpt1st 13082 . . . . 5  |-  ( ph  ->  ( z  e.  U. L ,  w  e.  U. M  |->  z )  e.  ( ( L  tX  M )  Cn  L
) )
103 hmeocnvcn 13100 . . . . . 6  |-  ( F  e.  ( J Homeo L )  ->  `' F  e.  ( L  Cn  J
) )
1041, 103syl 14 . . . . 5  |-  ( ph  ->  `' F  e.  ( L  Cn  J ) )
10597, 101, 102, 104cnmpt21f 13086 . . . 4  |-  ( ph  ->  ( z  e.  U. L ,  w  e.  U. M  |->  ( `' F `  z ) )  e.  ( ( L  tX  M )  Cn  J
) )
10697, 101cnmpt2nd 13083 . . . . 5  |-  ( ph  ->  ( z  e.  U. L ,  w  e.  U. M  |->  w )  e.  ( ( L  tX  M )  Cn  M
) )
107 hmeocnvcn 13100 . . . . . 6  |-  ( G  e.  ( K Homeo M )  ->  `' G  e.  ( M  Cn  K
) )
1089, 107syl 14 . . . . 5  |-  ( ph  ->  `' G  e.  ( M  Cn  K ) )
10997, 101, 106, 108cnmpt21f 13086 . . . 4  |-  ( ph  ->  ( z  e.  U. L ,  w  e.  U. M  |->  ( `' G `  w ) )  e.  ( ( L  tX  M )  Cn  K
) )
11097, 101, 105, 109cnmpt2t 13087 . . 3  |-  ( ph  ->  ( z  e.  U. L ,  w  e.  U. M  |->  <. ( `' F `  z ) ,  ( `' G `  w )
>. )  e.  (
( L  tX  M
)  Cn  ( J 
tX  K ) ) )
11193, 110eqeltrd 2247 . 2  |-  ( ph  ->  `' ( x  e.  X ,  y  e.  Y  |->  <. ( F `  x ) ,  ( G `  y )
>. )  e.  (
( L  tX  M
)  Cn  ( J 
tX  K ) ) )
112 ishmeo 13098 . 2  |-  ( ( 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 ) ) ) )
11321, 111, 112sylanbrc 415 1  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |-> 
<. ( F `  x
) ,  ( G `
 y ) >.
)  e.  ( ( J  tX  K )
Homeo ( L  tX  M
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1348    e. wcel 2141   <.cop 3586   U.cuni 3796    |-> cmpt 4050    X. cxp 4609   `'ccnv 4610   -->wf 5194   -1-1-onto->wf1o 5197   ` cfv 5198  (class class class)co 5853    e. cmpo 5855   1stc1st 6117   2ndc2nd 6118   Topctop 12789  TopOnctopon 12802    Cn ccn 12979    tX ctx 13046   Homeochmeo 13094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-map 6628  df-topgen 12600  df-top 12790  df-topon 12803  df-bases 12835  df-cn 12982  df-tx 13047  df-hmeo 13095
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator