Here is a proof of the categoricity of second-order Peano arithmetic. I have trouble understanding a part of it. Let $\mathfrak N=(V',\mathbb N,\text P(\mathbb N),\text P(\mathbb N^2),\text P(\mathbb N^3),...)$ be the standard model and $\mathfrak M=(V,D,\text P(D),\text P(D^2),\text P(D^3),...)$ be a full model for PA$_2$ where $D,\text P(D^n)$s are carriers for individuals and relations and $V$ assigns constant symbols to elements of their carriers. The proof shows there is a $\tilde0\in D$ and a successor $\sigma(a)$ for each $a\in D$. It then constructs a yet-to-be-proved isomorphism $f:\mathbb N\rightarrow D,f(0)=\tilde 0,f(n+1)=\sigma(f(n))$ and shows it's injective. To prove it is surjective, it claims that
On the other hand $\tilde0=f(0)\in f(\mathbb N)\subseteq D$ then $\sigma(a)=f(n+1)\in f(\mathbb N)\subseteq D$. Thus $\mathfrak M\vDash\forall x[\mbox Z_0(x)\rightarrow\textbf M(x)]$ and $\mathfrak M\vDash\forall x\forall y[\textbf M(x)\rightarrow[\mbox S(x,y)\rightarrow\mathbf M(y)]]$ where $\textbf M=f(\mathbb N)$
and then uses axiom of induction to proceed. S($y,x$) is intended to mean $x=y+1$ and Z$_0(x)$:=$\forall y$~S($y,x$).
What I don't understand is the use of $\textbf M$. $\textbf M$ is not a symbol in the object language so it must be a meta-symbol to be substituted by something in the object language. But $\textbf M=f(\mathbb N)$? Does it mean M is to be replaced by $f(\mathbb N)$ like macros in C or they have same denotation? I doubt the first case because $f(\mathbb N)$ is also in the metalanguage denoting a semantical thing.
The proof is from Mathematical Logic: A First Course by Joel W. Robbin, page 162. Thanks.
