brinxper

Description: Conditions for a reflexive, symmetric and transitive binary relation to be an equivalence relation over a class V . (Contributed by AV, 11-Jun-2025)

	Ref	Expression
Hypotheses	brinxper.r	$⊢ x \in V \to x \underset{˙}{\sim} x$
	brinxper.s	$⊢ x \in V \to (x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x)$
	brinxper.t	$⊢ x \in V \to ((x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z)$
Assertion	brinxper	$⊢ (\underset{˙}{\sim} \cap (V \times V)) Er V$

Proof

Step	Hyp	Ref	Expression
1		brinxper.r	$⊢ x \in V \to x \underset{˙}{\sim} x$
2		brinxper.s	$⊢ x \in V \to (x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x)$
3		brinxper.t	$⊢ x \in V \to ((x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z)$
4		relinxp	$⊢ Rel (\underset{˙}{\sim} \cap (V \times V))$
5		brxp	$⊢ x (V \times V) y \leftrightarrow (x \in V \land y \in V)$
6	2	adantr	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x)$
7		ancom	$⊢ (x \in V \land y \in V) \leftrightarrow (y \in V \land x \in V)$
8		brxp	$⊢ y (V \times V) x \leftrightarrow (y \in V \land x \in V)$
9	7 8	sylbb2	$⊢ (x \in V \land y \in V) \to y (V \times V) x$
10	6 9	jctird	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to (y \underset{˙}{\sim} x \land y (V \times V) x))$
11	5 10	sylbi	$⊢ x (V \times V) y \to (x \underset{˙}{\sim} y \to (y \underset{˙}{\sim} x \land y (V \times V) x))$
12	11	impcom	$⊢ (x \underset{˙}{\sim} y \land x (V \times V) y) \to (y \underset{˙}{\sim} x \land y (V \times V) x)$
13		brin	$⊢ x (\underset{˙}{\sim} \cap (V \times V)) y \leftrightarrow (x \underset{˙}{\sim} y \land x (V \times V) y)$
14		brin	$⊢ y (\underset{˙}{\sim} \cap (V \times V)) x \leftrightarrow (y \underset{˙}{\sim} x \land y (V \times V) x)$
15	12 13 14	3imtr4i	$⊢ x (\underset{˙}{\sim} \cap (V \times V)) y \to y (\underset{˙}{\sim} \cap (V \times V)) x$
16		brin	$⊢ y (\underset{˙}{\sim} \cap (V \times V)) z \leftrightarrow (y \underset{˙}{\sim} z \land y (V \times V) z)$
17		brxp	$⊢ y (V \times V) z \leftrightarrow (y \in V \land z \in V)$
18	3	expd	$⊢ x \in V \to (x \underset{˙}{\sim} y \to (y \underset{˙}{\sim} z \to x \underset{˙}{\sim} z))$
19	18	adantr	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to (y \underset{˙}{\sim} z \to x \underset{˙}{\sim} z))$
20	19	impcom	$⊢ (x \underset{˙}{\sim} y \land (x \in V \land y \in V)) \to (y \underset{˙}{\sim} z \to x \underset{˙}{\sim} z)$
21	20	com12	$⊢ y \underset{˙}{\sim} z \to ((x \underset{˙}{\sim} y \land (x \in V \land y \in V)) \to x \underset{˙}{\sim} z)$
22	21	adantl	$⊢ ((y \in V \land z \in V) \land y \underset{˙}{\sim} z) \to ((x \underset{˙}{\sim} y \land (x \in V \land y \in V)) \to x \underset{˙}{\sim} z)$
23	22	imp	$⊢ (((y \in V \land z \in V) \land y \underset{˙}{\sim} z) \land (x \underset{˙}{\sim} y \land (x \in V \land y \in V))) \to x \underset{˙}{\sim} z$
24		simplr	$⊢ ((y \in V \land z \in V) \land y \underset{˙}{\sim} z) \to z \in V$
25		simprl	$⊢ (x \underset{˙}{\sim} y \land (x \in V \land y \in V)) \to x \in V$
26	24 25	anim12ci	$⊢ (((y \in V \land z \in V) \land y \underset{˙}{\sim} z) \land (x \underset{˙}{\sim} y \land (x \in V \land y \in V))) \to (x \in V \land z \in V)$
27	23 26	jca	$⊢ (((y \in V \land z \in V) \land y \underset{˙}{\sim} z) \land (x \underset{˙}{\sim} y \land (x \in V \land y \in V))) \to (x \underset{˙}{\sim} z \land (x \in V \land z \in V))$
28	27	exp31	$⊢ (y \in V \land z \in V) \to (y \underset{˙}{\sim} z \to ((x \underset{˙}{\sim} y \land (x \in V \land y \in V)) \to (x \underset{˙}{\sim} z \land (x \in V \land z \in V))))$
29	17 28	sylbi	$⊢ y (V \times V) z \to (y \underset{˙}{\sim} z \to ((x \underset{˙}{\sim} y \land (x \in V \land y \in V)) \to (x \underset{˙}{\sim} z \land (x \in V \land z \in V))))$
30	29	impcom	$⊢ (y \underset{˙}{\sim} z \land y (V \times V) z) \to ((x \underset{˙}{\sim} y \land (x \in V \land y \in V)) \to (x \underset{˙}{\sim} z \land (x \in V \land z \in V)))$
31	5	anbi2i	$⊢ (x \underset{˙}{\sim} y \land x (V \times V) y) \leftrightarrow (x \underset{˙}{\sim} y \land (x \in V \land y \in V))$
32		brxp	$⊢ x (V \times V) z \leftrightarrow (x \in V \land z \in V)$
33	32	anbi2i	$⊢ (x \underset{˙}{\sim} z \land x (V \times V) z) \leftrightarrow (x \underset{˙}{\sim} z \land (x \in V \land z \in V))$
34	30 31 33	3imtr4g	$⊢ (y \underset{˙}{\sim} z \land y (V \times V) z) \to ((x \underset{˙}{\sim} y \land x (V \times V) y) \to (x \underset{˙}{\sim} z \land x (V \times V) z))$
35	16 34	sylbi	$⊢ y (\underset{˙}{\sim} \cap (V \times V)) z \to ((x \underset{˙}{\sim} y \land x (V \times V) y) \to (x \underset{˙}{\sim} z \land x (V \times V) z))$
36	35	com12	$⊢ (x \underset{˙}{\sim} y \land x (V \times V) y) \to (y (\underset{˙}{\sim} \cap (V \times V)) z \to (x \underset{˙}{\sim} z \land x (V \times V) z))$
37	13 36	sylbi	$⊢ x (\underset{˙}{\sim} \cap (V \times V)) y \to (y (\underset{˙}{\sim} \cap (V \times V)) z \to (x \underset{˙}{\sim} z \land x (V \times V) z))$
38	37	imp	$⊢ (x (\underset{˙}{\sim} \cap (V \times V)) y \land y (\underset{˙}{\sim} \cap (V \times V)) z) \to (x \underset{˙}{\sim} z \land x (V \times V) z)$
39		brin	$⊢ x (\underset{˙}{\sim} \cap (V \times V)) z \leftrightarrow (x \underset{˙}{\sim} z \land x (V \times V) z)$
40	38 39	sylibr	$⊢ (x (\underset{˙}{\sim} \cap (V \times V)) y \land y (\underset{˙}{\sim} \cap (V \times V)) z) \to x (\underset{˙}{\sim} \cap (V \times V)) z$
41		id	$⊢ x \in V \to x \in V$
42		brxp	$⊢ x (V \times V) x \leftrightarrow (x \in V \land x \in V)$
43	41 41 42	sylanbrc	$⊢ x \in V \to x (V \times V) x$
44	1 43	jca	$⊢ x \in V \to (x \underset{˙}{\sim} x \land x (V \times V) x)$
45	42	simplbi	$⊢ x (V \times V) x \to x \in V$
46	45	adantl	$⊢ (x \underset{˙}{\sim} x \land x (V \times V) x) \to x \in V$
47	44 46	impbii	$⊢ x \in V \leftrightarrow (x \underset{˙}{\sim} x \land x (V \times V) x)$
48		brin	$⊢ x (\underset{˙}{\sim} \cap (V \times V)) x \leftrightarrow (x \underset{˙}{\sim} x \land x (V \times V) x)$
49	47 48	bitr4i	$⊢ x \in V \leftrightarrow x (\underset{˙}{\sim} \cap (V \times V)) x$
50	4 15 40 49	iseri	$⊢ (\underset{˙}{\sim} \cap (V \times V)) Er V$

Metamath Proof Explorer

Theorem brinxper

Proof