qsdisj

Description: Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010) (Revised by Mario Carneiro, 11-Jul-2014)

Step	Hyp	Ref	Expression
1		qsdisj.1	$⊢ φ \to R Er X$
2		qsdisj.2	$⊢ φ \to B \in (A / R)$
3		qsdisj.3	$⊢ φ \to C \in (A / R)$
4		eqid	$⊢ A / R = A / R$
5		eqeq1	$⊢ [x] R = B \to ([x] R = C \leftrightarrow B = C)$
6		ineq1	$⊢ [x] R = B \to [x] R \cap C = B \cap C$
7	6	eqeq1d	$⊢ [x] R = B \to ([x] R \cap C = \emptyset \leftrightarrow B \cap C = \emptyset)$
8	5 7	orbi12d	$⊢ [x] R = B \to (([x] R = C \lor [x] R \cap C = \emptyset) \leftrightarrow (B = C \lor B \cap C = \emptyset))$
9		eqeq2	$⊢ [y] R = C \to ([x] R = [y] R \leftrightarrow [x] R = C)$
10		ineq2	$⊢ [y] R = C \to [x] R \cap [y] R = [x] R \cap C$
11	10	eqeq1d	$⊢ [y] R = C \to ([x] R \cap [y] R = \emptyset \leftrightarrow [x] R \cap C = \emptyset)$
12	9 11	orbi12d	$⊢ [y] R = C \to (([x] R = [y] R \lor [x] R \cap [y] R = \emptyset) \leftrightarrow ([x] R = C \lor [x] R \cap C = \emptyset))$
13	1	ad2antrr	$⊢ ((φ \land x \in A) \land y \in A) \to R Er X$
14		erdisj	$⊢ R Er X \to ([x] R = [y] R \lor [x] R \cap [y] R = \emptyset)$
15	13 14	syl	$⊢ ((φ \land x \in A) \land y \in A) \to ([x] R = [y] R \lor [x] R \cap [y] R = \emptyset)$
16	4 12 15	ectocld	$⊢ ((φ \land x \in A) \land C \in (A / R)) \to ([x] R = C \lor [x] R \cap C = \emptyset)$
17	3 16	mpidan	$⊢ (φ \land x \in A) \to ([x] R = C \lor [x] R \cap C = \emptyset)$
18	4 8 17	ectocld	$⊢ (φ \land B \in (A / R)) \to (B = C \lor B \cap C = \emptyset)$
19	2 18	mpdan	$⊢ φ \to (B = C \lor B \cap C = \emptyset)$

Metamath Proof Explorer