Theorem mainer

Description: The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	mainer	⊢ ( 𝑅 ErALTV 𝐴 → CoMembEr 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqvrelqseqdisj2	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ElDisj 𝐴 )
2		eldisjim	⊢ ( ElDisj 𝐴 → CoElEqvRel 𝐴 )
3	1 2	syl	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → CoElEqvRel 𝐴 )
4		n0eldmqseq	⊢ ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ¬ ∅ ∈ 𝐴 )
5	4	adantl	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ¬ ∅ ∈ 𝐴 )
6		eldisjn0el	⊢ ( ElDisj 𝐴 → ( ¬ ∅ ∈ 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
7	1 6	syl	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ( ¬ ∅ ∈ 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
8	5 7	mpbid	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 )
9	3 8	jca	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
10		dferALTV2	⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) )
11		dfcomember3	⊢ ( CoMembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
12	9 10 11	3imtr4i	⊢ ( 𝑅 ErALTV 𝐴 → CoMembEr 𝐴 )