This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 /. .~ ) )