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	syl5bi	⊢ ( EqvRel 𝑅 → ( ¬ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
23	22	orrd	⊢ ( EqvRel 𝑅 → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
24	23	orcomd	⊢ ( EqvRel 𝑅 → ( [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) )