 Solution

The forcing theorem has two central clauses. Definability: for each first-order formula $\phi$, the relation $p⊩\phi (\vec{\tau })$ on conditions and ground-model names is first-order definable in $M$. Truth lemma: for every $M$-generic $G$ and every tuple of names in $M$,Forcing is monotone under strengthening and agrees with the generic-extension semantics. Together with the generic model construction, $M[G]$ is a transitive model of ZFC containing $M$ with the same ordinals. The definability and truth clauses are the auxiliary parts used when proving individual extension axioms.