Metamath Proof Explorer

Theorem txswaphmeo

Description: There is a homeomorphism from X X. Y to Y X. X . (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion txswaphmeo 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( J tX K ) Homeo ( K tX J ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> J e. ( TopOn ` X ) )
2 simpr 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> K e. ( TopOn ` Y ) )
3 1 2 cnmpt2nd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
4 1 2 cnmpt1st 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
5 1 2 3 4 cnmpt2t 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( J tX K ) Cn ( K tX J ) ) )
6 opelxpi 
 |-  ( ( y e. Y /\ x e. X ) -> <. y , x >. e. ( Y X. X ) )
7 6 ancoms 
 |-  ( ( x e. X /\ y e. Y ) -> <. y , x >. e. ( Y X. X ) )
8 7 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( x e. X /\ y e. Y ) ) -> <. y , x >. e. ( Y X. X ) )
9 8 ralrimivva 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> A. x e. X A. y e. Y <. y , x >. e. ( Y X. X ) )
10 eqid 
 |-  ( x e. X , y e. Y |-> <. y , x >. ) = ( x e. X , y e. Y |-> <. y , x >. )
11 10 fmpo 
 |-  ( A. x e. X A. y e. Y <. y , x >. e. ( Y X. X ) <-> ( x e. X , y e. Y |-> <. y , x >. ) : ( X X. Y ) --> ( Y X. X ) )
12 9 11 sylib 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( x e. X , y e. Y |-> <. y , x >. ) : ( X X. Y ) --> ( Y X. X ) )
13 opelxpi 
 |-  ( ( x e. X /\ y e. Y ) -> <. x , y >. e. ( X X. Y ) )
14 13 ancoms 
 |-  ( ( y e. Y /\ x e. X ) -> <. x , y >. e. ( X X. Y ) )
15 14 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( y e. Y /\ x e. X ) ) -> <. x , y >. e. ( X X. Y ) )
16 15 ralrimivva 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> A. y e. Y A. x e. X <. x , y >. e. ( X X. Y ) )
17 eqid 
 |-  ( y e. Y , x e. X |-> <. x , y >. ) = ( y e. Y , x e. X |-> <. x , y >. )
18 17 fmpo 
 |-  ( A. y e. Y A. x e. X <. x , y >. e. ( X X. Y ) <-> ( y e. Y , x e. X |-> <. x , y >. ) : ( Y X. X ) --> ( X X. Y ) )
19 16 18 sylib 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( y e. Y , x e. X |-> <. x , y >. ) : ( Y X. X ) --> ( X X. Y ) )
20 txswaphmeolem 
 |-  ( ( x e. X , y e. Y |-> <. y , x >. ) o. ( y e. Y , x e. X |-> <. x , y >. ) ) = ( _I |` ( Y X. X ) )
21 txswaphmeolem 
 |-  ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( _I |` ( X X. Y ) )
22 fcof1o 
 |-  ( ( ( ( x e. X , y e. Y |-> <. y , x >. ) : ( X X. Y ) --> ( Y X. X ) /\ ( y e. Y , x e. X |-> <. x , y >. ) : ( Y X. X ) --> ( X X. Y ) ) /\ ( ( ( x e. X , y e. Y |-> <. y , x >. ) o. ( y e. Y , x e. X |-> <. x , y >. ) ) = ( _I |` ( Y X. X ) ) /\ ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( _I |` ( X X. Y ) ) ) ) -> ( ( x e. X , y e. Y |-> <. y , x >. ) : ( X X. Y ) -1-1-onto-> ( Y X. X ) /\ `' ( x e. X , y e. Y |-> <. y , x >. ) = ( y e. Y , x e. X |-> <. x , y >. ) ) )
23 20 21 22 mpanr12 
 |-  ( ( ( x e. X , y e. Y |-> <. y , x >. ) : ( X X. Y ) --> ( Y X. X ) /\ ( y e. Y , x e. X |-> <. x , y >. ) : ( Y X. X ) --> ( X X. Y ) ) -> ( ( x e. X , y e. Y |-> <. y , x >. ) : ( X X. Y ) -1-1-onto-> ( Y X. X ) /\ `' ( x e. X , y e. Y |-> <. y , x >. ) = ( y e. Y , x e. X |-> <. x , y >. ) ) )
24 12 19 23 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( x e. X , y e. Y |-> <. y , x >. ) : ( X X. Y ) -1-1-onto-> ( Y X. X ) /\ `' ( x e. X , y e. Y |-> <. y , x >. ) = ( y e. Y , x e. X |-> <. x , y >. ) ) )
25 24 simprd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> `' ( x e. X , y e. Y |-> <. y , x >. ) = ( y e. Y , x e. X |-> <. x , y >. ) )
26 2 1 cnmpt2nd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( y e. Y , x e. X |-> x ) e. ( ( K tX J ) Cn J ) )
27 2 1 cnmpt1st 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( y e. Y , x e. X |-> y ) e. ( ( K tX J ) Cn K ) )
28 2 1 26 27 cnmpt2t 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( y e. Y , x e. X |-> <. x , y >. ) e. ( ( K tX J ) Cn ( J tX K ) ) )
29 25 28 eqeltrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> `' ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( K tX J ) Cn ( J tX K ) ) )
30 ishmeo 
 |-  ( ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( J tX K ) Homeo ( K tX J ) ) <-> ( ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( J tX K ) Cn ( K tX J ) ) /\ `' ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( K tX J ) Cn ( J tX K ) ) ) )
31 5 29 30 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( J tX K ) Homeo ( K tX J ) ) )