[proofplan]
We prove the two required containments by exhibiting explicit $\mathbb{P}$-names in $M$. For each $x \in M$, the canonical check name $\check{x}$ belongs to $M$ and evaluates to $x$, so every ground-model set appears in the generic extension. Then we define the canonical name $\dot{G}$ for the generic filter using the conditions of $\mathbb{P}$ itself, verify that $\dot{G} \in M$, and compute its valuation to be exactly $G$.
[/proofplan]
[step:Build the check name of each ground-model set inside $M$]
Fix $x \in M$. Define the check-name assignment on the [transitive closure](/theorems/1493) of $x$ by recursion on rank: for each set $a$ in that closure,
\begin{align*}
\check{a} := \{(\check{b}, 1_{\mathbb{P}}) : b \in a\}.
\end{align*}
Since $M$ is transitive, every $b \in a$ which occurs in this recursion belongs to $M$. Since $\mathbb{P} \in M$, its greatest condition $1_{\mathbb{P}}$ belongs to M. The recursive definition is therefore carried out inside $M$, and by the closure of $M$ under the set-forming operations used in the recursion, $\check{x} \in M$. Moreover $\check{x}$ is a $\mathbb{P}$-name, because each pair appearing in it has the form $(\sigma,p)$ with $\sigma$ a $\mathbb{P}$-name and $p \in \mathbb{P}$.
[guided]
Fix $x \in M$. The purpose of the check name is to represent the old set $x$ as a forcing name whose interpretation will not depend on the generic filter. We define it recursively by rank. For every set $a$ appearing in the transitive closure of $x$, put
\begin{align*}
\check{a} := \{(\check{b}, 1_{\mathbb{P}}) : b \in a\}.
\end{align*}
This definition is legitimate inside $M$ for two reasons. First, $M$ is transitive, so whenever $a \in M$ and $b \in a$, we also have $b \in M$. Thus the recursion never leaves $M$ while descending through elements of $x$. Second, $\mathbb{P} \in M$, so the distinguished greatest condition $1_{\mathbb{P}}$ is an object of $M$. Hence every pair $(\check{b},1_{\mathbb{P}})$ used to form $\check{a}$ is built from objects already available in $M$ at earlier stages of the recursion.
The output $\check{x}$ is a $\mathbb{P}$-name because its elements are ordered pairs $(\sigma,p)$ where $\sigma$ is a previously constructed $\mathbb{P}$-name and $p = 1_{\mathbb{P}} \in \mathbb{P}$. Since the recursion is performed over the set-theoretic rank of elements below $x$, the final object $\check{x}$ belongs to $M$.
[/guided]
[/step]
[step:Evaluate each check name as the original set]
We prove by induction on rank that
\begin{align*}
\operatorname{val}_G(\check{a}) = a
\end{align*}
for every $a \in M$. By definition of valuation,
\begin{align*}
\operatorname{val}_G(\check{a}) = \{\operatorname{val}_G(\check{b}) : b \in a \text{ and } 1_{\mathbb{P}} \in G\}.
\end{align*}
Since $G$ is a filter on $\mathbb{P}$ and $1_{\mathbb{P}}$ is the greatest condition, $1_{\mathbb{P}} \in G$. The induction hypothesis gives $\operatorname{val}_G(\check{b}) = b$ for every $b \in a$, so
\begin{align*}
\operatorname{val}_G(\check{a}) = \{b : b \in a\} = a.
\end{align*}
Taking $a=x$, we obtain $\operatorname{val}_G(\check{x}) = x$. Since $\check{x} \in M$ is a $\mathbb{P}$-name, the definition of $M[G]$ gives $x \in M[G]$. Because $x \in M$ was arbitrary, $M \subset M[G]$.
[/step]
[step:Define the canonical name for the generic filter inside $M$]
Define the canonical generic-filter name by
\begin{align*}
\dot{G} := \{(\check{p},p) : p \in \mathbb{P}\}.
\end{align*}
For every $p \in \mathbb{P}$, transitivity and $\mathbb{P} \in M$ imply $p \in M$, so the previous steps give $\check{p} \in M$. Therefore the displayed set is definable in $M$ from the parameter $\mathbb{P}$, and hence $\dot{G} \in M$. It is a $\mathbb{P}$-name because each element has the form $(\check{p},p)$ with $\check{p}$ a $\mathbb{P}$-name and $p \in \mathbb{P}$.
[/step]
[step:Evaluate the canonical generic-filter name as $G$]
By the definition of valuation,
\begin{align*}
\operatorname{val}_G(\dot{G}) = \{\operatorname{val}_G(\check{p}) : p \in \mathbb{P} \text{ and } p \in G\}.
\end{align*}
The check-name computation gives $\operatorname{val}_G(\check{p}) = p$ for every $p \in \mathbb{P}$. Hence
\begin{align*}
\operatorname{val}_G(\dot{G}) = \{p : p \in \mathbb{P} \text{ and } p \in G\}.
\end{align*}
Since $G \subset \mathbb{P}$, this set is exactly $G$. Thus $\operatorname{val}_G(\dot{G}) = G$. Because $\dot{G} \in M$ is a $\mathbb{P}$-name, the definition of $M[G]$ gives $G \in M[G]$.
[/step]
[step:Combine the two explicit names]
The check-name construction shows that every $x \in M$ is equal to $\operatorname{val}_G(\check{x})$ for some $\mathbb{P}$-name $\check{x} \in M$, so $M \subset M[G]$. The canonical generic-filter name satisfies $\dot{G} \in M$ and $\operatorname{val}_G(\dot{G}) = G$, so $G \in M[G]$. These are exactly the two assertions of the theorem.
[/step]
