# 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`