Theorem elrefsymrels2

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 ) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom R X. ran R ) ) C R version of dfrefrels2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 22-Jul-2019)

	Ref	Expression
Assertion	elrefsymrels2	$$⊢R\in \left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\wedge R^{-1}\subseteq R\right)\wedge R\in \mathrm{Rels}\right)$$

Proof

Step	Hyp	Ref	Expression
1		refsymrels2	$$⊢\mathrm{RefRels}\cap \mathrm{SymRels}=\left\{r\in \mathrm{Rels}|\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\wedge r^{-1}\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	5 7	anbi12d	$$⊢r=R\to \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\wedge r^{-1}\subseteq r\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\wedge R^{-1}\subseteq R\right)\right)$$
9	1 8	rabeqel	$$⊢R\in \left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\wedge R^{-1}\subseteq R\right)\wedge R\in \mathrm{Rels}\right)$$