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

Metamath Proof Explorer

Theorem reltpos

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

		Ref	Expression
	Assertion	reltpos	$⊢ Rel tpos F$

Step	Hyp	Ref	Expression
1		tposssxp	$⊢ tpos F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F$
2		relxp	$⊢ Rel (({dom F}^{-1} \cup \{\emptyset\}) \times ran F)$
3		relss	$⊢ tpos F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F \to (Rel (({dom F}^{-1} \cup \{\emptyset\}) \times ran F) \to Rel tpos F)$
4	1 2 3	mp2	$⊢ Rel tpos F$