In the Princeton Companion to Mathematics chapter on set theory, Joan Bagaria challenges the reader to show that $\langle \mathbb{N}, \text{E}\rangle$ is a model of ZFC without the axiom of infinity, where $m\text{E}n$ if and only if the $m$th digit of the binary expansion of $n$ (counting from the right) is $1$. I've attempted to show that the power set axiom remains true in this model, and would appreciate any verification or correction.
The power set axiom states that $\forall x \exists y \forall z \left[z\in y \iff \forall w \left(w\in z \implies w\in x\right)\right]$. Replacing $\in$ with $\text{E}$, and interpreting the variables as natural numbers, I want to prove that $\forall x \exists y \forall z \left[z\text{E} y \iff \forall w \left(w\text{E} z \implies w\text{E} x\right)\right]$. My proof goes as follows:
Let $x$ be a given natural number, and write the binary expansion of $x$ as $(a_k)_{k\geq 0}$, $a_j = 0$ or $1$. That is, $x = \sum_{k = 0}^na_k2^k$, where $a_n = 1$ and $n+1$ is the length of the binary expansion of $x$. Let $y$ be the natural number such that the $m$th digit in its binary expansion (counting from the right, starting at $1$) is equal to $1$ if and only if $m = \sum_{A\subseteq \{0,1,...,n\}} a_k2^k$ for some subset $A$ of $\{0,1,...,n\}$. It remains to show that $\forall z \left[z\text{E} y \iff \forall w \left(w\text{E} z \implies w\text{E} x\right)\right]$.
Let $z$ be a natural number.
If $z\text{E}y$, then the $z$th digit of $y$ is $1$, which means that, by definition of $y$, $z = \sum_{A\subseteq \{0,1,...,n\}} a_k2^k$ for some $A$. Then if the $w$th digit of $z$ is $1$, the $w$th digit of $x$ must be $1$. This proves the forward implication.
If $\forall w \left(w\text{E} z \implies w\text{E} x\right)$, then the binary expansion of $z$ looks like the binary expansion of $x$, but with some (or none) $0$s replaced by $1$s. Thus $z = \sum_{A\subseteq \{0,1,...,n\}} a_k2^k$ for some $A$, and by definition of $y$, $z\text{E}y$. This proves the backwards implication.
Thus the $y$ defined above satisfies the power set axiom, as we wanted to show.
Is my proof correct? Is there an easier way to show that the power set axiom holds in $\langle\mathbb{N}, \text{E}\rangle$, or in general, an easier way to show that something is a model of a fragment of ZFC?