Theorem elrefrels2

Description: Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019)

	Ref	Expression
Assertion	elrefrels2	$$⊢R\in \mathrm{RefRels}\leftrightarrow \left(\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\wedge R\in \mathrm{Rels}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfrefrels2	$$⊢\mathrm{RefRels}=\left\{r\in \mathrm{Rels}|\mathrm{I}\cap \left(\mathrm{dom}r\times \mathrm{ran}r\right)\subseteq r\right\}$$
2		dmeq	$$⊢r=R\to \mathrm{dom}r=\mathrm{dom}R$$
3		rneq	$$⊢r=R\to \mathrm{ran}r=\mathrm{ran}R$$
4	2 3	xpeq12d	$$⊢r=R\to \mathrm{dom}r\times \mathrm{ran}r=\mathrm{dom}R\times \mathrm{ran}R$$
5	4	ineq2d	$$⊢r=R\to \mathrm{I}\cap \left(\mathrm{dom}r\times \mathrm{ran}r\right)=\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
6		id	$$⊢r=R\to r=R$$
7	5 6	sseq12d	$$⊢r=R\to \left(\mathrm{I}\cap \left(\mathrm{dom}r\times \mathrm{ran}r\right)\subseteq r\leftrightarrow \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\right)$$
8	1 7	rabeqel	$$⊢R\in \mathrm{RefRels}\leftrightarrow \left(\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\wedge R\in \mathrm{Rels}\right)$$