refsymrel3

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the A. x e. dom R x R x version for its reflexive part, not just the A. x e. dom R A. y e. ran R ( x = y -> x R y ) version of dfrefrel3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 23-Aug-2021)

		Ref	Expression
	Assertion	refsymrel3	$⊢ (RefRel R \land SymRel R) \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		dfrefrel3	$⊢ RefRel R \leftrightarrow (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land Rel R)$
2		dfsymrel3	$⊢ SymRel R \leftrightarrow (\forall x \forall y (x R y \to y R x) \land Rel R)$
3	1 2	anbi12i	$⊢ (RefRel R \land SymRel R) \leftrightarrow ((\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land Rel R) \land (\forall x \forall y (x R y \to y R x) \land Rel R))$
4		anandi3r	$⊢ (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land Rel R \land \forall x \forall y (x R y \to y R x)) \leftrightarrow ((\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land Rel R) \land (\forall x \forall y (x R y \to y R x) \land Rel R))$
5		3anan32	$⊢ (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land Rel R \land \forall x \forall y (x R y \to y R x)) \leftrightarrow ((\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land \forall x \forall y (x R y \to y R x)) \land Rel R)$
6	3 4 5	3bitr2i	$⊢ (RefRel R \land SymRel R) \leftrightarrow ((\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land \forall x \forall y (x R y \to y R x)) \land Rel R)$
7		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)$
8	7	pm5.32ri	$⊢ (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land \forall x \forall y (x R y \to y R x)) \leftrightarrow (\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x))$
9	8	anbi1i	$⊢ ((\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land \forall x \forall y (x R y \to y R x)) \land Rel R) \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R)$
10	6 9	bitri	$⊢ (RefRel R \land SymRel R) \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R)$

Metamath Proof Explorer

Theorem refsymrel3

Proof