Metamath Proof Explorer

Theorem intasym

Description: Two ways of saying a relation is antisymmetric. Definition of antisymmetry in Schechter p. 51. (Contributed by NM, 9-Sep-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	intasym	$⊢ R \cap R^{-1} \subseteq I \leftrightarrow \forall x \forall y ((x R y \land y R x) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel R^{-1}$
2		relin2	$⊢ Rel R^{-1} \to Rel (R \cap R^{-1})$
3		ssrel	$⊢ Rel (R \cap R^{-1}) \to (R \cap R^{-1} \subseteq I \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \to ⟨x, y⟩ \in I))$
4	1 2 3	mp2b	$⊢ R \cap R^{-1} \subseteq I \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \to ⟨x, y⟩ \in I)$
5		elin	$⊢ ⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow (⟨x, y⟩ \in R \land ⟨x, y⟩ \in R^{-1})$
6		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	brcnv	$⊢ x R^{-1} y \leftrightarrow y R x$
10		df-br	$⊢ x R^{-1} y \leftrightarrow ⟨x, y⟩ \in R^{-1}$
11	9 10	bitr3i	$⊢ y R x \leftrightarrow ⟨x, y⟩ \in R^{-1}$
12	6 11	anbi12i	$⊢ (x R y \land y R x) \leftrightarrow (⟨x, y⟩ \in R \land ⟨x, y⟩ \in R^{-1})$
13	5 12	bitr4i	$⊢ ⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow (x R y \land y R x)$
14		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
15	8	ideq	$⊢ x I y \leftrightarrow x = y$
16	14 15	bitr3i	$⊢ ⟨x, y⟩ \in I \leftrightarrow x = y$
17	13 16	imbi12i	$⊢ (⟨x, y⟩ \in (R \cap R^{-1}) \to ⟨x, y⟩ \in I) \leftrightarrow ((x R y \land y R x) \to x = y)$
18	17	2albii	$⊢ \forall x \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \to ⟨x, y⟩ \in I) \leftrightarrow \forall x \forall y ((x R y \land y R x) \to x = y)$
19	4 18	bitri	$⊢ R \cap R^{-1} \subseteq I \leftrightarrow \forall x \forall y ((x R y \land y R x) \to x = y)$