Theorem eleqvrels2

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

	Ref	Expression
Assertion	eleqvrels2	$$⊢R\in \mathrm{EqvRels}\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\wedge R^{-1}\subseteq R\wedge R\circ R\subseteq R\right)\wedge R\in \mathrm{Rels}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfeqvrels2	$$⊢\mathrm{EqvRels}=\left\{r\in \mathrm{Rels}|\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\wedge r^{-1}\subseteq r\wedge r\circ r\subseteq r\right)\right\}$$
2		dmeq	$$⊢r=R\to \mathrm{dom}r=\mathrm{dom}R$$
3	2	reseq2d	$$⊢r=R\to {\mathrm{I}\upharpoonright }_{\mathrm{dom}r}={\mathrm{I}\upharpoonright }_{\mathrm{dom}R}$$
4		id	$$⊢r=R\to r=R$$
5	3 4	sseq12d	$$⊢r=R\to \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\leftrightarrow {\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\right)$$
6		cnveq	$$⊢r=R\to r^{-1}=R^{-1}$$
7	6 4	sseq12d	$$⊢r=R\to \left(r^{-1}\subseteq r\leftrightarrow R^{-1}\subseteq R\right)$$
8		coideq	$$⊢r=R\to r\circ r=R\circ R$$
9	8 4	sseq12d	$$⊢r=R\to \left(r\circ r\subseteq r\leftrightarrow R\circ R\subseteq R\right)$$
10	5 7 9	3anbi123d	$$⊢r=R\to \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\wedge r^{-1}\subseteq r\wedge r\circ r\subseteq r\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\wedge R^{-1}\subseteq R\wedge R\circ R\subseteq R\right)\right)$$
11	1 10	rabeqel	$$⊢R\in \mathrm{EqvRels}\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\wedge R^{-1}\subseteq R\wedge R\circ R\subseteq R\right)\wedge R\in \mathrm{Rels}\right)$$