Proof that we can't get $\omega + \omega$ without Replacement It is well known that Replacement gives us that $\omega + \omega$ is a set (provable by a simple recursion). It is vaguely intuitive that this could not be done without -- whilst we can 'see' $\{\omega, \omega + 1, \omega + 2, \ldots \}$, there is no guarantee that this is a set (Burali-Forti might make us wary).
I was wondering where I might find a proof of this fact -- i.e. that in $\textsf{ZF}$ without replacement, we are unable to prove that $\omega + \omega$ is a set.
I've seen some basic techniques for stuff like this -- by considering 'hereditarily finite' sets (sets $X$ which are finite, and which have $x$ finite for all $x \in X$) we can show that from Empty Set, Extensionality, Pairs, Unions, and Comprehension we can't get Infinity; by changing 'finite' to 'countable' we can show that we can't get Powerset. (The proofs proceed by considering the classes of all hereditarily finite/countable sets, and showing the first collection of axioms is met, whilst the last is not -- so there is no $\omega$ or $\mathcal{P}X$, resp., in them.) Is the proof for this proof similar or do the techniques get more advanced?
Thanks for any help
 A: The proof of this result is exactly the same: we find an ordinal $\alpha$ such that $V_\alpha\models\mathsf{ZC}$ (= $\mathsf{ZFC}$ without replacement; although you didn't ask for it, I'm including choice because it gives a stronger result but doesn't cost us anything) but $\omega+\omega\not\in V_\alpha$.
Note that this latter condition is equivalent to $\omega+\omega\ge\alpha$; does this suggest a choice of $\alpha$ to look at? (Think about how Powerset and Infinity restrict our options here.)
EDIT: OK fine, "exactly" might be unfair here. You mentioned constructions using hereditary cardinality, namely $H_\omega$ (= hereditarily finite sets) and $H_{\omega_1}$ (= hereditarily countable sets); here we want to use the $V$-hierarchy instead of the $H$-hierarchy. However, modulo this difference the arguments are the same: determine which levels of the relevant hierarchy satisfy which axioms of the theory in question, and then amongst those levels pick one which avoids the ordinal in question.
