Theorem qsdisj

Description: Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010) (Revised by Mario Carneiro, 11-Jul-2014)

	Ref	Expression
Hypotheses	qsdisj.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
	qsdisj.2	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 / 𝑅 ) )
	qsdisj.3	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 / 𝑅 ) )
Assertion	qsdisj	⊢ ( 𝜑 → ( 𝐵 = 𝐶 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		qsdisj.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2		qsdisj.2	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 / 𝑅 ) )
3		qsdisj.3	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 / 𝑅 ) )
4		eqid	⊢ ( 𝐴 / 𝑅 ) = ( 𝐴 / 𝑅 )
5		eqeq1	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( [ 𝑥 ] 𝑅 = 𝐶 ↔ 𝐵 = 𝐶 ) )
6		ineq1	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) )
7	6	eqeq1d	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) = ∅ ↔ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
8	5 7	orbi12d	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) = ∅ ) ↔ ( 𝐵 = 𝐶 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ) )
9		eqeq2	⊢ ( [ 𝑦 ] 𝑅 = 𝐶 → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ↔ [ 𝑥 ] 𝑅 = 𝐶 ) )
10		ineq2	⊢ ( [ 𝑦 ] 𝑅 = 𝐶 → ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) )
11	10	eqeq1d	⊢ ( [ 𝑦 ] 𝑅 = 𝐶 → ( ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ↔ ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) = ∅ ) )
12	9 11	orbi12d	⊢ ( [ 𝑦 ] 𝑅 = 𝐶 → ( ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) ↔ ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) = ∅ ) ) )
13	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑅 Er 𝑋 )
14		erdisj	⊢ ( 𝑅 Er 𝑋 → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) )
15	13 14	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) )
16	4 12 15	ectocld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ∈ ( 𝐴 / 𝑅 ) ) → ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) = ∅ ) )
17	3 16	mpidan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅 ∩ 𝐶 ) = ∅ ) )
18	4 8 17	ectocld	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ) → ( 𝐵 = 𝐶 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
19	2 18	mpdan	⊢ ( 𝜑 → ( 𝐵 = 𝐶 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )