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 yY,xXxyxX,yYyx=IX×Y

Proof

Step Hyp Ref Expression
1 id z=xyz=xy
2 1 mpompt zX×Yz=xX,yYxy
3 mptresid IX×Y=zX×Yz
4 opelxpi yYxXyxY×X
5 4 ancoms xXyYyxY×X
6 5 adantl xXyYyxY×X
7 eqidd xX,yYyx=xX,yYyx
8 sneq z=yxz=yx
9 8 cnveqd z=yxz-1=yx-1
10 9 unieqd z=yxz-1=yx-1
11 opswap yx-1=xy
12 10 11 eqtrdi z=yxz-1=xy
13 12 mpompt zY×Xz-1=yY,xXxy
14 13 eqcomi yY,xXxy=zY×Xz-1
15 14 a1i yY,xXxy=zY×Xz-1
16 6 7 15 12 fmpoco yY,xXxyxX,yYyx=xX,yYxy
17 16 mptru yY,xXxyxX,yYyx=xX,yYxy
18 2 3 17 3eqtr4ri yY,xXxyxX,yYyx=IX×Y