Metamath Proof Explorer


Theorem tposmpo

Description: Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis tposmpo.1 F=xA,yBC
Assertion tposmpo tposF=yB,xAC

Proof

Step Hyp Ref Expression
1 tposmpo.1 F=xA,yBC
2 df-mpo xA,yBC=xyz|xAyBz=C
3 ancom xAyByBxA
4 3 anbi1i xAyBz=CyBxAz=C
5 4 oprabbii xyz|xAyBz=C=xyz|yBxAz=C
6 1 2 5 3eqtri F=xyz|yBxAz=C
7 6 tposoprab tposF=yxz|yBxAz=C
8 df-mpo yB,xAC=yxz|yBxAz=C
9 7 8 eqtr4i tposF=yB,xAC