I am trying to understand the proof that $\Diamond$ holds in the constructible universe. I am following Kunen's Set Theory, where the proof is on pages 230-231 (the more recent, 2011 edition).
I am able to follow the arguments in the proof, up to the second to last paragraph, which starts with:
Applying $M \preccurlyeq H(\omega_2)$ and absoluteness: For each ordinal $\alpha \in M$, $A_\alpha, C_\alpha \in M$ and mos$(A_\alpha) = A_{\text{mos}(\alpha)}$ and mos$(C_\alpha) = C_{\text{mos}(\alpha)}$.
I don't understand why the above statement holds true. Any help clarifying this would be appreciated.
Edit: For context, the proof is trying to show that $\langle A_\alpha : \alpha < \omega_1 \rangle$ is a $\Diamond$-sequence. Towards a contradiction, we assume it is not a $\Diamond$-sequence.
The definition of the sequence goes as follows. For limit ordinals $\alpha$, define $$P(\alpha, A, C) \iff A, C \subseteq \alpha \land C \text{ is club in } \alpha \land \neg \exists \xi \in C (A \cap \xi = A_\xi).$$ Then let $(A_\alpha, C_\alpha)$ be the $<_L$ first pair such that $P(\alpha, A, C)$. If there is no such pair, or if $\alpha$ is not a limit, let $A_\alpha = C_\alpha = \emptyset$.
Also, mos refers to the Mostowski isomorphism from a countable $M \preccurlyeq H(\omega_2)=L(\omega_2)$ to some transitive $T$.
For $\alpha\in M\implies A_\alpha,C_\alpha\in M$, the key observation is that the sequence $\mathfrak{S}=(A_\alpha,C_\alpha)_{\alpha<\omega_1}$ is an element of $M$. This is just because it is definable without parameters in $H_{\omega_2}$ (check this).
Now of course this doesn't mean $\mathfrak{S}\subseteq M$ - and indeed, if $M$ is "small" (e.g. countable) it won't be - but it does mean that $M$ sees as much of $\mathfrak{S}$ as it should: $$\alpha\in Ord\cap M\implies (A_\alpha,C_\alpha)\in M.$$ We're not using anything special about $\mathfrak{S}$, just that if a sequence and an index are in $M$ then so is the term of the sequence with that index.
For the Mostowski collapse calculations, think about what happens to the $L$-ordering and to $P$-ness when we take the Mostowski collapse. The point is that we know that $mos(A_\alpha)\subseteq mos(\alpha)$, so we just need to check that $mos(A_\alpha)$ satisfies $P$ and is the $L$-least subset of $\alpha$ to satisfy $P$; and the ideal situation would be that everything "stays the same" when we take the Mostowski collapse.