Metamath Proof Explorer

Theorem eqvreldisj

Description: Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of Suppes p. 83. (Contributed by NM, 15-Jun-2004) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

Ref Expression
Assertion eqvreldisj 
|- ( EqvRel R -> ( [ A ] R = [ B ] R \/ ( [ A ] R i^i [ B ] R ) = (/) ) )

Proof

Step Hyp Ref Expression
1 neq0 
 |-  ( -. ( [ A ] R i^i [ B ] R ) = (/) <-> E. x x e. ( [ A ] R i^i [ B ] R ) )
2 simpl 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> EqvRel R )
3 elinel1 
 |-  ( x e. ( [ A ] R i^i [ B ] R ) -> x e. [ A ] R )
4 3 adantl 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> x e. [ A ] R )
5 ecexr 
 |-  ( x e. [ A ] R -> A e. _V )
6 4 5 syl 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> A e. _V )
7 vex 
 |-  x e. _V
8 elecALTV 
 |-  ( ( A e. _V /\ x e. _V ) -> ( x e. [ A ] R <-> A R x ) )
9 6 7 8 sylancl 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> ( x e. [ A ] R <-> A R x ) )
10 4 9 mpbid 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> A R x )
11 elinel2 
 |-  ( x e. ( [ A ] R i^i [ B ] R ) -> x e. [ B ] R )
12 11 adantl 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> x e. [ B ] R )
13 ecexr 
 |-  ( x e. [ B ] R -> B e. _V )
14 12 13 syl 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> B e. _V )
15 elecALTV 
 |-  ( ( B e. _V /\ x e. _V ) -> ( x e. [ B ] R <-> B R x ) )
16 14 7 15 sylancl 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> ( x e. [ B ] R <-> B R x ) )
17 12 16 mpbid 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> B R x )
18 2 10 17 eqvreltr4d 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> A R B )
19 2 18 eqvrelthi 
 |-  ( ( EqvRel R /\ x e. ( [ A ] R i^i [ B ] R ) ) -> [ A ] R = [ B ] R )
20 19 ex 
 |-  ( EqvRel R -> ( x e. ( [ A ] R i^i [ B ] R ) -> [ A ] R = [ B ] R ) )
21 20 exlimdv 
 |-  ( EqvRel R -> ( E. x x e. ( [ A ] R i^i [ B ] R ) -> [ A ] R = [ B ] R ) )
22 1 21 syl5bi 
 |-  ( EqvRel R -> ( -. ( [ A ] R i^i [ B ] R ) = (/) -> [ A ] R = [ B ] R ) )
23 22 orrd 
 |-  ( EqvRel R -> ( ( [ A ] R i^i [ B ] R ) = (/) \/ [ A ] R = [ B ] R ) )
24 23 orcomd 
 |-  ( EqvRel R -> ( [ A ] R = [ B ] R \/ ( [ A ] R i^i [ B ] R ) = (/) ) )