Is it true that $V$ and $H_{\omega_1}$ agree on the truth value of $\Sigma_1$ sentences?

Question

I want to see if the following result is correct or not:

Let $\varphi(x)$ be a formula in $\mathcal{L}_{\mathrm{ZF}}$ with only bounded quantifiers such that $\exists x\,\varphi(x)$ holds in $V$, then $\exists x\,\varphi(x)$ holds in $H_{\omega_1}$.

I wrote a proof for it using the following reasoning:

$\varphi$ is absolute for all transitive models; let $\exists x\,\varphi(x)$ be true, then $\varphi(a)$ holds for some $a$. Let $\vartheta\in\mathbf{ON}$ such that $a\in V_\vartheta$. Let $M\prec V_\vartheta$ be a countable elementary substructure, $\bar M$ be the Mostowski collapse ($\bar M\cong M$), then $\bar M$ is transitive and countable, hence hereditarily countable, so $\bar M\subseteq H_{\omega_1}$, so there is a witness for $\varphi(x)$ in $H_{\omega_1}$.

My questions are: (1) is the result above correct? (2) Is the proof given correct? (3) If the result is correct and the proof is not correct, what would be a correct proof for the result?

Answer 1

The proof is correct, but I'd change the order of a few things and extend a bit to make it slightly clearer:

We assume that $\exists x\varphi(x)$ is true in $V$, so there is some $a$ such that $\varphi(a)$ holds. Let $\vartheta$ an ordinal such that $a\in V_\vartheta$, since $V_\vartheta$ is transitive and $\varphi$ is a bounded formula, $V_\vartheta\models\varphi(a)$ and therefore $V_\vartheta\models\exists x\varphi(x)$. Let $M$ be a countable elementary submodel of $V_\vartheta$ and let $\overline M$ be its Mostowski collapse, then $\overline M\in H_{\omega_1}$.

Finally, since $M$ is an elementary submodel of $V_\vartheta$, and $M\cong\overline M$ we have that $\overline M\models\exists x\varphi(x)$. So there is some $a'\in\overline M$ such that $\overline M\models\varphi(a')$, but again by absoluteness of bounded formulas between transitive sets, $H_{\omega_1}\models\varphi(a')$ so $H_{\omega_1}\models\exists x\varphi(x)$ as wanted.

Essentially the same proof can be extended to show that $H_\kappa\prec_{\Sigma_1}V$, as remarked by GME in the comments.