In a set-theoretic context, my view is that the most compelling concept of mereology is simply the $\subseteq$ relation, and so my conception of set-theoretic mereology is simply the theory of the $\subseteq$ relation.

So this doesn't answer your question, and I won't get into your theory and the theory is different, but some readers may be interested in this alternative approach to set-theoretic mereology, which I introduced in my paper with Makoto Kikuchi:

• Hamkins, Joel David; Kikuchi, Makoto, Set-theoretic mereology, Log. Log. Philos. 25, No. 3, 285-308 (2016). ZBL1369.03047. arxiv:1601.06593.

Namely, we study the relation $\subseteq$ in a model of set theory, and we regard this theory as "set-theoretic mereology."

It is very easy to see in ZFC set theory that $\in$ is bi-interpretable with $\subseteq$ and the singleton operator, as we note in the paper, because of the following equivalences: $$u\subseteq v\quad\iff\quad\forall x\, (x\in u\to x\in v)$$ $$y=\{x\}\quad\iff\quad \forall z\, (z\in y\iff z=x).$$ Conversely, we may define $\in$ from $\subseteq$ and singletons via $$x\in y\quad\iff\quad \{x\}\subseteq y.$$ The conclusion, in short, is that yes, indeed, set-theoretic mereology with the singleton operator is bi-interpretable with $\in$-based set theory. You can define $\in$ from $\subseteq$ and $x\mapsto\{x\}$ and conversely.

But in regard to your specific axiomatization, I wouldn't have anything more to say.

In a set-theoretic context, my view is that the most compelling concept of mereology is simply the $\subseteq$ relation, and so my conception of set-theoretic mereology is simply the theory of the $\subseteq$ relation.

So this doesn't answer your question, and I won't get into your theory, which is different from how I understand things, but some readers may be interested in this alternative approach to set-theoretic mereology, and so let me mention this alternative approach, which I introduced in my paper with Makoto Kikuchi:

• Hamkins, Joel David; Kikuchi, Makoto, Set-theoretic mereology, Log. Log. Philos. 25, No. 3, 285-308 (2016). ZBL1369.03047. arxiv:1601.06593.

Namely, we study the relation $\subseteq$ in a model of set theory, and we regard this theory as "set-theoretic mereology."

It is very easy to see in ZFC set theory that $\in$ is bi-interpretable with $\subseteq$ and the singleton operator, as we note in the paper, because of the following equivalences: $$u\subseteq v\quad\iff\quad\forall x\, (x\in u\to x\in v)$$ $$y=\{x\}\quad\iff\quad \forall z\, (z\in y\iff z=x).$$ These show that from the $\in$ relation one can define both $\subseteq$ and the singleton operator. Conversely, we may define $\in$ from $\subseteq$ and singletons via $$x\in y\quad\iff\quad \{x\}\subseteq y.$$ The conclusion is that the two accounts of set theory are bi-interpretable. Set-theoretic mereology with the singleton operator is bi-interpretable with $\in$-based set theory. You can define $\in$ from $\subseteq$ and $x\mapsto\{x\}$ and conversely.

But in regard to your specific axiomatization, I wouldn't have anything more to say.