Metamath Proof Explorer

Theorem erdisj

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)

Ref Expression
Assertion erdisj ( 𝑅 Er 𝑋 → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) )

Proof

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