asymref2

Description: Two ways of saying a relation is antisymmetric and reflexive. (Contributed by NM, 6-May-2008) (Proof shortened by Mario Carneiro, 4-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		asymref	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \leftrightarrow \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \leftrightarrow x = y)$
2		albiim	$⊢ \forall y ((x R y \land y R x) \leftrightarrow x = y) \leftrightarrow (\forall y ((x R y \land y R x) \to x = y) \land \forall y (x = y \to (x R y \land y R x)))$
3	2	ralbii	$⊢ \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \leftrightarrow x = y) \leftrightarrow \forall x \in ⋃ ⋃ R (\forall y ((x R y \land y R x) \to x = y) \land \forall y (x = y \to (x R y \land y R x)))$
4		r19.26	$⊢ \forall x \in ⋃ ⋃ R (\forall y ((x R y \land y R x) \to x = y) \land \forall y (x = y \to (x R y \land y R x))) \leftrightarrow (\forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \to x = y) \land \forall x \in ⋃ ⋃ R \forall y (x = y \to (x R y \land y R x)))$
5		ancom	$⊢ (\forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \to x = y) \land \forall x \in ⋃ ⋃ R \forall y (x = y \to (x R y \land y R x))) \leftrightarrow (\forall x \in ⋃ ⋃ R \forall y (x = y \to (x R y \land y R x)) \land \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \to x = y))$
6		equcom	$⊢ x = y \leftrightarrow y = x$
7	6	imbi1i	$⊢ (x = y \to (x R y \land y R x)) \leftrightarrow (y = x \to (x R y \land y R x))$
8	7	albii	$⊢ \forall y (x = y \to (x R y \land y R x)) \leftrightarrow \forall y (y = x \to (x R y \land y R x))$
9		breq2	$⊢ y = x \to (x R y \leftrightarrow x R x)$
10		breq1	$⊢ y = x \to (y R x \leftrightarrow x R x)$
11	9 10	anbi12d	$⊢ y = x \to ((x R y \land y R x) \leftrightarrow (x R x \land x R x))$
12		anidm	$⊢ (x R x \land x R x) \leftrightarrow x R x$
13	11 12	bitrdi	$⊢ y = x \to ((x R y \land y R x) \leftrightarrow x R x)$
14	13	equsalvw	$⊢ \forall y (y = x \to (x R y \land y R x)) \leftrightarrow x R x$
15	8 14	bitri	$⊢ \forall y (x = y \to (x R y \land y R x)) \leftrightarrow x R x$
16	15	ralbii	$⊢ \forall x \in ⋃ ⋃ R \forall y (x = y \to (x R y \land y R x)) \leftrightarrow \forall x \in ⋃ ⋃ R x R x$
17		df-ral	$⊢ \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \to x = y) \leftrightarrow \forall x (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \to x = y))$
18		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
19		vex	$⊢ x \in V$
20		vex	$⊢ y \in V$
21	19 20	opeluu	$⊢ ⟨x, y⟩ \in R \to (x \in ⋃ ⋃ R \land y \in ⋃ ⋃ R)$
22	21	simpld	$⊢ ⟨x, y⟩ \in R \to x \in ⋃ ⋃ R$
23	18 22	sylbi	$⊢ x R y \to x \in ⋃ ⋃ R$
24	23	adantr	$⊢ (x R y \land y R x) \to x \in ⋃ ⋃ R$
25	24	pm2.24d	$⊢ (x R y \land y R x) \to (\neg x \in ⋃ ⋃ R \to x = y)$
26	25	com12	$⊢ \neg x \in ⋃ ⋃ R \to ((x R y \land y R x) \to x = y)$
27	26	alrimiv	$⊢ \neg x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \to x = y)$
28		id	$⊢ \forall y ((x R y \land y R x) \to x = y) \to \forall y ((x R y \land y R x) \to x = y)$
29	27 28	ja	$⊢ (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \to x = y)) \to \forall y ((x R y \land y R x) \to x = y)$
30		ax-1	$⊢ \forall y ((x R y \land y R x) \to x = y) \to (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \to x = y))$
31	29 30	impbii	$⊢ (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \to x = y)) \leftrightarrow \forall y ((x R y \land y R x) \to x = y)$
32	31	albii	$⊢ \forall x (x \in ⋃ ⋃ R \to \forall y ((x R y \land y R x) \to x = y)) \leftrightarrow \forall x \forall y ((x R y \land y R x) \to x = y)$
33	17 32	bitri	$⊢ \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \to x = y) \leftrightarrow \forall x \forall y ((x R y \land y R x) \to x = y)$
34	16 33	anbi12i	$⊢ (\forall x \in ⋃ ⋃ R \forall y (x = y \to (x R y \land y R x)) \land \forall x \in ⋃ ⋃ R \forall y ((x R y \land y R x) \to x = y)) \leftrightarrow (\forall x \in ⋃ ⋃ R x R x \land \forall x \forall y ((x R y \land y R x) \to x = y))$
35	4 5 34	3bitri	$⊢ \forall x \in ⋃ ⋃ R (\forall y ((x R y \land y R x) \to x = y) \land \forall y (x = y \to (x R y \land y R x))) \leftrightarrow (\forall x \in ⋃ ⋃ R x R x \land \forall x \forall y ((x R y \land y R x) \to x = y))$
36	1 3 35	3bitri	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \leftrightarrow (\forall x \in ⋃ ⋃ R x R x \land \forall x \forall y ((x R y \land y R x) \to x = y))$

Metamath Proof Explorer

Theorem asymref2

Proof