Theorem symrefref2

Description: Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 . (Contributed by Peter Mazsa, 19-Jul-2018)

	Ref	Expression
Assertion	symrefref2	$$⊢R^{-1}\subseteq R\to \left(\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\leftrightarrow {\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnss	$$⊢R^{-1}\subseteq R\to \mathrm{ran}{R}^{-1}\subseteq \mathrm{ran}R$$
2		rncnv	$$⊢\mathrm{ran}{R}^{-1}=\mathrm{dom}R$$
3	2	sseq1i	$$⊢\mathrm{ran}{R}^{-1}\subseteq \mathrm{ran}R\leftrightarrow \mathrm{dom}R\subseteq \mathrm{ran}R$$
4	3	biimpi	$$⊢\mathrm{ran}{R}^{-1}\subseteq \mathrm{ran}R\to \mathrm{dom}R\subseteq \mathrm{ran}R$$
5		idreseqidinxp	$$⊢\mathrm{dom}R\subseteq \mathrm{ran}R\to \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}R}$$
6	1 4 5	3syl	$$⊢R^{-1}\subseteq R\to \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}R}$$
7	6	sseq1d	$$⊢R^{-1}\subseteq R\to \left(\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\leftrightarrow {\mathrm{I}\upharpoonright }_{\mathrm{dom}R}\subseteq R\right)$$