Metamath Proof Explorer


Theorem tposf

Description: The domain and range of a transposition. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tposf F : A × B C tpos F : B × A C

Proof

Step Hyp Ref Expression
1 relxp Rel A × B
2 tposf2 Rel A × B F : A × B C tpos F : A × B -1 C
3 1 2 ax-mp F : A × B C tpos F : A × B -1 C
4 cnvxp A × B -1 = B × A
5 4 feq2i tpos F : A × B -1 C tpos F : B × A C
6 3 5 sylib F : A × B C tpos F : B × A C