asymref

Description: Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld . (Contributed by NM, 6-May-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	asymref	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \leftrightarrow \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \leftrightarrow x = y)$

Proof

Step	Hyp	Ref	Expression
1		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	opeluu	$⊢ ⟨x, y⟩ \in R \to (x \in ⋃ ⋃ R \land y \in ⋃ ⋃ R)$
5	1 4	sylbi	$⊢ x R y \to (x \in ⋃ ⋃ R \land y \in ⋃ ⋃ R)$
6	5	simpld	$⊢ x R y \to x \in ⋃ ⋃ R$
7	6	adantr	$⊢ (x R y \land y R x) \to x \in ⋃ ⋃ R$
8	7	pm4.71ri	$⊢ (x R y \land y R x) \leftrightarrow (x \in ⋃ ⋃ R \land (x R y \land y R x))$
9	8	bibi1i	$⊢ ((x R y \land y R x) \leftrightarrow (x \in ⋃ ⋃ R \land x = y)) \leftrightarrow ((x \in ⋃ ⋃ R \land (x R y \land y R x)) \leftrightarrow (x \in ⋃ ⋃ R \land x = y))$
10		elin	$⊢ ⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow (⟨x, y⟩ \in R \land ⟨x, y⟩ \in R^{-1})$
11	2 3	brcnv	$⊢ x R^{-1} y \leftrightarrow y R x$
12		df-br	$⊢ x R^{-1} y \leftrightarrow ⟨x, y⟩ \in R^{-1}$
13	11 12	bitr3i	$⊢ y R x \leftrightarrow ⟨x, y⟩ \in R^{-1}$
14	1 13	anbi12i	$⊢ (x R y \land y R x) \leftrightarrow (⟨x, y⟩ \in R \land ⟨x, y⟩ \in R^{-1})$
15	10 14	bitr4i	$⊢ ⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow (x R y \land y R x)$
16	3	opelresi	$⊢ ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R}) \leftrightarrow (x \in ⋃ ⋃ R \land ⟨x, y⟩ \in I)$
17		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
18	3	ideq	$⊢ x I y \leftrightarrow x = y$
19	17 18	bitr3i	$⊢ ⟨x, y⟩ \in I \leftrightarrow x = y$
20	19	anbi2i	$⊢ (x \in ⋃ ⋃ R \land ⟨x, y⟩ \in I) \leftrightarrow (x \in ⋃ ⋃ R \land x = y)$
21	16 20	bitri	$⊢ ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R}) \leftrightarrow (x \in ⋃ ⋃ R \land x = y)$
22	15 21	bibi12i	$⊢ (⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R})) \leftrightarrow ((x R y \land y R x) \leftrightarrow (x \in ⋃ ⋃ R \land x = y))$
23		pm5.32	$⊢ (x \in ⋃ ⋃ R \to ((x R y \land y R x) \leftrightarrow x = y)) \leftrightarrow ((x \in ⋃ ⋃ R \land (x R y \land y R x)) \leftrightarrow (x \in ⋃ ⋃ R \land x = y))$
24	9 22 23	3bitr4i	$⊢ (⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R})) \leftrightarrow (x \in ⋃ ⋃ R \to ((x R y \land y R x) \leftrightarrow x = y))$
25	24	albii	$⊢ \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R})) \leftrightarrow \forall y (x \in ⋃ ⋃ R \to ((x R y \land y R x) \leftrightarrow x = y))$
26		19.21v	$⊢ \forall y (x \in ⋃ ⋃ R \to ((x R y \land y R x) \leftrightarrow x = y)) \leftrightarrow (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \leftrightarrow x = y))$
27	25 26	bitri	$⊢ \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R})) \leftrightarrow (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \leftrightarrow x = y))$
28	27	albii	$⊢ \forall x \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R})) \leftrightarrow \forall x (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \leftrightarrow x = y))$
29		relcnv	$⊢ Rel R^{-1}$
30		relin2	$⊢ Rel R^{-1} \to Rel (R \cap R^{-1})$
31	29 30	ax-mp	$⊢ Rel (R \cap R^{-1})$
32		relres	$⊢ Rel ({I ↾}_{⋃ ⋃ R})$
33		eqrel	$⊢ (Rel (R \cap R^{-1}) \land Rel ({I ↾}_{⋃ ⋃ R})) \to (R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R})))$
34	31 32 33	mp2an	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (R \cap R^{-1}) \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{⋃ ⋃ R}))$
35		df-ral	$⊢ \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \leftrightarrow x = y) \leftrightarrow \forall x (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \leftrightarrow x = y))$
36	28 34 35	3bitr4i	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \leftrightarrow \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \leftrightarrow x = y)$

Metamath Proof Explorer

Theorem asymref

Proof