In a posting to MathStackExchange, I've presented a theory of rudimentary relations having a rudimentary kind of membership together with a primitive ordered pairing with the aim for it to capture the notions of sets and set membership.

I would say here that this theory itself can be captured in a mono-sorted way, especially in Mereology. Simply to Atomic General Extensional Mereology (without bottom), add a primitive partial function symbol $(,)$ standing for ordered pairing, then add axioms about it as:

Restriction: $ p=(a,b) \implies p,a,b \text{ are atoms }$

Pairs: $ \forall \text { atoms } a,b \, \exists p: p=(a,b) $

Pairing:$ (a,b)=(c,d) \implies (a=c \land b=d)$

Also add an axiom about existence of an atom that is not an ordered pair.

This is just a straightforward capture of relations in terms of Mereology, so the whole thought is about establishing a theory about relations. That's why I call it Relational Mereology. However, this turns to capture ample aspects about set membership?!

Now we define $\in$ as:

$A \in B \iff \exists b: A=[ a \mid (a,b) \operatorname {P} B]$

Where "$[x\mid \phi]$" stands for Mereological fusion of atoms satisfying $\phi$; $\mathbb P$ is atomic part-hood, that is:

$x \ \mathbb P \ y \iff atom(x) \land x \operatorname {P} y \\ y=[x \mid \phi] \iff \forall x \, (x \ \mathbb P \ y \iff \phi) $

This would prove existence of an empty set, pairing, Set unions, Infinity, Separation, and Replacement. Which I think is enough to get to interpret second order arithmetic.

The problem is that it cannot interpret Extensionality, nor prove Power.

To interpret Extensionality we need the axiom of equivalence classes under co-extensionality, that is for any set there is a set of all sets co-extensional with it.

Actually we only need to add ONE axiom to get to interpret full $\sf ZFC$! That is the axiom of Powerset, written here completely as written in $\sf Z$. In nutshell:

$\sf Relational\ Mereology + Powerset \equiv ZFC$

The idea for that equi-interpetability is for it to be established in the cumulative hierarchies of this theory.

Interpreting $\sf ZFC$ can be even done in weaker ways, like adding equivalence classes under co-extensionality, and also adding an axiom of larger cardinals, that is for any set there is a strictly larger set in cardinality.

Has this particular idea of grounding Set Theory in Relational Mereology been done before? Reference?