Troubles with a proof from Kunen's book I'm studying Godel's constructible universe and those statements that are true inside it: specifically $L\vDash\lozenge$. In this regard, I need to understand the following Lemma from Kunnen's book Set Theory (2011).

$\bf Lemma\ III.7.12\ $ Let $\theta$ be an uncountable cardinal, and let $M$ be countable with $M\preccurlyeq H(\theta)$. Then
  
  
*
  
*If $a\in M$ and $a$ is countable, then $a\subseteq M$.
  
*$M\cap\omega_1$ is a countable limit ordinal. 
  
*If $\theta=\omega_1$, then $M$ is transitive.
  
*If $\theta\gt\omega_1$: $\omega_1\in M$ and $\omega_1\not\subseteq M$; if $\beta=M\cap\omega_1$ and $\operatorname{mos}$ is the Mostowski isomorphism from $M$ onto a transitive $T$, then $\operatorname{mos}(\omega_1)=\beta$ and $\operatorname{mos}(\xi)=\xi$ for all $\xi\lt\beta$. Also $T\vDash ZFC-P$ (if $\theta$ is regular), and $\beta=(\omega_1)^T$.
  

I'm having troubles with the proof of the first statement. More concretely I don't understand who the condition $M\preccurlyeq H(\theta)$ allows the author to state the following:

$\bf Proof.$ For $(1)$, note that $\omega$ and all smaller ordinals are definable in $H(\theta)$, so $\omega\in M$ and $\omega\subseteq M$. Assume that $a\neq\emptyset$ (otherwise the result is trivial); so there is a function $f:\omega\overset{\text{onto}}\longrightarrow a$. All such $f$ are in $H(\theta)$, so $M\preccurlyeq  H(\theta)$ implies that some such $f$ is in $M$. Now every element of $a$ is of the form $f(n)$ for some $n$, and $f$, $n\in M\to f(n)\in M$ (by $M\preccurlyeq H(\theta)$), so $a\subseteq M$.

So for example:


*

*It is clear that $\omega$ and the natural numbers are defined in $H(\theta)$, but why are they defined in $M$?

*Why is there a function $f$ that lies in $M$ as a consequence of $M\preccurlyeq H(\theta)$?

*Why $f(n)\in M$ as a consequence of $M\preccurlyeq H(\theta)$?


Every help or comment would be much apreciated. Thanks in advance.
 A: Note that each of the natural numbers (and indeed, the set of all of them) are definable without parameters. So $M$ can run this definition as well, and get 'its version' of $\omega$. But then elementarity tells you that this version must be the real $\omega$, and M's natural numbers the real natural numbers.
If $a \in M$ and is countable, then the statement "$a$ is countable" is true. But this is a statement that only involves the parameter $a$, which is in $M$. So $M$ can make it as well, and again, elementarity tells us that it must be correct about this. But this means $M$ thinks that there is some function $f$ from $\omega$ onto $a$ which is in $M$. But then again, by elementarity, $M$ must be correct about these properties of this function.
Finally, $M$ thinks that $f$ is a function whose domain is $\omega$, and $n \in M$ as we have seen above. So then $M$ sees that $f(n)$ is defined, and again, $M$ must be correct about the statement "$f(n)$ is defined". So then if $M$ thinks that $f(n) = b$, by a final application of correctness, $M$ must be correct about this.
Hope this helps.
A: Well, $\omega$ is definable - by a formula $\varphi$ - in $H(\theta)$. So $H(\theta)\models \exists! x\varphi(x)$. (Here "$\exists!$" is shorthand for "there exists a unique".) By elementarity, this means $M\models\exists! x\varphi(x)$. Let $m\in M$ be such that $M\models\varphi(m)$. Then by elementarity, $H(\theta)\models\varphi(m)$. So $m=\omega$.
Similarly, every finite ordinal is definable in $M$ in the same way it is definable in $H(\theta)$ - and hence in $M$.
Moving on: suppose $a\in M$ is countable. Then by elementarity, $M$ thinks that $a$ is countable. This means that $M$ thinks there is a bijection $f$ from $a$ to $\omega$. By elementarity, $H(\theta)$ also thinks $f$ is a bijection from $a$ to $\omega$ - that is, $f$ really is a bijection from $a$ to $\omega$.
Now suppose $b\in a$. Then - in $H(\theta)$ - we have some $n\in\omega$ such that $f(b)=n$. So by elementarity, $M\models\exists x(f(x)=n)$. (Note that this uses that $n\in M$.) Let $c\in M$ be such that $M\models f(c)=n$. Then by elementarity, $H(\theta)\models f(c)=n$, that is, $f(c)$ really equals $n$. But then $c=b$, so $b\in M$.
