Theorem elcnvrefrels2

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

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

Proof

Step	Hyp	Ref	Expression
1		dfcnvrefrels2	$$⊢\mathrm{CnvRefRels}=\left\{r\in \mathrm{Rels}|r\subseteq \mathrm{I}\cap \left(\mathrm{dom}r\times \mathrm{ran}r\right)\right\}$$
2		id	$$⊢r=R\to r=R$$
3		dmeq	$$⊢r=R\to \mathrm{dom}r=\mathrm{dom}R$$
4		rneq	$$⊢r=R\to \mathrm{ran}r=\mathrm{ran}R$$
5	3 4	xpeq12d	$$⊢r=R\to \mathrm{dom}r\times \mathrm{ran}r=\mathrm{dom}R\times \mathrm{ran}R$$
6	5	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)$$
7	2 6	sseq12d	$$⊢r=R\to \left(r\subseteq \mathrm{I}\cap \left(\mathrm{dom}r\times \mathrm{ran}r\right)\leftrightarrow R\subseteq \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\right)$$
8	1 7	rabeqel	$$⊢R\in \mathrm{CnvRefRels}\leftrightarrow \left(R\subseteq \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\wedge R\in \mathrm{Rels}\right)$$