This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem txswaphmeolem

Description: Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion txswaphmeolem 
|- ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( _I |` ( X X. Y ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( z = <. x , y >. -> z = <. x , y >. )
2 1 mpompt 
 |-  ( z e. ( X X. Y ) |-> z ) = ( x e. X , y e. Y |-> <. x , y >. )
3 mptresid 
 |-  ( _I |` ( X X. Y ) ) = ( z e. ( X X. Y ) |-> z )
4 opelxpi 
 |-  ( ( y e. Y /\ x e. X ) -> <. y , x >. e. ( Y X. X ) )
5 4 ancoms 
 |-  ( ( x e. X /\ y e. Y ) -> <. y , x >. e. ( Y X. X ) )
6 5 adantl 
 |-  ( ( T. /\ ( x e. X /\ y e. Y ) ) -> <. y , x >. e. ( Y X. X ) )
7 eqidd 
 |-  ( T. -> ( x e. X , y e. Y |-> <. y , x >. ) = ( x e. X , y e. Y |-> <. y , x >. ) )
8 sneq 
 |-  ( z = <. y , x >. -> { z } = { <. y , x >. } )
9 8 cnveqd 
 |-  ( z = <. y , x >. -> `' { z } = `' { <. y , x >. } )
10 9 unieqd 
 |-  ( z = <. y , x >. -> U. `' { z } = U. `' { <. y , x >. } )
11 opswap 
 |-  U. `' { <. y , x >. } = <. x , y >.
12 10 11 eqtrdi 
 |-  ( z = <. y , x >. -> U. `' { z } = <. x , y >. )
13 12 mpompt 
 |-  ( z e. ( Y X. X ) |-> U. `' { z } ) = ( y e. Y , x e. X |-> <. x , y >. )
14 13 eqcomi 
 |-  ( y e. Y , x e. X |-> <. x , y >. ) = ( z e. ( Y X. X ) |-> U. `' { z } )
15 14 a1i 
 |-  ( T. -> ( y e. Y , x e. X |-> <. x , y >. ) = ( z e. ( Y X. X ) |-> U. `' { z } ) )
16 6 7 15 12 fmpoco 
 |-  ( T. -> ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( x e. X , y e. Y |-> <. x , y >. ) )
17 16 mptru 
 |-  ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( x e. X , y e. Y |-> <. x , y >. )
18 2 3 17 3eqtr4ri 
 |-  ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( _I |` ( X X. Y ) )