Metamath Proof Explorer

Theorem antisymrelres

Description: (Contributed by Peter Mazsa, 25-Jun-2024)

		Ref	Expression
	Assertion	antisymrelres	$⊢ AntisymRel ({R ↾}_{A}) \leftrightarrow \forall x \in A \forall y \in A ((x R y \land y R x) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({R ↾}_{A})$
2		dfantisymrel5	$⊢ AntisymRel ({R ↾}_{A}) \leftrightarrow (\forall x \forall y ((x ({R ↾}_{A}) y \land y ({R ↾}_{A}) x) \to x = y) \land Rel ({R ↾}_{A}))$
3	1 2	mpbiran2	$⊢ AntisymRel ({R ↾}_{A}) \leftrightarrow \forall x \forall y ((x ({R ↾}_{A}) y \land y ({R ↾}_{A}) x) \to x = y)$
4		brres	$⊢ y \in V \to (x ({R ↾}_{A}) y \leftrightarrow (x \in A \land x R y))$
5	4	elv	$⊢ x ({R ↾}_{A}) y \leftrightarrow (x \in A \land x R y)$
6		brres	$⊢ x \in V \to (y ({R ↾}_{A}) x \leftrightarrow (y \in A \land y R x))$
7	6	elv	$⊢ y ({R ↾}_{A}) x \leftrightarrow (y \in A \land y R x)$
8	5 7	anbi12i	$⊢ (x ({R ↾}_{A}) y \land y ({R ↾}_{A}) x) \leftrightarrow ((x \in A \land x R y) \land (y \in A \land y R x))$
9		an4	$⊢ ((x \in A \land x R y) \land (y \in A \land y R x)) \leftrightarrow ((x \in A \land y \in A) \land (x R y \land y R x))$
10	8 9	bitri	$⊢ (x ({R ↾}_{A}) y \land y ({R ↾}_{A}) x) \leftrightarrow ((x \in A \land y \in A) \land (x R y \land y R x))$
11	10	imbi1i	$⊢ ((x ({R ↾}_{A}) y \land y ({R ↾}_{A}) x) \to x = y) \leftrightarrow (((x \in A \land y \in A) \land (x R y \land y R x)) \to x = y)$
12	11	2albii	$⊢ \forall x \forall y ((x ({R ↾}_{A}) y \land y ({R ↾}_{A}) x) \to x = y) \leftrightarrow \forall x \forall y (((x \in A \land y \in A) \land (x R y \land y R x)) \to x = y)$
13		r2alan	$⊢ \forall x \forall y (((x \in A \land y \in A) \land (x R y \land y R x)) \to x = y) \leftrightarrow \forall x \in A \forall y \in A ((x R y \land y R x) \to x = y)$
14	3 12 13	3bitri	$⊢ AntisymRel ({R ↾}_{A}) \leftrightarrow \forall x \in A \forall y \in A ((x R y \land y R x) \to x = y)$