ZF axioms on a transitive class 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
 A: 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.
A: You can prove by induction: If $\alpha$ is an ordinal and $\alpha\subseteq M$, then $\alpha\in M$. Therefore every ordinal is in $M$, in particular $\omega$ itself. 
To see why, let $y\in M$ such that $\alpha\subseteq y$ and use Comprehension to separate the ordinals which are in $y$, namely define $x\in M$ to be $\{u\in y\mid u\text{ is an ordinal}\}$ using Comprehension (here it is important that $M$ is transitive and agrees with the universe on being an ordinal). Either there is some $\gamma\in x$ such that $\alpha<\gamma$ and by the transitive property of $M$ now $\alpha\in M$, or simply $x=\alpha$ and we are done. 
