Metamath Proof Explorer

Theorem dfer2

Description: Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997) (Revised by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Assertion	dfer2	$⊢ R Er A \leftrightarrow (Rel R \land dom R = A \land \forall x \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z)))$

Proof

Step	Hyp	Ref	Expression
1		df-er	$⊢ R Er A \leftrightarrow (Rel R \land dom R = A \land R^{-1} \cup (R \circ R) \subseteq R)$
2		cnvsym	$⊢ R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \to y R x)$
3		cotr	$⊢ R \circ R \subseteq R \leftrightarrow \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
4	2 3	anbi12i	$⊢ (R^{-1} \subseteq R \land R \circ R \subseteq R) \leftrightarrow (\forall x \forall y (x R y \to y R x) \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z))$
5		unss	$⊢ (R^{-1} \subseteq R \land R \circ R \subseteq R) \leftrightarrow R^{-1} \cup (R \circ R) \subseteq R$
6		19.28v	$⊢ \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z)) \leftrightarrow ((x R y \to y R x) \land \forall z ((x R y \land y R z) \to x R z))$
7	6	albii	$⊢ \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall y ((x R y \to y R x) \land \forall z ((x R y \land y R z) \to x R z))$
8		19.26	$⊢ \forall y ((x R y \to y R x) \land \forall z ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall y (x R y \to y R x) \land \forall y \forall z ((x R y \land y R z) \to x R z))$
9	7 8	bitri	$⊢ \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall y (x R y \to y R x) \land \forall y \forall z ((x R y \land y R z) \to x R z))$
10	9	albii	$⊢ \forall x \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x (\forall y (x R y \to y R x) \land \forall y \forall z ((x R y \land y R z) \to x R z))$
11		19.26	$⊢ \forall x (\forall y (x R y \to y R x) \land \forall y \forall z ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall x \forall y (x R y \to y R x) \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z))$
12	10 11	bitr2i	$⊢ (\forall x \forall y (x R y \to y R x) \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z))$
13	4 5 12	3bitr3i	$⊢ R^{-1} \cup (R \circ R) \subseteq R \leftrightarrow \forall x \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z))$
14	13	3anbi3i	$⊢ (Rel R \land dom R = A \land R^{-1} \cup (R \circ R) \subseteq R) \leftrightarrow (Rel R \land dom R = A \land \forall x \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z)))$
15	1 14	bitri	$⊢ R Er A \leftrightarrow (Rel R \land dom R = A \land \forall x \forall y \forall z ((x R y \to y R x) \land ((x R y \land y R z) \to x R z)))$