Theorem eltrrels2

Description: Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021)

	Ref	Expression
Assertion	eltrrels2	$$⊢R\in \mathrm{TrRels}\leftrightarrow \left(R\circ R\subseteq R\wedge R\in \mathrm{Rels}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dftrrels2	$$⊢\mathrm{TrRels}=\left\{r\in \mathrm{Rels}|r\circ r\subseteq r\right\}$$
2		coideq	$$⊢r=R\to r\circ r=R\circ R$$
3		id	$$⊢r=R\to r=R$$
4	2 3	sseq12d	$$⊢r=R\to \left(r\circ r\subseteq r\leftrightarrow R\circ R\subseteq R\right)$$
5	1 4	rabeqel	$$⊢R\in \mathrm{TrRels}\leftrightarrow \left(R\circ R\subseteq R\wedge R\in \mathrm{Rels}\right)$$