Metamath Proof Explorer


Theorem tposfun

Description: The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion tposfun Fun F Fun tpos F

Proof

Step Hyp Ref Expression
1 funmpt Fun x dom F -1 x -1
2 funco Fun F Fun x dom F -1 x -1 Fun F x dom F -1 x -1
3 1 2 mpan2 Fun F Fun F x dom F -1 x -1
4 df-tpos tpos F = F x dom F -1 x -1
5 4 funeqi Fun tpos F Fun F x dom F -1 x -1
6 3 5 sylibr Fun F Fun tpos F