[proofplan] The proof is an unwinding of the definition of the generic extension. Every element of $M[G]$ is, by definition, the $G$-interpretation of some $\mathbb{P}$-name belonging to $M$. The hypothesis on $N$ therefore places each element of $M[G]$ in $N$. Finally, $M[G]$ itself has the same closure property by its defining set comprehension, so it is the least such set or class. [/proofplan] [step:Use the defining representation of elements of $M[G]$] Let $x \in M[G]$ be arbitrary. By the definition of $M[G]$, there exists a $\mathbb{P}$-name $\tau \in M$ such that $x = \tau_G$. [guided] We begin with an arbitrary element of the generic extension and translate membership in $M[G]$ into the definition of $M[G]$. Let $x \in M[G]$. Since \begin{align*} M[G] = \{\tau_G : \tau \in M \text{ and } \tau \text{ is a } \mathbb{P}\text{-name}\}, \end{align*} membership of $x$ in $M[G]$ means precisely that $x$ is the interpretation of some $\mathbb{P}$-name from $M$. Thus there exists a $\mathbb{P}$-name $\tau \in M$ such that $x = \tau_G$. This is the only structural fact about forcing extensions needed here: no density argument or genericity argument is being used. The genericity of $G$ is part of the ambient setup that makes $M[G]$ the forcing extension, but the minimality statement follows directly from the definition of the extension as the collection of all interpreted names. [/guided] [/step] [step:Apply the closure hypothesis on $N$ to the representing name] The hypothesis on $N$ says that for every $\mathbb{P}$-name $\rho \in M$, the interpreted value $\rho_G$ belongs to $N$. Applying this with $\rho = \tau$, we obtain $\tau_G \in N$. Since $x = \tau_G$, it follows that $x \in N$. Because $x \in M[G]$ was arbitrary, we conclude that $M[G] \subset N$. [/step] [step:Verify that $M[G]$ itself has the required closure property] Let $\tau \in M$ be a $\mathbb{P}$-name. By the definition of $M[G]$, the interpreted value $\tau_G$ is an element of $M[G]$. Therefore $M[G]$ is itself a set or class containing the interpretation of every $\mathbb{P}$-name in $M$. [/step] [step:Conclude the leastness of the generic extension] Let $N$ be any set or class containing $\tau_G$ for every $\mathbb{P}$-name $\tau \in M$. The preceding inclusion argument gives $M[G] \subset N$. Since $M[G]$ also has this same property, $M[G]$ is contained in every set or class with the property and is itself one of them. Hence $M[G]$ is the least set or class containing the interpretation of every $\mathbb{P}$-name in $M$. [/step]