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 )