I'm trying to understand the proof in Kunen's book (Set Theory) of $PFA \implies SOCA.$ (Proper Forcing Axiom, Semi Open Coloring Axiom.) I do not think you need to know all the details to the proof to answer my questions. So you may want to skip these definitions and the proof.
Given $W\subseteq E\times E$ symmetric (with respect to the diagonal) a subset of $T$ of $E$ is called $W$-connected if $T\times T \setminus \Delta T$ is contained in $W$ and $W$-free if $T\times T \setminus \Delta T$ is disjoint from $W$. (Where $\Delta T$ is $T$'s diagonal.)
$SOCA$ is the statement: Whenever $E$ is an uncountable separable metric space and $W$ is an open susbet of $E\times E \setminus \Delta E$ with $W$ symmetric, there is an uncountable subse $T$ of $E$ such that either $T$ is $W$-connected or $T$ is $W$-free.
$\textbf{My first question:}$ Kunen uses the Countable Transitive Model approach to forcing. I make sense of this proof this way: We assume $PFA$. We fix $M$ a countable transitive model for ZFC and fix an uncountable separable metric space $E$ in it, and we show that $SOCA$ holds for it. This proves $PFA$ implies $SOCA$ as if it is true for an arbitrary metric space of an arbitrary countable model, then it is true for every model of ZFC and hence a consequence of ZFC. As if we get a model of ZFC where $SOCA$ fails we could get a countable transitive model where it fails. Is this reasoning correct?
$\textbf{My second question:}$ As I want $SOCA$ to be true in my fixed countable transitive $M$, I need the set (third paragraph) $\{e_\eta:\eta\in I\}$ to be an element of $M$, but to get this I probably need $I$ to be an element of $M$ as well. But as $I$ uses $G$ in its definition it seems likely that it is not actually an element of $M$. How do I fix this problem? How do I check that $\{e_\eta:\eta\in I\}\in M$? Or is this not what I want?
I appreciate very much any kind of help. Thank you for reading.