Theorem relcnvtr

Description: A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011) (Proof shortened by Peter Mazsa, 17-Oct-2023)

	Ref	Expression
Assertion	relcnvtr	$$⊢\mathrm{Rel}R\to \left(R\circ R\subseteq R\leftrightarrow R^{-1}\circ R^{-1}\subseteq R^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		3anidm	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{Rel}R\wedge \mathrm{Rel}R\right)\leftrightarrow \mathrm{Rel}R$$
2		relcnvtrg	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{Rel}R\wedge \mathrm{Rel}R\right)\to \left(R\circ R\subseteq R\leftrightarrow R^{-1}\circ R^{-1}\subseteq R^{-1}\right)$$
3	1 2	sylbir	$$⊢\mathrm{Rel}R\to \left(R\circ R\subseteq R\leftrightarrow R^{-1}\circ R^{-1}\subseteq R^{-1}\right)$$