Theorem qsdisj2

Description: A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016)

	Ref	Expression
Assertion	qsdisj2	⊢ ( 𝑅 Er 𝑋 → Disj 𝑥 ∈ ( 𝐴 / 𝑅 ) 𝑥 )

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		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
7	6	disjor	⊢ ( Disj 𝑥 ∈ ( 𝐴 / 𝑅 ) 𝑥 ↔ ∀ 𝑥 ∈ ( 𝐴 / 𝑅 ) ∀ 𝑦 ∈ ( 𝐴 / 𝑅 ) ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
8	5 7	sylibr	⊢ ( 𝑅 Er 𝑋 → Disj 𝑥 ∈ ( 𝐴 / 𝑅 ) 𝑥 )