Theorem erprt

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

	Ref	Expression
Assertion	erprt	|- ( .~ Er X -> Prt ( A /. .~ ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( .~ Er X /\ ( x e. ( A /. .~ ) /\ y e. ( A /. .~ ) ) ) -> .~ Er X )
2		simprl	|- ( ( .~ Er X /\ ( x e. ( A /. .~ ) /\ y e. ( A /. .~ ) ) ) -> x e. ( A /. .~ ) )
3		simprr	|- ( ( .~ Er X /\ ( x e. ( A /. .~ ) /\ y e. ( A /. .~ ) ) ) -> y e. ( A /. .~ ) )
4	1 2 3	qsdisj	|- ( ( .~ Er X /\ ( x e. ( A /. .~ ) /\ y e. ( A /. .~ ) ) ) -> ( x = y \/ ( x i^i y ) = (/) ) )
5	4	ralrimivva	|- ( .~ Er X -> A. x e. ( A /. .~ ) A. y e. ( A /. .~ ) ( x = y \/ ( x i^i y ) = (/) ) )
6		df-prt	|- ( Prt ( A /. .~ ) <-> A. x e. ( A /. .~ ) A. y e. ( A /. .~ ) ( x = y \/ ( x i^i y ) = (/) ) )
7	5 6	sylibr	|- ( .~ Er X -> Prt ( A /. .~ ) )