Metamath Proof Explorer

Theorem symrefref3

Description: Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 . (Contributed by Peter Mazsa, 23-Aug-2021) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	symrefref3	$⊢ \forall x \forall y (x R y \to y R x) \to (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \leftrightarrow \forall x \in dom R x R x)$

Proof

Step	Hyp	Ref	Expression
1		symrefref2	$⊢ R^{-1} \subseteq R \to (I \cap (dom R \times ran R) \subseteq R \leftrightarrow {I ↾}_{dom R} \subseteq R)$
2		cnvsym	$⊢ R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \to y R x)$
3		idinxpss	$⊢ I \cap (dom R \times ran R) \subseteq R \leftrightarrow \forall x \in dom R \forall y \in ran R (x = y \to x R y)$
4		idrefALT	$⊢ {I ↾}_{dom R} \subseteq R \leftrightarrow \forall x \in dom R x R x$
5	3 4	bibi12i	$⊢ (I \cap (dom R \times ran R) \subseteq R \leftrightarrow {I ↾}_{dom R} \subseteq R) \leftrightarrow (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \leftrightarrow \forall x \in dom R x R x)$
6	1 2 5	3imtr3i	$⊢ \forall x \forall y (x R y \to y R x) \to (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \leftrightarrow \forall x \in dom R x R x)$