erprt

Description: The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010)

		Ref	Expression
	Assertion	erprt	$⊢ \underset{˙}{\sim} Er X \to Prt (A / \underset{˙}{\sim})$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (\underset{˙}{\sim} Er X \land (x \in (A / \underset{˙}{\sim}) \land y \in (A / \underset{˙}{\sim}))) \to \underset{˙}{\sim} Er X$
2		simprl	$⊢ (\underset{˙}{\sim} Er X \land (x \in (A / \underset{˙}{\sim}) \land y \in (A / \underset{˙}{\sim}))) \to x \in (A / \underset{˙}{\sim})$
3		simprr	$⊢ (\underset{˙}{\sim} Er X \land (x \in (A / \underset{˙}{\sim}) \land y \in (A / \underset{˙}{\sim}))) \to y \in (A / \underset{˙}{\sim})$
4	1 2 3	qsdisj	$⊢ (\underset{˙}{\sim} Er X \land (x \in (A / \underset{˙}{\sim}) \land y \in (A / \underset{˙}{\sim}))) \to (x = y \lor x \cap y = \emptyset)$
5	4	ralrimivva	$⊢ \underset{˙}{\sim} Er X \to \forall x \in (A / \underset{˙}{\sim}) \forall y \in (A / \underset{˙}{\sim}) (x = y \lor x \cap y = \emptyset)$
6		df-prt	$⊢ Prt (A / \underset{˙}{\sim}) \leftrightarrow \forall x \in (A / \underset{˙}{\sim}) \forall y \in (A / \underset{˙}{\sim}) (x = y \lor x \cap y = \emptyset)$
7	5 6	sylibr	$⊢ \underset{˙}{\sim} Er X \to Prt (A / \underset{˙}{\sim})$

Metamath Proof Explorer