Theorem mpets

Description: Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet , the Partition-Equivalence Theorem, with general R . (Contributed by Peter Mazsa, 31-Dec-2024)

	Ref	Expression
Assertion	mpets	$$⊢\mathrm{MembParts}=\mathrm{CoMembErs}$$

Proof

Step	Hyp	Ref	Expression
1		mpets2	$$⊢a\in \mathrm{V}\to \left(\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a\leftrightarrow \wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a\right)$$
2	1	elv	$$⊢\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a\leftrightarrow \wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a$$
3	2	abbii	$$⊢\left\{a|\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a\right\}=\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a\right\}$$
4		df-membparts	$$⊢\mathrm{MembParts}=\left\{a|\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a\right\}$$
5		df-comembers	$$⊢\mathrm{CoMembErs}=\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a\right\}$$
6	3 4 5	3eqtr4i	$$⊢\mathrm{MembParts}=\mathrm{CoMembErs}$$