I am using the book Set theory by Kunen (2013 edition, numeration is completely different than the previous ones) and I'm trying to show the following (theorem II.4.27):
Let $M$ be a transitive class verifying:
Comprehension axiom holds.
$\forall x\subset M$ there exists $y\in M$ such that $x\subset y$.
Then all ZF axioms hold in M.
I managed to show all axioms (using II.2.4 and II.2.8) except for the axiom on infinity, that is $\omega \in M$, the book says that I should use lemma II.4.10 which is
$M$ transitive class in BST, then
$[M]^{<\omega}\subset M$
HF$\subset M$
I'm probably missing something obvious but I really can't see how you do it, it's probably easier to show $\omega\subset M$ (which is enough by (2)) but I haven't managed to do that either.se
You know that $HF\subset M$, so by (2) you know that there is some $y\in M$ with $HF\subseteq y$. Now, you just want to build $\omega$ from $y$.
The obvious problem is that $y$ is "too big" - it contains $HF$ (which is much bigger than $\omega$), and it might contain a lot more than $HF$ (we just know $HF\subseteq y$ not $HF=y$). So we need to "trim" it.
This is where Separation comes into play. There are lots of ways to define the finite ordinals - for example, let $\varphi(x)$ be the formula "$x$ is an ordinal and every ordinal in $x$ is either a successor ordinal or $0$." So apply Separation to $y$ using any such formula; this will give you exactly $\omega$.
Well, that last bit takes proof: you need to argue that the things $M$ thinks are finite ordinals are exactly the finite ordinals. But this isn't hard - you have $HF\subset M$, so clearly the things $M$ thinks are finite ordinals consist of at least the actual finite ordinals, and conversely you can use the transitivity of $M$ to show that $M$ doesn't think anything is a finite ordinal that isn't actually a finite ordinal.