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:

 - <cite authors="Hamkins, Joel David; Kikuchi, Makoto">_Hamkins, Joel David; Kikuchi, Makoto_, [**Set-theoretic mereology**](https://doi.org/10.12775/LLP.2016.007), Log. Log. Philos. 25, No. 3, 285-308 (2016). [ZBL1369.03047](https://zbmath.org/?q=an:1369.03047). arxiv:[1601.06593](https://arxiv.org/abs/1601.06593).</cite>

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.