erdisj

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)

		Ref	Expression
	Assertion	erdisj	$⊢ R Er X \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	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to R Er X$
3		elinel1	$⊢ x \in ([A] R \cap [B] R) \to x \in [A] R$
4	3	adantl	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to x \in [A] R$
5		vex	$⊢ x \in V$
6		ecexr	$⊢ x \in [A] R \to A \in V$
7	4 6	syl	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to A \in V$
8		elecg	$⊢ (x \in V \land A \in V) \to (x \in [A] R \leftrightarrow A R x)$
9	5 7 8	sylancr	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to (x \in [A] R \leftrightarrow A R x)$
10	4 9	mpbid	$⊢ (R Er X \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	$⊢ (R Er X \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	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to B \in V$
15		elecg	$⊢ (x \in V \land B \in V) \to (x \in [B] R \leftrightarrow B R x)$
16	5 14 15	sylancr	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to (x \in [B] R \leftrightarrow B R x)$
17	12 16	mpbid	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to B R x$
18	2 10 17	ertr4d	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to A R B$
19	2 18	erthi	$⊢ (R Er X \land x \in ([A] R \cap [B] R)) \to [A] R = [B] R$
20	19	ex	$⊢ R Er X \to (x \in ([A] R \cap [B] R) \to [A] R = [B] R)$
21	20	exlimdv	$⊢ R Er X \to (\exists x x \in ([A] R \cap [B] R) \to [A] R = [B] R)$
22	1 21	biimtrid	$⊢ R Er X \to (\neg [A] R \cap [B] R = \emptyset \to [A] R = [B] R)$
23	22	orrd	$⊢ R Er X \to ([A] R \cap [B] R = \emptyset \lor [A] R = [B] R)$
24	23	orcomd	$⊢ R Er X \to ([A] R = [B] R \lor [A] R \cap [B] R = \emptyset)$

Metamath Proof Explorer

Theorem erdisj

Proof