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	|- ( ph -> R Er X )
	qsdisj.2	|- ( ph -> B e. ( A /. R ) )
	qsdisj.3	|- ( ph -> C e. ( A /. R ) )
Assertion	qsdisj	|- ( ph -> ( B = C \/ ( B i^i C ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		qsdisj.1	|- ( ph -> R Er X )
2		qsdisj.2	|- ( ph -> B e. ( A /. R ) )
3		qsdisj.3	|- ( ph -> C e. ( A /. R ) )
4		eqid	|- ( A /. R ) = ( A /. R )
5		eqeq1	|- ( [ x ] R = B -> ( [ x ] R = C <-> B = C ) )
6		ineq1	|- ( [ x ] R = B -> ( [ x ] R i^i C ) = ( B i^i C ) )
7	6	eqeq1d	|- ( [ x ] R = B -> ( ( [ x ] R i^i C ) = (/) <-> ( B i^i C ) = (/) ) )
8	5 7	orbi12d	|- ( [ x ] R = B -> ( ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) <-> ( B = C \/ ( B i^i C ) = (/) ) ) )
9		eqeq2	|- ( [ y ] R = C -> ( [ x ] R = [ y ] R <-> [ x ] R = C ) )
10		ineq2	|- ( [ y ] R = C -> ( [ x ] R i^i [ y ] R ) = ( [ x ] R i^i C ) )
11	10	eqeq1d	|- ( [ y ] R = C -> ( ( [ x ] R i^i [ y ] R ) = (/) <-> ( [ x ] R i^i C ) = (/) ) )
12	9 11	orbi12d	|- ( [ y ] R = C -> ( ( [ x ] R = [ y ] R \/ ( [ x ] R i^i [ y ] R ) = (/) ) <-> ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) ) )
13	1	ad2antrr	|- ( ( ( ph /\ x e. A ) /\ y e. A ) -> R Er X )
14		erdisj	|- ( R Er X -> ( [ x ] R = [ y ] R \/ ( [ x ] R i^i [ y ] R ) = (/) ) )
15	13 14	syl	|- ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( [ x ] R = [ y ] R \/ ( [ x ] R i^i [ y ] R ) = (/) ) )
16	4 12 15	ectocld	|- ( ( ( ph /\ x e. A ) /\ C e. ( A /. R ) ) -> ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) )
17	3 16	mpidan	|- ( ( ph /\ x e. A ) -> ( [ x ] R = C \/ ( [ x ] R i^i C ) = (/) ) )
18	4 8 17	ectocld	|- ( ( ph /\ B e. ( A /. R ) ) -> ( B = C \/ ( B i^i C ) = (/) ) )
19	2 18	mpdan	|- ( ph -> ( B = C \/ ( B i^i C ) = (/) ) )