Theorem relcnvtrOLD

Description: Obsolete form of relcnvtrg as of 8-Aug-2026. (Contributed by FL, 19-Sep-2011) (Proof shortened by Peter Mazsa, 17-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	relcnvtrOLD	$$⊢\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		relcnvtrgOLD	$$⊢\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)$$