I am self studying the proof of consistency of MA. At some point it seems that we need something like this:
Let $M$ be a countable transitive model for ZFC. Let $P_1$ and $P_2$ be forcing posets, with $P_1$ completely-embeddable into $P_2$. Suppose that $P_2$ is ccc. Let $G$ be $P_2$-generic over $M$. Suppose that $(X, {\leq}) \in M[G]$ and $(X, \leq) \in M[G \upharpoonright P_1]$. If $M[G] \models$ "$(X,\leq)$ is a ccc poset", then also $M[G \upharpoonright P_1] \models$ "$(X,\leq)$ is a ccc poset".
I already know that $G \upharpoonright P_1$ is $P_1$-generic over $M$ and $M[G \upharpoonright P_1] \subseteq M[G]$.
If $P_2$ were countably-closed, then this would be trivial, because it would preserve $\omega$-sequences. But this is not the case, so maybe we have an antichain $A \in M[G \upharpoonright P_1]$ which is of course countable in $M[G]$, but it might happen that the injection $f \colon A \to \omega$ is not in $M[G \upharpoonright P_1]$.
How can I handle this? Thank you.
Edit: Proof attempt.
Suppose to the contrary that $M[G \upharpoonright P_1] \models g \colon \omega_1 \to A$ is injective. Then $M[G] \models g \colon \omega_1^{M[G \upharpoonright P_1]} \to A$ is injective. But $\omega_1^{M[G]} = \omega_1^{M[G \upharpoonright P_1]}$ because $P_2$ is ccc and hence preserves $\omega_1$, and this is impossible.
Is that correct?