$V_\omega$ is countable Is there an easy way to prove this? I found a book that suggests the injection $h:V_\omega\to\omega$ defined by
$$h(\{x_1,x_2,\dots,x_n\})=2^{h(x_1)}+2^{h(x_2)}+\cdots+2^{h(x_n)},$$
but I hit some snags while proving that the function is well-defined. Are there any other clever ways to prove this fact? (Note: I am making a formal proof, so I need to be able to justify my steps.)
Edit: Let me see if I can make my difficulty more clear. Before I can start the proof by induction, I need a precise statement of the induction hypothesis, and this is what I am trying to hammer out. The hypothesis:

For each $n\in\omega$, there exists a unique bijection $h_n:V_n\to|V_n|$ such that $$h_n(x)=\sum_{m<|V_{n-1}|}\operatorname{if}(h_{n-1}^{-1}(m)\in x,2^m,0).$$
Moreover, the $h_n$ as defined satisfies $h_n\restriction |V_{n-1}|=h_{n-1}$.

Does this hypothesis contain enough to prove the claim? The reason for the odd way of stating the sum is that it avoids the issue in the linked question (we need to show that addition is a well-defined operation over sets), but as a consequence I have to prove that
the $h_n$ is a bijection and not just an injection, and I think I also need the restriction part in order to prove that the union $h=\bigcup_{n\in\omega}h_n$ is the required bijection.
 A: To prove that $h$ is well-defined and injective, it is most natural to proceed by induction on the rank of sets. The rank $\mathsf{rk}(x)$ of a set $x$ is an ordinal, defined recursively as follows (see also MathWorld for a definition for all sets):
$$\mathsf{rk}(x):= \sup\{\mathsf{rk}(y)+1: y \in x\}$$

Lemma: The rank of a set is well-defined.

This lemma can be proved using the Axiom of Foundation, see also this question. Since all suprema involved in computing $\mathsf{rk}$ for $x \in V_\omega$ are finite, the results are also finite ordinals.

The only set of rank zero is of course $\varnothing$; we define/obtain $h(\varnothing) = 0$.
Now given a set $X = \{x_1, \ldots, x_m\}$ of rank $n+1$, we use the Axiom of Replacement for $f(x) = 2^{h(x)}$, well-defined and injective by induction hypothesis.
We now have the set $Y = \{2^{h(x_1)},\ldots, 2^{h(x_m)}\}$; using your earlier question this gives rise to a well-defined number $h(X) = \sum Y$, so $h$ is well-defined on $X$ as well.
To show that $h$ is injective, let $X'$ be such that $\mathsf{rk}(X') \le \mathsf{rk}(X)$. Then we can obtain the sets $\{h(x_1),\ldots, h(x_m)\}$ and $\{h(x'_1),\ldots, h(x'_{m'})\}$ by the Basis Representation Theorem. The Axiom of Replacement can be applied to these sets since $h^{-1}$ is a functional relation, and we recover $X$ and $X'$; injectivity of both the Basis Representation and $h^{-1}$ ensures that $h(X) = h(X')$ implies $X = X'$. Thus $h$ is injective and well-defined on sets of rank at most $n+1$.
In conclusion, $h$ is well-defined on $V_\omega$; its injectivity on $V_\omega$ is trivially verified.
A: If you just need to prove that $V_\omega$ is countable, and if you're allowed to use the axiom of choice, then I think you're working too hard.  Prove, by induction on natural numbers $n$ that $V_n$ is finite (because the power set of a finite set is finite).  Then $V_\omega=\bigcup_{n\in\omega}V_n$ is the union of countably many finite sets, hence countable.
