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

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 𝑅 → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 neq0 ⊢ ( ¬ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) )
2 simpl ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → EqvRel 𝑅 )
3 elinel1 ⊢ ( 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) → 𝑥 ∈ [ 𝐴 ] 𝑅 )
4 3 adantl ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → 𝑥 ∈ [ 𝐴 ] 𝑅 )
5 ecexr ⊢ ( 𝑥 ∈ [ 𝐴 ] 𝑅 → 𝐴 ∈ V )
6 4 5 syl ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → 𝐴 ∈ V )
7 vex ⊢ 𝑥 ∈ V
8 elecALTV ⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
9 6 7 8 sylancl ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
10 4 9 mpbid ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → 𝐴 𝑅 𝑥 )
11 elinel2 ⊢ ( 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) → 𝑥 ∈ [ 𝐵 ] 𝑅 )
12 11 adantl ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → 𝑥 ∈ [ 𝐵 ] 𝑅 )
13 ecexr ⊢ ( 𝑥 ∈ [ 𝐵 ] 𝑅 → 𝐵 ∈ V )
14 12 13 syl ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → 𝐵 ∈ V )
15 elecALTV ⊢ ( ( 𝐵 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) )
16 14 7 15 sylancl ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) )
17 12 16 mpbid ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → 𝐵 𝑅 𝑥 )
18 2 10 17 eqvreltr4d ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → 𝐴 𝑅 𝐵 )
19 2 18 eqvrelthi ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ) → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
20 19 ex ⊢ ( EqvRel 𝑅 → ( 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
21 20 exlimdv ⊢ ( EqvRel 𝑅 → ( ∃ 𝑥 𝑥 ∈ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
22 1 21 biimtrid ⊢ ( EqvRel 𝑅 → ( ¬ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
23 22 orrd ⊢ ( EqvRel 𝑅 → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
24 23 orcomd ⊢ ( EqvRel 𝑅 → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) )