Theorem cnvtrrel

Description: The converse of a transitive relation is a transitive relation. (Contributed by RP, 25-Dec-2019)

	Ref	Expression
Assertion	cnvtrrel	$$⊢S\circ S\subseteq S\leftrightarrow S^{-1}\circ S^{-1}\subseteq S^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		cnvss	$$⊢S\circ S\subseteq S\to {\left(S\circ S\right)}^{-1}\subseteq S^{-1}$$
2		cnvss	$$⊢{\left(S\circ S\right)}^{-1}\subseteq S^{-1}\to {{\left(S\circ S\right)}^{-1}}^{-1}\subseteq {S^{-1}}^{-1}$$
3		cnvco	$$⊢{\left(S\circ S\right)}^{-1}=S^{-1}\circ S^{-1}$$
4	3	cnveqi	$$⊢{{\left(S\circ S\right)}^{-1}}^{-1}={\left(S^{-1}\circ S^{-1}\right)}^{-1}$$
5		cnvco	$$⊢{\left(S^{-1}\circ S^{-1}\right)}^{-1}={S^{-1}}^{-1}\circ {S^{-1}}^{-1}$$
6		cocnvcnv1	$$⊢{S^{-1}}^{-1}\circ {S^{-1}}^{-1}=S\circ {S^{-1}}^{-1}$$
7		cocnvcnv2	$$⊢S\circ {S^{-1}}^{-1}=S\circ S$$
8	6 7	eqtri	$$⊢{S^{-1}}^{-1}\circ {S^{-1}}^{-1}=S\circ S$$
9	4 5 8	3eqtri	$$⊢{{\left(S\circ S\right)}^{-1}}^{-1}=S\circ S$$
10	9	sseq1i	$$⊢{{\left(S\circ S\right)}^{-1}}^{-1}\subseteq {S^{-1}}^{-1}\leftrightarrow S\circ S\subseteq {S^{-1}}^{-1}$$
11	10	biimpi	$$⊢{{\left(S\circ S\right)}^{-1}}^{-1}\subseteq {S^{-1}}^{-1}\to S\circ S\subseteq {S^{-1}}^{-1}$$
12		cnvcnvss	$$⊢{S^{-1}}^{-1}\subseteq S$$
13	11 12	sstrdi	$$⊢{{\left(S\circ S\right)}^{-1}}^{-1}\subseteq {S^{-1}}^{-1}\to S\circ S\subseteq S$$
14	2 13	syl	$$⊢{\left(S\circ S\right)}^{-1}\subseteq S^{-1}\to S\circ S\subseteq S$$
15	1 14	impbii	$$⊢S\circ S\subseteq S\leftrightarrow {\left(S\circ S\right)}^{-1}\subseteq S^{-1}$$
16	3	sseq1i	$$⊢{\left(S\circ S\right)}^{-1}\subseteq S^{-1}\leftrightarrow S^{-1}\circ S^{-1}\subseteq S^{-1}$$
17	15 16	bitri	$$⊢S\circ S\subseteq S\leftrightarrow S^{-1}\circ S^{-1}\subseteq S^{-1}$$