I'm trying to show that if $\mathbb{P}$ is the set of partial functions $\omega_1\to\omega_1$ with countable domain, and $M$ is a ctm of $ZFC$, then $M[G]\models\diamondsuit$.
I came across this question, asked previously on this site. Now, when constructing the $\beta_n$ and $q_n$, we're stepping out of the ground model $M$, so I don't see why $\langle\beta_n:n<\omega\rangle$ should be bounded in $\omega_1^M$. I know this forcing does not add new bounded sequences of length $\le\omega_1$, but it's not clear to me that the sequence $\langle\beta_n:n<\omega\rangle$ even belongs to $M[G]$.
I have similar doubts regarding using closedness (?) of the forcing to get an extension of all the $q_n$ (since we want $\langle q_n:n<\omega\rangle\in M$), but I'm guessing both things will follow by a similar reasoning.