Showing that $\alpha$ isn't a cardinal in $J_{\alpha+1}^{\vec E}$ for a fine extender sequence $\vec E$ 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)

 A: We know that $\alpha = (\nu^{+})^{Ult(J^{\vec{E}}_{\alpha}, E_{\alpha})}$ and that $i_{E_{\alpha}} (\kappa) > \nu$, where $i_{E_{\alpha}}$ denotes the ultrapower embedding. Thus working in $Ult(J^{E_{\alpha}}_{\alpha}, E_{\alpha})$ any $\beta <\nu^{+}=\alpha$ can be represented in the ultrapower $Ult(J^{\vec{E}}_{\alpha}, E_{\alpha})$ using a function $f: [\kappa]^{|a|} \rightarrow \kappa$, for some $a \in [\nu]^{<\omega}$ and  $f \in J^{E_{\alpha}}_{\alpha}$. Thus we have a surjection from $(P(\kappa) \cap J^{E_{\alpha}}_{\alpha}) \times [\nu]^{<\omega}$ onto $\alpha$, via just looking at the representatives of ordinals less than $\alpha$ in the ultrapower.But the ultrapower can be constructed in $J^{\vec{E}}_{\alpha +1}$ as it has all the information. So $\alpha$ can not be a cardinal in $J^{\vec{E}}_{\alpha +1}$.
A: Here is an alternative answer (it is not true in general that $(E_{\alpha})_{a} \in J_{\alpha}^{E}$, for example when $E_{\alpha}$ is only a measure ) 
We use the fact that $g \in J_{\alpha+1}^{E} \cap P(J_{\alpha}^{E})$ iff $g$ is definable over $(J_{\alpha}^E,\in,E|\alpha,F)$. 
Define 
\begin{gather*} (\xi,\beta,\eta) \in g  \\ \longleftrightarrow \\ (J^{E}_{\alpha}, \in , E|\alpha, F) \models \xi < \kappa^{+} \\ \& \\
\exists \gamma_{\xi} \exists f_{\xi} [ (\gamma_{\xi} \ \text{is the least ordinal such that } \ F \cap J^{E}_{\xi} \in J^{E}_{\gamma_{\xi}} ) \\ \& \\ ( f_{\xi} \ \text{is the } \ <_{J^{E}_{\alpha}}- \text{least bijection from} |\gamma_{\xi}| \ \text{onto} \ \gamma_{\xi} \\ \& \\ ( (\beta,\eta) \in f_{\xi} \\ \vee \\ ( \beta < |\nu| \ \& \ \beta \not\in dom(f_{\xi}) \ \& \ \eta = \emptyset ))]
\end{gather*} 
Using lemma 2.9 from OIMT and the fact that there are no cardinals above $\nu$, it follows that $g:\kappa^{+}\times |\nu|^{J_{\alpha}^{E}} \rightarrow \alpha $ is onto.
