This question is about synonymy between Set theory and Mereology.

David Lewis in Mathematics is Megethology tried to reduce Set Theory to Mereology augmented with a singleton function. The following exposition is a formal capture of his Mereology.

Lets define a mereological theory $\sf M$ in mono-sorted first order logic with identity, add primitives of part-hood "$P$", and the partial unary function "$\mathfrak L $", denoting "is the lable of". Add the following axioms:

Mereological Axioms:

M1 $\textbf{Anti-symmetry: }X \ P \ Y \land Y \ P \ X \to X=Y$

M2 $\textbf{Bottom: }\exists X \forall Y: X \ P \ Y$

Define: $X = \varnothing \iff \forall Y: X \ P \ Y$

Define: $ X \ PP \ Y \iff X \ P \ Y \land \neg (Y \ P \ X)$

Define: $atom(X) \iff \forall Y: Y \ PP \ X \to Y=\varnothing$

Define: $ X\ P^*\ Y \iff atom(X) \land X \ P \ Y$

M3 $\textbf{Atomism: } \forall X (X \ P^* \ Y \to X \ P^* Z) \leftrightarrow Y \ P \ Z$

M4 $\textbf{Composition: }\\ \exists X \forall Y \ (Y \ P^* \ X \leftrightarrow Y=\varnothing \lor [atom(Y) \land \psi] ); \text{ if } X \text { is not free in } \psi $

Define: $X = \bigl[Y \mid \psi \bigr] \iff \forall Y \ (Y \ P^* \ X \leftrightarrow Y=\varnothing \lor [atom(Y) \land \psi] )$

Labeling Axioms

L1 $\textbf{Labeling: } \mathfrak L (X)=\mathfrak L (Y) \to X=Y$

L2 $\textbf{Purity: } \exists X \ (\mathfrak L(X)=Y) \leftrightarrow atom(Y) \land Y \neq \varnothing$

L3 $\textbf{Replacement: } \text { if } \psi(X,Y) \text { is a formula, then: } \\ \forall X \neg \exists^{>1} Y: \psi(X,Y), \land \\ B= \bigl[K \ P^* \ Y \mid \exists V (V=\mathfrak L(Y) \lor Y=\mathfrak L(V)) \land \exists X \ P \ A \ :\psi(X,Y)\bigr] \land \\\exists Z: \mathfrak L(A)=Z \\\to\\\exists Z: \mathfrak L(B)=Z $

L4 $\textbf{Infinity: } \exists I \exists X: \forall Y \ P^* \ X \bigl(\exists Z \ P \ X: \mathfrak L(Y)=Z \bigr) \land \mathfrak L (X)=I $

/

In David Lewis account he didn't round the system with a bottom object, so a modified version of his system would be captured by $\sf M$-$\sf Bottom$ which is obtained here by removing $\sf Bottom$ axiom, re-defining atoms as objects devoid of proper parts, and stipulating the existence of a unique non-labeling atom $\varnothing$.

Is theory $\sf M$ synonymous with "$\sf MK$ sans Foundation sans Choice"?

Is $\sf M$-$\sf Bottom$ bi-interpretable with "$\sf MK$ sans Foundation sans Choice"?

My plan is to keep equality, and to identify part-hood $P$ with subset-hood relation $\subseteq$, and the labeling function $\mathfrak L$ with the singleton function $X \mapsto \{X\}$; and on the other hand to define $\in$ as: $X \in Y \iff \exists K \ P \ Y: \mathfrak L (X)=K$.

This way we come to identify classes with mereological totalities, and sets with labeled mereological totalities. All of this is following Lewis's own specifications. However, seeing that Lewis in his "Mathematics is Megethology" doesn't agree to Bottom axiom, it appears to me that without this axiom the whole Ontology would be plagued with Ur-elements, and so it appears to be so hostile to Extensionality, that I think synonymy with Set Theory cannot be achieved. However, the weaker requirement of bi-interpretability might be possible?