Many people find it natural to consider the set-theoretic analogue of mereology to be the inclusion relation $\subseteq$ rather than $\in$, since after all, $\subseteq$ is reflexive and transitive and admits relative complements, and these are all axioms listed on the mereology page to which you link, but $\in$ does not have these features. (For this reason, I am a little unsure about what you are trying to do with your translation of the part-hood relation as $\in$, since this seems flawed in many ways.)
If one does proceed with $\subseteq$ as the basis of set-theoretic mereology, then there is a bit of literature.
David Lewis, for example, in his 1991 book Parts of Classes outlines an approach to mereology by which the parthood relation is understood as $\subseteq$ in a system of class theory similar to Gödel-Bernays, and Lewis's system satisfies many of the axioms on the list itemized in the article to which you link.
More recently, I've written a few articles:
Hamkins, Joel David; Kikuchi, Makoto, Set-theoretic mereology, Logid and Logical Philosophy 25, No. 3, 285-308 (2016). Doi:10.12775/LLP.2016.007, ZBL1369.03047.
Hamkins, Joel David; Kikuchi, Makoto, The inclusion relations of the countable models of set theory are all isomorphic, arxiv:1704.04480, 2017.
Kikuchi and I undertake to analyze the nature and strength of what we call set-theoretic mereology, which is the study of the subst $\subseteq$ relation as it arises in ZFC set theory. Given a model of set theory $\langle V,\in\rangle\models\text{ZFC}$, we consider the definable reduct of this structure to the subset relation $\langle V,\subseteq\rangle$. Among other things, we prove that $\in$ is not definable from $\subseteq$ and that the theory of $\langle V,\subseteq\rangle$ is decidable — it is the theory of an unbounded atomic relatively complemented distributive lattice, and this is a finitely axiomatizable complete theory. Furthermore, we prove that all countable models of ZFC have isomorphic reducts to the subset relation. This is a sense in which set-theoretic mereology doesn't know any set theory, since it can't tell whether CH holds or fails, whether there are large cardinals or not, or ultimately, we prove, even whether there are infinite sets or not.
One philosophical point we make is that these results can be understood as an explanation of why there has been no successful implementation of set-theoretic mereology as a foundation of mathematics. Namely, one cannot use a decidable theory as a foundation of mathematics, since such a theory is not capable of serving as a foundation for the undecidable parts of mathematics, including arithmetic.
You can see more discussion of this at:
- The MathOverflow question, Why hasn't mereology succeeded as a foundation of mathematics?
- Various posts in the mereology tag on my blog, which includes the articles above as well as various other expository posts I've made and the mereology talks I've given.
Meanwhile, let me mention that if you augment $\subseteq$ with the singleton operator $a\mapsto\{a\}$, then you can easily recover the $\in$ relation via $x\in y\leftrightarrow \{x\}\subseteq y$, and so mereology-with-singleton-operator is bi-interpretable with $\in$-based set theory.