Theorem mpet3

Description: Member Partition-Equivalence Theorem. Together with mpet mpet2 , mostly in its conventional cpet and cpet2 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 with general R ). (Contributed by Peter Mazsa, 4-May-2018) (Revised by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	mpet3	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldisjn0elb	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\leftrightarrow \left(Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$
2		eqvrelqseqdisj3	$$⊢\left(EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)\to Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3	2	petlem	$$⊢\left(Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)\leftrightarrow \left(EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$
4		eqvreldmqs	$$⊢\left(EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$
5	1 3 4	3bitri	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$