dfantisymrel5

Description: Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024)

		Ref	Expression
	Assertion	dfantisymrel5	$⊢ AntisymRel R \leftrightarrow (\forall x \forall y ((x R y \land y R x) \to x = y) \land Rel R)$

Step	Hyp	Ref	Expression
1		df-antisymrel	$⊢ AntisymRel R \leftrightarrow (CnvRefRel (R \cap R^{-1}) \land Rel R)$
2		relcnv	$⊢ Rel R^{-1}$
3		relin2	$⊢ Rel R^{-1} \to Rel (R \cap R^{-1})$
4	2 3	ax-mp	$⊢ Rel (R \cap R^{-1})$
5		dfcnvrefrel5	$⊢ CnvRefRel (R \cap R^{-1}) \leftrightarrow (\forall x \forall y (x (R \cap R^{-1}) y \to x = y) \land Rel (R \cap R^{-1}))$
6	4 5	mpbiran2	$⊢ CnvRefRel (R \cap R^{-1}) \leftrightarrow \forall x \forall y (x (R \cap R^{-1}) y \to x = y)$
7		brcnvin	$⊢ (x \in V \land y \in V) \to (x (R \cap R^{-1}) y \leftrightarrow (x R y \land y R x))$
8	7	el2v	$⊢ x (R \cap R^{-1}) y \leftrightarrow (x R y \land y R x)$
9	8	imbi1i	$⊢ (x (R \cap R^{-1}) y \to x = y) \leftrightarrow ((x R y \land y R x) \to x = y)$
10	9	2albii	$⊢ \forall x \forall y (x (R \cap R^{-1}) y \to x = y) \leftrightarrow \forall x \forall y ((x R y \land y R x) \to x = y)$
11	6 10	bitri	$⊢ CnvRefRel (R \cap R^{-1}) \leftrightarrow \forall x \forall y ((x R y \land y R x) \to x = y)$
12	1 11	bianbi	$⊢ AntisymRel R \leftrightarrow (\forall x \forall y ((x R y \land y R x) \to x = y) \land Rel R)$

Metamath Proof Explorer