Theorem relcnvtrg

Description: Subclass law for converse of a composition. A particular case is ( ( R o. R ) C_ R <-> (`' R o. ``' R ) C_ ``' R ) ` , which says that a relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011) Generalize to a statement about three classes rather than one. (Revised by Peter Mazsa, 17-Oct-2023) Remove antecedent. (Revised by Eric Schmidt, 8-Aug-2026)

	Ref	Expression
Assertion	relcnvtrg	$$⊢R\circ S\subseteq T\leftrightarrow S^{-1}\circ R^{-1}\subseteq T^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		cnvco	$$⊢{\left(R\circ S\right)}^{-1}=S^{-1}\circ R^{-1}$$
2		cnvss	$$⊢R\circ S\subseteq T\to {\left(R\circ S\right)}^{-1}\subseteq T^{-1}$$
3	1 2	eqsstrrid	$$⊢R\circ S\subseteq T\to S^{-1}\circ R^{-1}\subseteq T^{-1}$$
4		cnvco	$$⊢{\left(S^{-1}\circ R^{-1}\right)}^{-1}={R^{-1}}^{-1}\circ {S^{-1}}^{-1}$$
5		cocnvcnv1	$$⊢{R^{-1}}^{-1}\circ {S^{-1}}^{-1}=R\circ {S^{-1}}^{-1}$$
6		cocnvcnv2	$$⊢R\circ {S^{-1}}^{-1}=R\circ S$$
7	4 5 6	3eqtri	$$⊢{\left(S^{-1}\circ R^{-1}\right)}^{-1}=R\circ S$$
8		cnvss	$$⊢S^{-1}\circ R^{-1}\subseteq T^{-1}\to {\left(S^{-1}\circ R^{-1}\right)}^{-1}\subseteq {T^{-1}}^{-1}$$
9	7 8	eqsstrrid	$$⊢S^{-1}\circ R^{-1}\subseteq T^{-1}\to R\circ S\subseteq {T^{-1}}^{-1}$$
10		cnvcnvss	$$⊢{T^{-1}}^{-1}\subseteq T$$
11	9 10	sstrdi	$$⊢S^{-1}\circ R^{-1}\subseteq T^{-1}\to R\circ S\subseteq T$$
12	3 11	impbii	$$⊢R\circ S\subseteq T\leftrightarrow S^{-1}\circ R^{-1}\subseteq T^{-1}$$