This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (I \cap (dom R \times ran R) \subseteq R \leftrightarrow {I ↾}_{dom R} \subseteq R)$

Proof

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