This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qsdisjALTV

Description: Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010) (Revised by Mario Carneiro, 11-Jul-2014) (Revised by Peter Mazsa, 3-Jun-2019)

Ref Expression
Hypotheses qsdisjALTV.1 
|- ( ph -> EqvRel R )
qsdisjALTV.2 
|- ( ph -> B e. ( A /. R ) )
qsdisjALTV.3 
|- ( ph -> C e. ( A /. R ) )
Assertion qsdisjALTV 
|- ( ph -> ( B = C \/ ( B i^i C ) = (/) ) )

Proof

Step Hyp Ref Expression
1 qsdisjALTV.1 
 |-  ( ph -> EqvRel R )
2 qsdisjALTV.2 
 |-  ( ph -> B e. ( A /. R ) )
3 qsdisjALTV.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 ) -> EqvRel R )
14 eqvreldisj 
 |-  ( EqvRel R -> ( [ 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 ) = (/) ) )