In [FSIT] and [OIMT] it is claimed that there is a surjection from $P(\kappa)\cap J^{\vec E}_{\nu(E_\alpha)}\times[\nu(E_\alpha)]^{<\omega}$ onto $\alpha$, and that this surjection lies in $J_{\alpha+1}^{\vec E}$. It is stated as a rather trivial fact, but I'm having trouble with seeing how this map should look like.
Here $\nu(E_\alpha)$ is the natural length of the $(\kappa,\alpha)$ pre-extender $E_\alpha$ and $\vec E$ is a fine extender sequence, the definition of which can be found in [OIMT] at page 11.
Since $E_\alpha$ is the trivial completion of $E_\alpha\upharpoonright\nu(E_\alpha)$ I can see that $\nu(E_\alpha)$ somehow "carries enough information" to determine $\alpha$, but this vague analogy just doesn't give me anything concrete. Of course, if a given surjection is found and is shown to be definable over $J_\alpha^{\vec E}$, then it's in $J_{\alpha+1}^{\vec E}$.
Thanks in advance!
References:
- [FSIT] "Fine structure and iteration trees" by Steel and Mitchell
- [OIMT] "Outline of inner model theory" in the handbook, by Steel (preprint at https://math.berkeley.edu/~steel/papers/steel1.pdf)