qsdisj2

Description: A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016)

		Ref	Expression
	Assertion	qsdisj2	$⊢ R Er X \to \underset{x \in A / R}{Disj} x$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (R Er X \land (x \in (A / R) \land y \in (A / R))) \to R Er X$
2		simprl	$⊢ (R Er X \land (x \in (A / R) \land y \in (A / R))) \to x \in (A / R)$
3		simprr	$⊢ (R Er X \land (x \in (A / R) \land y \in (A / R))) \to y \in (A / R)$
4	1 2 3	qsdisj	$⊢ (R Er X \land (x \in (A / R) \land y \in (A / R))) \to (x = y \lor x \cap y = \emptyset)$
5	4	ralrimivva	$⊢ R Er X \to \forall x \in (A / R) \forall y \in (A / R) (x = y \lor x \cap y = \emptyset)$
6		id	$⊢ x = y \to x = y$
7	6	disjor	$⊢ \underset{x \in A / R}{Disj} x \leftrightarrow \forall x \in (A / R) \forall y \in (A / R) (x = y \lor x \cap y = \emptyset)$
8	5 7	sylibr	$⊢ R Er X \to \underset{x \in A / R}{Disj} x$

Metamath Proof Explorer