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×BCtposF:B×AC

Proof

Step Hyp Ref Expression
1 relxp RelA×B
2 tposf2 RelA×BF:A×BCtposF:A×B-1C
3 1 2 ax-mp F:A×BCtposF:A×B-1C
4 cnvxp A×B-1=B×A
5 4 feq2i tposF:A×B-1CtposF:B×AC
6 3 5 sylib F:A×BCtposF:B×AC