The Completeness of PA with the ω-rule

Although it's a well-known fact that the theory obtained by "closing $PA$ under the $\omega$-rule" is complete, I cannot find an immediately available online source, so here is a proof. (Something like this is in a proof theory textbook, like Takeuti, but almost all my books are a thousand miles away.)

The language $L_A$ is the first-order language of arithmetic with $=,0,S,+$ and $\times$. Assume a Hilbert-style linear deductive system, with Modus Ponens; By "$\varphi$ is an axiom of $PA$" I mean "either $\varphi$ is a logical axiom or $\varphi$ is one of usual axioms for $S,+$ and $\times$, or $\varphi$ is an instance of induction". But we shall allow infinitely long derivations, indexed by ordinals. We define the system $P{A}^{\omega }$ as follows: a (possibly infinite) sequence $({\theta }_0,...,{\theta }_{\alpha })$ of formulas is an derivation in $\omega$-logic from $PA$ iff, for each $\beta \le \alpha$:

(i) either ${\theta }_{\beta }$ is an axiom of $PA$;
(ii) or there are $\gamma ,\delta <\beta$, such that ${\theta }_{\delta }$ has the form ${\theta }_{\gamma }\to {\theta }_{\beta }$;
(iii) or ${\theta }_{\beta }$ has the form $\mathrm{\forall }x\psi (x)$ for some formula $\psi (x)$ with exactly $x$ free, and there is an injection $f:\omega \to \beta$ such that ${\theta }_{f(n)}=\psi (n)$, for all $n\in \omega$.

Here $\alpha ,\beta ,\gamma$ and $\delta$ are ordinals; derivations may be infinite; the second condition (ii) expresses a single application of Modus Ponens; the third condition (iii) expresses a single application of the $\omega$-rule - roughly, the derivation has a subsequence which is an $\omega$-sequence of the form $\psi (0),\psi (1),...$, and the "conclusion" formula has the form $\mathrm{\forall }x\psi (x)$.

Say that $\varphi$ is a theorem of $PA$ in $\omega$-logic just when there is an $\omega$-derivation of the form $(\dots ,\varphi )$ from $PA$. Let $P{A}^{\omega }$ be the set of theorems of $PA$ in $\omega$-logic. We aim to prove that: $P{A}^{\omega }$ is the same as true arithmetic; that is,

Theorem. $P{A}^{\omega }=Th(\mathbb{N})$.

Lemma 1. If, for all $n\in \omega ,\varphi (n)\in P{A}^{\omega }$, then $\mathrm{\forall }x\varphi (x)\in P{A}^{\omega }$. (I.e., $P{A}^{\omega }$ is closed under the $\omega$-rule.)
[Proof: Assume that, for all $n\in \omega ,\varphi (n)\in P{A}^{\omega }$. So, for each $\varphi (n)$, there is an $\omega$-derivation; next, take all these $\omega$-derivations (of $\varphi (0),\varphi (1)$, etc.) and paste them together; place the formula $\mathrm{\forall }x\varphi (x)$ at the end. This is an $\omega$-derivation of $\mathrm{\forall }x\varphi (x)$. So, $\mathrm{\forall }x\varphi (x)\in P{A}^{\omega }$.]

Lemma 2. If $\varphi \in P{A}^{\omega }$, then $\mathbb{N}\models \varphi$. (I.e., $P{A}^{\omega }$ is sound.)
[Proof: Each axiom of $PA$ is true in $\mathbb{N}$. Modus ponens is sound for $\mathbb{N}$. The $\omega$-rule is sound for $\mathbb{N}$. Hence, in any given $\omega$-derivation from $PA$, every formula is true in $\mathbb{N}$. So, all $\omega$-theorems of $PA$ are true in $\mathbb{N}$.]

Lemma 3. For all sentences $\varphi$, either $\varphi \in P{A}^{\omega }$ or $\mathrm{\neg }\varphi \in P{A}^{\omega }$. (I.e., $P{A}^{\omega }$ is complete.)
[Proof. This is by induction on the complexity of $\varphi$. $PA$ is itself negation-complete for atomic sentences. If $\varphi$ is of the form $\mathrm{\neg }\theta$ and either $\theta \in P{A}^{\omega }$ or $\mathrm{\neg }\theta \in P{A}^{\omega }$, then either $\mathrm{\neg }\mathrm{\neg }\theta \in P{A}^{\omega }$ or $\mathrm{\neg }\theta \in P{A}^{\omega }$; and so, either $\varphi \in P{A}^{\omega }$ or $\mathrm{\neg }\varphi \in P{A}^{\omega }$. And similarly with conjunctions.
For quantified formulas, suppose $\varphi$ has the form $\mathrm{\forall }x\psi$. As induction hypothesis, suppose that, for all $n\in \omega$, either $\psi (n)\in P{A}^{\omega }$ or $\mathrm{\neg }\psi (n)\in P{A}^{\omega }$. Consider two cases.
Case 1. Suppose that, for all $n\in \omega$, $\psi (n)\in P{A}^{\omega }$. Then, $\mathrm{\forall }x\psi \in P{A}^{\omega }$, by lemma 1. So, either $\varphi \in P{A}^{\omega }$ or $\mathrm{\neg }\varphi \in P{A}^{\omega }$, as required.
Case 2. Suppose that, for some $n\in \omega$, $\psi (n)\notin P{A}^{\omega }$. So, by induction hypothesis, $\mathrm{\neg }\psi (n)\in P{A}^{\omega }$. So, $\mathrm{\exists }x\mathrm{\neg }\psi \in P{A}^{\omega }$. So, $\mathrm{\neg }\varphi \in P{A}^{\omega }$. So, either $\varphi \in P{A}^{\omega }$ or $\mathrm{\neg }\varphi \in P{A}^{\omega }$, as required.]

Lemmas 2 and 3 say that $P{A}^{\omega }$ is sound and complete. Hence, all of its models are elementarily equivalent. Since $\mathbb{N}$ is a model of $P{A}^{\omega }$, all of its models are elementarily equivalent to $\mathbb{N}$. So, $P{A}^{\omega }=Th(\mathbb{N})$. In fact, the only properties of $PA$ we actually needed to use are that its axioms are true in $\mathbb{N}$ and that it is negation-complete for atomic sentences. These properties both hold for Robinson arithmetic $Q$. So, we get that $Q^{\omega }=Th(\mathbb{N})$.