  Let $M$ be an iterable fine structural mouse.
  We prove that if $E\in M$ and $M\models$``$E$ is a countably complete short
extender whose support is a cardinal $\theta$ and
$\mathcal{H}_\theta\subseteq\mathrm{Ult}(V,E)$'' then $E$ is in the extender
sequence $\mathbb{E}^M$ of $M$. We also prove other related facts, and use them
to establish that if $\kappa$ is an uncountable cardinal of $M$ and
$(\kappa^+)^M$ exists in $M$ then $(\mathcal{H}_{\kappa^+})^M$ satisfies the
Axiom of Global Choice.
  We then prove that if $M$ satisfies the Power Set Axiom then $\mathbb{E}^M$
is definable over the universe of $M$ from the parameter
$X=\mathbb{E}^M{\upharpoonright}\aleph_1^M$, and therefore $M$ satisfies
``Every set is $\mathrm{OD}_X$''. We also prove various local versions of this
fact in which $M$ has a largest cardinal, and a version for generic extensions
of $M$.
  As a consequence, for example, the minimal proper class mouse with a Woodin
limit of Woodin cardinals models ``$V=\mathrm{HOD}$''. This adapts to many
other similar examples.
  We also describe a simplified approach to Mitchell-Steel fine structure,
which does away with the parameters $u_n$.
