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	$$⊢RErALTVA\to CoMembErA$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelqseqdisj2	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to ElDisjA$$
2		eldisjim	$$⊢ElDisjA\to CoElEqvRelA$$
3	1 2	syl	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to CoElEqvRelA$$
4		n0eldmqseq	$$⊢\mathrm{dom}R/R=A\to \neg \varnothing \in A$$
5	4	adantl	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \neg \varnothing \in A$$
6		eldisjn0el	$$⊢ElDisjA\to \left(\neg \varnothing \in A\leftrightarrow \bigcup A/\sim A=A\right)$$
7	1 6	syl	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \left(\neg \varnothing \in A\leftrightarrow \bigcup A/\sim A=A\right)$$
8	5 7	mpbid	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \bigcup A/\sim A=A$$
9	3 8	jca	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$
10		dferALTV2	$$⊢RErALTVA\leftrightarrow \left(EqvRelR\wedge \mathrm{dom}R/R=A\right)$$
11		dfcomember3	$$⊢CoMembErA\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$
12	9 10 11	3imtr4i	$$⊢RErALTVA\to CoMembErA$$