I'm going through some problems about absoluteness for transitive models and got stuck on something:
Let $M$ be a transitive model of ZFC. Let $T$ be a tree on $\omega\times\omega$ with $T\in M$, and let $x\in M$ be such that $x\in \text{proj}([T])$, i.e. $$ \exists y\in \omega^\omega \forall n<\omega [(x|n,y|n)\in T]. $$ Does it necessarily follow that $(x\in \text{proj}([T]))^M$? Since the property of being a function $\omega\to\omega$ is absolute, $(\omega^\omega)^M=\omega^\omega\cap M$, so that $(x\in\text{proj}([T]))^M$ would mean that $$ \exists y\in\omega^\omega\cap M\forall n<\omega [(x|n,y|n)\in T] $$ by absoluteness of the various notions involved. So I'd need to construct an element of $M\cap\omega^\omega$ which satisfies the above formula, but I don't see how to do this.