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

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 e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
2 funco 
 |-  ( ( Fun F /\ Fun ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) -> Fun ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) )
3 1 2 mpan2 
 |-  ( Fun F -> Fun ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) )
4 df-tpos 
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
5 4 funeqi 
 |-  ( Fun tpos F <-> Fun ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) )
6 3 5 sylibr 
 |-  ( Fun F -> Fun tpos F )