My question concerns the proof of the fact that the set of valid sentences of 2nd order logic (SOL) is not recursively enumerable, as presented in "Computability and Logic" 4th edition in Proposition 22.8
Let $\ulcorner\varphi\urcorner$ be the Gödel number of $\varphi$. Let $\mathrm{PA}_2$ be the conjunction of the axioms for 2nd order Peano arithmetic. The function $f$ that takes $\ulcorner\varphi\urcorner$ to $\ulcorner\mathrm{PA}_2\rightarrow\varphi\urcorner$ is recursive. Let $\mathfrak{N}$ be the standard model of arithmetic. Consider it to be the full model when the SOL is taken into account. Now, consider $\mathrm{Th}(\mathfrak{N})$ - the first-order theory of $\mathfrak{N}$, about which we know that is not definable, the more so is not r.e. We have: $$\varphi\in\mathrm{Th}(\mathfrak{N})\qquad\text{iff}\qquad\vDash\mathrm{PA}_2\rightarrow\varphi\,.$$ The conclusion that is drawn, is that if the set $\mathrm{Val}_2$ of Gödel numbers of 2nd order logical validities were r.e., $\mathrm{Th}(\mathfrak{N})$ would have to be r.e., but we know it is not. However, does r.e. of $\mathrm{Val}_2$ entail r.e. of $A=\{\ulcorner\mathrm{PA}_2\rightarrow\varphi\urcorner\mid\varphi\in\mathrm{Th}(\mathfrak{N})\}$? For what I can see, the proof demonstrates that the recursive function $f$ sends $\mathrm{Th}(\mathfrak{N})$ onto $A$, which is a proper subset of $\mathrm{Val}_2$ (which contains, e.g., numbers of all formulas $\mathrm{PA}_2\rightarrow\psi$, where $\psi$ is a 2nd order formula true in the stadnard full model): $$\mathrm{Th}(\mathfrak{N})=f^{-1}[A]\qquad\text{and}\qquad A\subsetneq\mathrm{Val}_2\,.$$ In general, subsets of r.e. sets are not r.e., so I cannot reason like "If $\mathrm{Val}_2$ were r.e., then $A$ would be too, and so $\mathrm{Th}(\mathfrak{N})$ either".
What am I missing to see that the set of valid formulas of SOL cannot be r.e.?
Note first that $$ A=\{\ulcorner\mathrm{PA}_2\rightarrow\varphi\urcorner\mid\varphi\in\mathrm{Th}(\mathfrak{N})\}=\{\ulcorner\mathrm{PA}_2\rightarrow\varphi\urcorner\mid(\mathrm{PA}_2\rightarrow\varphi)\in\mathrm{Val}_2,\varphi\text{ is a $\mathrm{PA}_1$-formula}\}. $$ Now assume you had an algorithm $f$ which outputs $\mathrm{Val}_2$. Consider the function $f'$ which works like $f$, but discards all formulas in the output which are not of the form $\mathrm{PA}_2\rightarrow\varphi$ where $\varphi$ is a $\mathrm{PA}_1$-formula. Since this is only a simple syntactic check, $f'$ is computable as well and so $A$ is r.e. From this you get the desired contradiction.