I'm trying to prove that the class of all hereditary countable sets, $HC=\{x: |tc(x)|\leq\omega_0\}$ is a subset of $V_{\omega_1}$. Here $tc(x)$ denotes the transitive closure. I've already proven that $HC$ is a transitive class; Now I tried using $\in$-induction:
Let $X=\{x: x\in HC\rightarrow rank(x)<\omega_1\}$ and suppose that $x\subset X$. Our goal is to prove that $x\in X$. Suppose that $x\in HC$. Then, if $y\in x$, since $HC$ is transitive, we have that $y\in HC$; but $y\in X$ too, therefore $rank(y)<\omega_1$. Now since $\omega_1$ is a limit ordinal, it will be $rank(y)+1<\omega_1$. Now $y$ was arbitrary, so $\sup\{rank(y)+1: y\in x\}\leq\omega_1$. But this is exactly $rank(x)$, therefore $rank(x)\leq\omega_1$.
Now I can't rule out the case where $rank(x)=\omega_1$. Any hints?
Here is a very nice observation:
The following are equivalent for any set $x$:
Using this claim, if $x\notin V_{\omega+1}$, then its transitive closure has an obvious map onto $\omega_1$, and is therefore not countable, so $x\notin\rm HC$.
The proof of the claim is by $\in$-induction on $x$:
Note that $\operatorname{tcl}(x)=x\cup\bigcup\{\operatorname{tcl}(y)\mid y\in x\}$. If $\beta<\alpha$, where $\alpha$ is the rank of $x$, then for some $y\in x$, the rank of $y\geq\beta$. Apply the induction hypothesis to $y$, and obtain that $\operatorname{tcl}(x)\cap V_{\beta+1}\setminus V_\beta$ is not empty.
In the other direction, note that if the rank of $x$ is some $\alpha'>\alpha$, then there is some $y\in x$ whose rank is at least $\alpha$, so in $\operatorname{tcl}(x)$ there is some $y'$ whose rank is $\alpha$, and therefore $\operatorname{tcl}(x)\cap V_{\alpha+1}\setminus V_\alpha\neq\varnothing$.