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

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 = ( x e. A , y e. B |-> C )
Assertion tposmpo 
|- tpos F = ( y e. B , x e. A |-> C )

Proof

Step Hyp Ref Expression
1 tposmpo.1 
 |-  F = ( x e. A , y e. B |-> C )
2 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
3 ancom 
 |-  ( ( x e. A /\ y e. B ) <-> ( y e. B /\ x e. A ) )
4 3 anbi1i 
 |-  ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( y e. B /\ x e. A ) /\ z = C ) )
5 4 oprabbii 
 |-  { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { <. <. x , y >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) }
6 1 2 5 3eqtri 
 |-  F = { <. <. x , y >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) }
7 6 tposoprab 
 |-  tpos F = { <. <. y , x >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) }
8 df-mpo 
 |-  ( y e. B , x e. A |-> C ) = { <. <. y , x >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) }
9 7 8 eqtr4i 
 |-  tpos F = ( y e. B , x e. A |-> C )