# Is the class of image mappings first-order axiomatizable?

Let $$S$$ be a set, and let $$R$$ be a binary relation on $$S$$. $$R$$ induces a mapping $$f:\mathcal{P}(S) \rightarrow \mathcal{P}(S)$$ such that for any subset $$T$$ of $$S$$, $$f(T)$$ is the image of $$T$$ under the relation $$R$$. Now, consider the class of structures of the form $$(\mathcal{P}(S);f,0,1,\cup,\cap,\setminus,\subseteq)$$, where $$0$$ is the empty set, $$1$$ is the set $$S$$, $$\setminus$$ is set difference, and the other symbols are well-known. We can write down some statements that image mappings satisfy, like $$f(0)=0$$ and $$f(x \cup y) = f(x) \cup f(y)$$. My question is this. In the first-order language $$\{f,0,1,\cup,\cap,\setminus,\subseteq\}$$, is there a set of axioms that characterize whenever $$f$$ is an image mapping induced by a relation $$R$$. More precisely, if we restrict our attention on the class of structures of the form $$(\mathcal{P}(S);f,0,1,\cup,\cap,\setminus,\subseteq)$$, and we interpret $$0$$ as the empty set, $$1$$ as the set $$S$$, $$\cup$$ as union, $$\cap$$ as intersection, $$\setminus$$ as set difference, and $$\subseteq$$ as the subset relation, is there a set of first-order axioms that hold true precisely when $$f$$ is an induced image mapping? And if there is, is there a finite such set of axioms?

First note that the set of atoms in the power set algebra is definable. Now consider the following sentence $$\varphi$$: for all $$X$$ and all atoms $$y$$, $$y$$ is below $$f(X)$$ if and only if there is some atom $$x$$ below $$X$$ such that $$y$$ is below $$f(x)$$.
Suppose $$R$$ is a binary relation on $$S$$, and $$f\colon \mathcal{P}(S)\to \mathcal{P}(S)$$ is the image mapping. Note that $$xRy$$ if and only if $$\{y\}\subseteq f(\{x\})$$. And for any $$X\subseteq S$$, $$y\in f(X)$$ if and only if there is $$x\in X$$ such that $$xRy$$. Putting these observations together, for an atom $$\{y\}$$, we have $$\{y\}\subseteq f(X)$$ if and only if there exists an atom $$\{x\}\subseteq X$$ such that $$\{y\}\subseteq f(\{x\})$$. This shows that every image mapping satisfies $$\varphi$$.
Conversely, I claim that for every structure $$(\mathcal{P}(S);f,0,1,\cup,\cap,\setminus,\subseteq)$$ which satisfies $$\varphi$$, $$f$$ is the image mapping for some binary relation $$R$$ on $$S$$. Define the relation $$R$$ by $$xRy$$ if and only if $$\{y\}\subseteq f(\{x\})$$, and let $$f'$$ be the image mapping for this $$R$$. It remains to show that $$f' = f$$. So pick $$X\subseteq S$$ and show that $$f(X) = f'(X)$$. For any $$y\in S$$, we have $$y\in f(X)$$ iff $$\{y\}\subseteq f(X)$$ iff (by $$\varphi$$) there is some $$\{x\}\subseteq X$$ such that $$\{y\}\subseteq f(\{x\})$$ iff (by definition of $$R$$) there is some $$x\in X$$ such that $$xRy$$ iff $$y\in f'(X)$$.