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 )