Theorem reltpos

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

	Ref	Expression
Assertion	reltpos	⊢ Rel tpos 𝐹

Proof

Step	Hyp	Ref	Expression
1		tposssxp	⊢ tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 )
2		relxp	⊢ Rel ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 )
3		relss	⊢ ( tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) → ( Rel ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) → Rel tpos 𝐹 ) )
4	1 2 3	mp2	⊢ Rel tpos 𝐹