Question about the incompleteness proof (Theorem V) Question in short: Where do I find a complete proof of Theorem V from Gödels incompleteness proof? If it does not exists, can someone provide it?

Question in detail:
I am trying to understand Gödels incompleteness proof, by reading the following translation here. I was able to follow the proof until the bottom of page 13, where he states Theorem V.
I tried to proof Theorem V for a constant primitive recursive function $\phi(\nu) = c$, then one only has to show that
$$  y = \phi(\nu) \Rightarrow \quad \vdash \varphi(\overline{y},\overline{\nu}) $$
$$  y \neq \phi(\nu) \Rightarrow \quad \vdash \neg \varphi(\overline{y},\overline{\nu}) $$
where for $n \in \mathbb{N}$ we define $$\overline{n}= \underbrace{f\cdots f}_{\text{n times}} 0,$$
and
$$\varphi(y_1,x_1) := (y_1 = \overline{c}), $$
where '=' is a metasymbol for
$$ x_i = y_i :\Leftrightarrow \forall z_{i+1} (z_{i+1}(x_i) \rightarrow z_{i+1}(y_i) $$
I can proof within PA that it holds
$$ \vdash \sigma_i = \sigma_i$$
for any variable of typ $i \in \mathbb{N}$. To be more precise, from axiom II it follows $p \Rightarrow p$. Therefore, it holds
$$  \begin{align}\vdash & z_{i+1}(\sigma_i) \Rightarrow z_{i+1}(\sigma_i) \\
\vdash& \forall z_{i+1}( z_{i+1}(\sigma_i) \Rightarrow z_{i+1}(\sigma_i))  \end{align}$$
 Now, if $y =\phi(\nu) =c$, then $\overline{y}$ and $\overline{c}$ denote the same sign of type one. Therefore, one can prove that
$$ \vdash \overline{y} = \overline{c}.$$ 
However, I already struggle to prove that if $y \neq c$ that then $$\vdash \neg( \overline{y} = \overline{c}).$$ 
How do I prove that? Does anyone know a source where the complete detailed proof of Theorem V is given?
Also, if I understood it correctly, then the prove for $$  y \neq \phi(\nu) \Rightarrow \quad \vdash \neg \varphi(\overline{y},\overline{\nu}) $$
can only be shown with metamathematic and it does not derive from some formal PA system, right?
 A: For a modern exposition, see Elliott Mendelson, Introduction to mathematical logic (4ed - 1997), Ch.3.2 NUMBER-THEORETIC FUNCTIONS AND RELATIONS : 

We say that a number-theoretic relation $R$ of $n$ arguments is expressible in $K$ if and only if there is a wf $\varphi(x_1,\ldots, x_n)$ of $K$ with the free variables $x_1,\ldots, x_n$, such that, for any natural numbers $k_1,\ldots, k_n$, the following hold: 

    
*
    
*If $R(k_1,\ldots, k_n)$ is true, then $\vdash_K \varphi(\overline {k_1},\ldots, \overline {k_n})$.
    
*If $R(k_1,\ldots, k_n)$ is false, then $\vdash_K \lnot \varphi(\overline {k_1},\ldots, \overline {k_n})$. 


After this definition there is a long list of number-theoretic relations (and functions) which are showed to be representable.

For example, the number-theoretic relation of identity is expressed in $S$ by the wf $x = x$.
In fact, if $k_1 = k_2$, then $\overline {k_1}$ is the same term as $\overline {k_2}$ and so, by Proposition 3.2(a) $\vdash_S \overline {k_1} = \overline {k_2}$. 
Moreover, if $k_1 \ne k_2$ then, by Proposition 3.6(a), $\vdash_S \lnot \overline {k_1} = \overline {k_2}$. 
Likewise, the relation 'less than' is expressed in $S$ by the wf $x_1 < x_2$. Recall 
  that $x_1 < x_2$ is $(\exists x_3)(x_3 \ne 0 \land x_3 + x_1 = x_2)$. If $k_1 < k_2$, then there is some non-zero number $n$ such that $k_2 = n + k_1$.  

All these results are achieved proving that the system $S$ (usual Robinson arithmetic) has "enough expressive capabilities".
See e.g. Mendelson, PROPOSITION 3.6(a) :

Let $m,n$ be any natural numbers. 
(i) If $m \ne n$, then $\vdash_S \lnot \overline {m} = \overline {n}$.
(ii) $\vdash_S \overline {m+n} = \overline {m} + \overline {n}$ and $\vdash_S \overline {m \cdot n} = \overline {m} \cdot \overline {n}$.

These results are metamathematical : they show that for every $m,n$ there is a formal derivation in $S$ of the corresponding formula. But their proof is constructive : it shows a formal derivation is $S$ of the required formula.
