I am referring to the proof of (4) implies (1) in Theorem 3.16 of Woodin's *The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal*. His proof leverages on the fact that if the sharp of every real exists, then $\delta^1\_2 = u\_2$, where $u\_2$ is the second uniform indiscernible (the least ordinal above $\omega\_1$ which is an $x$-indiscernible for every real $x$).


This is roughly how it goes:


* Fix any ordinal $\alpha$ strictly between $\omega\_1$ and $\omega\_2$, and a well-ordering $<\_{\alpha}$ of $\omega\_1$ of ordertype $\alpha$.
* Find a club $C$ of $\omega\_1$ such that for every $\gamma \in C$, the rank of $<\_{\alpha}$ restricted to $\gamma$ is less than the least ordinal in C greater than $\gamma$.
* By hypothesis, there is a $D \subset C$, $D$ a club of $\omega\_1$, such that $D$ is constructible from a real $z$. We can assume $D$ is definable from $z$ and $\omega\_1$ in $L[z]$ since $z^\sharp$ exists.
* By reflecting the definition of $D$ downwards, we have that for every $\gamma \in D$, $rank(<\_{\alpha} \restriction \gamma) < rank(\mathcal{M}(z^{\sharp}, \gamma + 1))$, where $\mathcal{M}(z^{\sharp}, \gamma + 1)$ stands for (quoting Woodin) "the $\gamma$[$+1$] model of $z^{\sharp}$". I am not exactly sure what that quote means, so I assumed $rank(\mathcal{M}(z^{\sharp}, \gamma + 1))$ is the least $z$-indiscernible above $\gamma$, which works for the arguments hitherto. Did I make a mistake in my interpretation here?
* Now, following the previous inequality of ranks, he immediately concluded that $\alpha < rank(\mathcal{M}(z^{\sharp}, \omega\_1 + 1))$, which finishes the proof.


It is at the last step (the final bullet point) that I got lost. How does $\alpha < rank(\mathcal{M}(z^{\sharp}, \omega\_1 + 1))$ follow from the previous steps?


EDIT: Alternatively, I would appreciate it if anyone can point me to another proof of the statement "if the sharp of every real exists and every club contains a club constructible from a real, then $\delta^1\_2 = \omega\_2$"



On a particular proof of "if the sharp of every real exists and every club contains a club constructible from a real, then $\delta^1_2 = \omega_2$"
Let $\kappa$ be a sufficiently large regular cardinal. Take a countable elementary substructure $H$ of $H(\kappa)$ containing $z$ and $<\_\alpha$ with $\omega\_1\cap H\in D$. Let $\pi : M\to H(\kappa)$ be the inverse of the transitive collapse of $H$. To see the fifth bullet point, it suffices to show that in $M$, $\pi^{-1}(<\_\alpha)$ has rank less than $(\text{rk}(\mathcal M(z^\#,\omega\_1^M+1)))^M$. But this follows from the fourth bullet point since $\omega\_1^M = \omega\_1\cap H \in D$, $\pi^{-1}({<}\_\alpha) = {<}\_\alpha \restriction \omega\_1^M$, and $M$ correctly computes $\text{rk}(\mathcal M(z^\#,\omega\_1^M+1))$ since $z^\#$ is in $M$. 


