[proofplan] The external countability assertion is exactly the hypothesis that $M$ is a countable subset of the ambient universe. For the internal assertion, we express “$\omega_1$ is uncountable” as the first-order statement that no function from $\omega$ onto $\omega_1$ exists. This statement is true in $(H_\theta,\in)$, and since $\omega_1 \in M$ and $M \preccurlyeq (H_\theta,\in)$, elementarity transfers it to $M$. [/proofplan] [step:Record the external countability of $M$] By hypothesis, $M$ is countable in the ambient universe. Thus there exists, externally, a surjective map \begin{align*} e:\omega \to M. \end{align*} This proves the external countability part of the theorem. [/step] [step:Express uncountability of $\omega_1$ by a first-order formula] Let $\varphi(a)$ be the first-order formula in the language of set theory saying: \begin{align*} \text{there is no function } f \text{ such that } f:\omega \to a \text{ is surjective}. \end{align*} More explicitly, $\varphi(a)$ asserts that there is no set $f$ such that $f$ is a function with domain $\omega$, range contained in $a$, and \begin{align*} \forall y \in a \, \exists n \in \omega \, ((n,y) \in f). \end{align*} In the ambient universe, $\omega_1$ is the first uncountable ordinal, so there is no surjection from $\omega$ onto $\omega_1$. Therefore \begin{align*} (H_\theta,\in) \models \varphi(\omega_1). \end{align*} [/step] [step:Transfer the statement to $M$ by elementarity] Since $M \preccurlyeq (H_\theta,\in)$ and $\omega_1 \in M$, elementarity applies to the formula $\varphi(a)$ with parameter $a=\omega_1$. Hence \begin{align*} (M,\in) \models \varphi(\omega_1). \end{align*} Unwinding the definition of $\varphi$, this says that $M$ contains no object that it regards as a surjective function from $\omega$ onto $\omega_1$. Thus $M$ is countable externally, while internally it satisfies that $\omega_1$ is uncountable. [/step]