Metamath Proof Explorer

Theorem qsdisjALTV

Description: Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010) (Revised by Mario Carneiro, 11-Jul-2014) (Revised by Peter Mazsa, 3-Jun-2019)

		Ref	Expression
	Hypotheses	qsdisjALTV.1	$⊢ φ \to EqvRel R$
		qsdisjALTV.2	$⊢ φ \to B \in (A / R)$
		qsdisjALTV.3	$⊢ φ \to C \in (A / R)$
	Assertion	qsdisjALTV	$⊢ φ \to (B = C \lor B \cap C = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		qsdisjALTV.1	$⊢ φ \to EqvRel R$
2		qsdisjALTV.2	$⊢ φ \to B \in (A / R)$
3		qsdisjALTV.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 EqvRel R$
14		eqvreldisj	$⊢ EqvRel R \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)$