Theorem reltpos

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

	Ref	Expression
Assertion	reltpos	|- Rel tpos F

Proof

Step	Hyp	Ref	Expression
1		tposssxp	|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )
2		relxp	|- Rel ( ( `' dom F u. { (/) } ) X. ran F )
3		relss	|- ( tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F ) -> ( Rel ( ( `' dom F u. { (/) } ) X. ran F ) -> Rel tpos F ) )
4	1 2 3	mp2	|- Rel tpos F