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 𝑋 → Prt ( 𝐴 / ∼ ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( ∼ Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / ∼ ) ∧ 𝑦 ∈ ( 𝐴 / ∼ ) ) ) → ∼ Er 𝑋 )
2 simprl ⊢ ( ( ∼ Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / ∼ ) ∧ 𝑦 ∈ ( 𝐴 / ∼ ) ) ) → 𝑥 ∈ ( 𝐴 / ∼ ) )
3 simprr ⊢ ( ( ∼ Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / ∼ ) ∧ 𝑦 ∈ ( 𝐴 / ∼ ) ) ) → 𝑦 ∈ ( 𝐴 / ∼ ) )
4 1 2 3 qsdisj ⊢ ( ( ∼ Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / ∼ ) ∧ 𝑦 ∈ ( 𝐴 / ∼ ) ) ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
5 4 ralrimivva ⊢ ( ∼ Er 𝑋 → ∀ 𝑥 ∈ ( 𝐴 / ∼ ) ∀ 𝑦 ∈ ( 𝐴 / ∼ ) ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
6 df-prt ⊢ ( Prt ( 𝐴 / ∼ ) ↔ ∀ 𝑥 ∈ ( 𝐴 / ∼ ) ∀ 𝑦 ∈ ( 𝐴 / ∼ ) ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
7 5 6 sylibr ⊢ ( ∼ Er 𝑋 → Prt ( 𝐴 / ∼ ) )