The theorem states that for every closed formula $\tau$ of signature $\sigma$ there exists a formula $\tau'$ in the $\sum_2$ class (of the signature $\sigma$ with some additional predicate symbols) that is a validity iff $\tau$ is a validity.
The semantic proof that I know considers the dual question of satisfiability (since $\lnot \tau$ is satisfiable iff $\tau$ is not a validity) and thus instead proves that there exists a corresponding formula in $\prod_2$. It's probably easier shown by example: if the source formula is $\forall x \forall y \exists z \forall u \exists v \varphi(x, y, z, u, v)$, then the corresponding formula $\psi$ would be
\begin{align*} \forall x \forall y \exists z &\ F(x, y, z) \land \\ \forall x \forall y \forall u \exists v &\ G(x, y, u, v) \land \\ \forall x \forall y \forall z \forall u \forall v &\ (F(x, y, z) \land G(x, y, u, v) \rightarrow \varphi (x, y, z, u, v)), \end{align*}
which is a conjunction of $\prod_2$ formulas and thus is in $\prod_2$, and its negation is in $\sum_2$, as expected.
Clearly, it's satisfiable iff the original formula is satisfiable (as we're free to choose $F$ and $G$ to be the predicates corresponding to the Skolem functions), so we're done.
But can we prove the theorem purely syntactically, by considering derivations instead of the semantic notion of satisfiability? That is, in this case, can we show that $\{ \forall x \forall y \exists z \forall u \exists v \varphi(x, y, z, u, v) \} \vdash \psi$, and, in the other direction, $\{ \psi \} \vdash \forall x \forall y \exists z \forall u \exists v \varphi(x, y, z, u, v)$? Would that be insightful compared to the semantic proof? I tried to do the derivation myself, but got lost quickly, as I don't have much intuition for FOL derivations.