About a step in the proof of Gödel-Rosser Theorem. I am reading about the Gödel-Rosser Theorem, i.e. the Rosser's refinement of first Gödel's incompleteness Theorem, which states that if $\mathbf{PA}$ is consistent then it is incomplete.
I am posting this question to understand a point in its proof as written in van Dalen "Logic and Structure" 4th Edition.

Just the Foreground (Please, feel free to skip it).
Rosser's trick amounts to consider the wff $\mathscr{R}(x)$ defined by
$$\forall y[\overline{\mathrm{Neg}}(x,y)\to\forall z(\overline{\mathrm{Prov}}(z,y)\to\exists w< z\overline{\mathrm{Prov}}(w,x)],$$
where

*

*the formula $\overline{\mathrm{Neg}}(x,y)$ represents the numeric function $f$ defined by $f(m)=n$ iff there exists a wff $\phi$ such that $m$ and $n$ are the Gödel numers of $\phi$ and $\neg\phi$ respectively; and


*the formula $\overline{\mathrm{Prov}}(z,y)$ represents the numeric relation $R$ such that $(m,n)\in R$ iff there exists a wff $\phi,$ whose Gödel number is $n,$ while $m$ is the Gödel number of a deduction of $\phi.$
Applying the Fixed Point Theorem, we find  a sentence $\psi$ such that
$$\vdash\psi\leftrightarrow\neg\mathscr R(\overline{g(\psi)}),$$
where we are denoting the Godel numbering with $g,$ and the $n$-th ordinal as $\overline{n}.$

Gödel-Rosser Theorem: If $\mathbf{PA}$ is consistent then $\psi$ is indecidible, therefore $\mathbf{PA}$ is incomplete.


My Question about the Proof

In the step "if $\vdash\psi$ then $\mathbf{PA}$ is inconsistent" (see snapshot below), after having written the assumption as $\vdash\overline{Prov}(\overline{n},\overline{g(\psi)}),$ for some natural number $n,$ I think that we should distinguish between the following two cases:
$$\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)}),\tag{a}$$
$$\not\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)}).\tag{b}$$


My thoughts about
In the case $(a),$ we would get immediately the inconsistency of $\mathbf{PA},$ precisely $\overline{Prov}(\overline{n},\overline{g(\psi)})$ is indecidible.
In the case $(b),$ $\not\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)})$ implies $$\not\vdash\exists z>\overline{n}(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w<z\neg\overline{Prov}(w,\overline{g(\psi)})).\tag{*}$$
Observe that $\neg\mathscr R(\overline{g(\psi)})$ is equivalent to $\exists z(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w<z\neg\overline{Prov}(w,\overline{g(\psi)})).$
Now by $(*)$, $\vdash\psi$ and $\vdash\psi\leftrightarrow\neg\mathscr R(\overline{g(\psi)}),$ we infer $$\vdash\exists z\leq\overline{n}(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w<z\neg\overline{Prov}(w,\overline{g(\psi)})).$$
Consequently $\vdash\exists z\leq\overline{n}\overline{Prov}(z,\overline{g(\neg\psi)}),$  and so $\vdash\neg\psi.$ Therefore $\psi$ is indecidible and $\mathbf{PA}$ is inconsistent.
 A: I love van Dalen's book in general, but it has to be said that this proof isn't his clearest effort at all. For a start the move from $\vdash (\exists y < \overline{n})\varphi(y)$ to $\vdash\varphi(\overline{0})$ or $\vdash\varphi(\overline{1})$ or ... or $\vdash\varphi(\overline{n - 1})$ doesn't depend on $\varphi$ being $\Delta_0$. It obtains for any $\varphi$ so long as we are working in a theory which is as strong as Robinson Arithmetic $Q$.
But that said, the proof idea works just fine, and there is no need for a detour through an explicit mention of (a) and (b). 
Think of it like this, to stand back from the implementation details. We can construct a Rosser-provability predicate, $\mathsf{RProv}$, and then take a fixed point $\psi$ for its negation, so $\vdash \psi \equiv \neg\mathsf{RProv}([\varphi])$ We want to prove (i) $\nvdash \psi$ and (ii) $\nvdash\neg\psi$, assuming we are working in a consistent theory. We are now considering just (i).
So, for reductio, suppose $\vdash\psi$, i.e. suppose $\psi$ is provable, so (A) some number  $n$ numbers a proof of $\psi$. By our consistency assumption, (B) no number $m < n$ numbers a proof of $\neg\psi$. Because we are working in a sufficiently strong theory, given (A) and (B) we'll be able to show $\vdash \mathsf{RProv}([\varphi])$, whence $\vdash\neg\psi$, making the theory we are working in inconsistent contrary to hypothesis.  
Do we need, to make this argument fly, to explicitly make the assumption that (a) or (b) and then argue by cases? No. For it is a given that we are dealing with a consistent theory. Now once we get to (A), since we are dealing with a sufficiently strong theory, that gives us van Dalen's (2), and the consistency assumption immediately rules out (a). And though (b) is therefore immediate, it doesn't actually get mentioned in the rest of the proof which is concerned with  arguing from (B) (which involves $m < n$). 
