eqvreldisj

Description: Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of Suppes p. 83. (Contributed by NM, 15-Jun-2004) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

		Ref	Expression
	Assertion	eqvreldisj	$⊢ EqvRel R \to ([A] R = [B] R \lor [A] R \cap [B] R = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		neq0	$⊢ \neg [A] R \cap [B] R = \emptyset \leftrightarrow \exists x x \in ([A] R \cap [B] R)$
2		simpl	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to EqvRel R$
3		elinel1	$⊢ x \in ([A] R \cap [B] R) \to x \in [A] R$
4	3	adantl	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to x \in [A] R$
5		ecexr	$⊢ x \in [A] R \to A \in V$
6	4 5	syl	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to A \in V$
7		vex	$⊢ x \in V$
8		elecALTV	$⊢ (A \in V \land x \in V) \to (x \in [A] R \leftrightarrow A R x)$
9	6 7 8	sylancl	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to (x \in [A] R \leftrightarrow A R x)$
10	4 9	mpbid	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to A R x$
11		elinel2	$⊢ x \in ([A] R \cap [B] R) \to x \in [B] R$
12	11	adantl	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to x \in [B] R$
13		ecexr	$⊢ x \in [B] R \to B \in V$
14	12 13	syl	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to B \in V$
15		elecALTV	$⊢ (B \in V \land x \in V) \to (x \in [B] R \leftrightarrow B R x)$
16	14 7 15	sylancl	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to (x \in [B] R \leftrightarrow B R x)$
17	12 16	mpbid	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to B R x$
18	2 10 17	eqvreltr4d	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to A R B$
19	2 18	eqvrelthi	$⊢ (EqvRel R \land x \in ([A] R \cap [B] R)) \to [A] R = [B] R$
20	19	ex	$⊢ EqvRel R \to (x \in ([A] R \cap [B] R) \to [A] R = [B] R)$
21	20	exlimdv	$⊢ EqvRel R \to (\exists x x \in ([A] R \cap [B] R) \to [A] R = [B] R)$
22	1 21	biimtrid	$⊢ EqvRel R \to (\neg [A] R \cap [B] R = \emptyset \to [A] R = [B] R)$
23	22	orrd	$⊢ EqvRel R \to ([A] R \cap [B] R = \emptyset \lor [A] R = [B] R)$
24	23	orcomd	$⊢ EqvRel R \to ([A] R = [B] R \lor [A] R \cap [B] R = \emptyset)$

Metamath Proof Explorer

Theorem eqvreldisj

Proof