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