[proofplan] We prove transitivity directly from the recursive definition of name evaluation. Given $x \in y \in M[G]$, choose a $\mathbb{P}$-name $\tau \in M$ with $y = \tau_G$. Membership in $\tau_G$ means that $x$ is the evaluation of some name $\sigma$ appearing in $\tau$ together with a condition from $G$. Since $\tau \in M$ and $M$ is transitive, that name $\sigma$ belongs to $M$, so its evaluation $\sigma_G$ belongs to $M[G]$. [/proofplan] [step:Represent the element of the extension by a name in $M$] Let $x$ and $y$ be sets such that $x \in y$ and $y \in M[G]$. By the definition of $M[G]$, there exists a $\mathbb{P}$-name $\tau \in M$ such that \begin{align*} y = \tau_G. \end{align*} The recursive evaluation of a $\mathbb{P}$-name by $G$ is \begin{align*} \tau_G = \{\sigma_G : \text{there exists } p \in G \text{ such that } (\sigma,p) \in \tau\}. \end{align*} Since $x \in y = \tau_G$, this definition gives a $\mathbb{P}$-name $\sigma$ and a condition $p \in G$ such that \begin{align*} (\sigma,p) \in \tau \end{align*} and \begin{align*} x = \sigma_G. \end{align*} [/step] [step:Use transitivity of $M$ to show the witnessing name lies in $M$] Because $\tau \in M$ and $(\sigma,p) \in \tau$, transitivity of $M$ implies \begin{align*} (\sigma,p) \in M. \end{align*} Using the standard ordered-pair coding, membership of $(\sigma,p)$ in the transitive set $M$ implies that each coordinate of the ordered pair belongs to $M$. In particular, \begin{align*} \sigma \in M. \end{align*} [guided] The only point that needs care is why the name $\sigma$ itself belongs to $M$. We know that $\tau \in M$ and that $(\sigma,p) \in \tau$. Since $M$ is transitive, every element of every element of $M$ is again an element of $M$. Applying this to the element $\tau \in M$ gives \begin{align*} (\sigma,p) \in M. \end{align*} Now we extract the first coordinate of the ordered pair. With the usual Kuratowski coding, \begin{align*} (\sigma,p) = \{\{\sigma\},\{\sigma,p\}\}. \end{align*} Since $(\sigma,p) \in M$ and $M$ is transitive, every element of $(\sigma,p)$ lies in $M$, so $\{\sigma\} \in M$. Applying transitivity once more to $\{\sigma\} \in M$ gives \begin{align*} \sigma \in M. \end{align*} This is exactly what is needed: the object whose evaluation gives $x$ is not merely some external name, but a name already contained in the ground model $M$. [/guided] [/step] [step:Conclude that every element of an element of $M[G]$ lies in $M[G]$] We have shown that $\sigma \in M$ and that \begin{align*} x = \sigma_G. \end{align*} Therefore, by the definition of the forcing extension, \begin{align*} x \in M[G]. \end{align*} Since $x$ and $y$ were arbitrary with $x \in y$ and $y \in M[G]$, the set $M[G]$ is transitive. [/step]