The Definability of the Extender Sequence From In

Let M be a short extender mouse. We prove that if E∈ M and M “ E is a countably complete short extender whose support is a cardinal θ and H_θ ⊆ Ult(V,E) ”, then E is in the extender sequence EM of M . We also prove other related facts, and use them to establish that if κ is an uncountable cardinal of M and κ +M exists in M then (Hκ ⁺)M satisfies the Axiom of Global Choice. We prove that if M satisfies the Power Set Axiom then EM is definable over the universe of M from the parameter X=EM\! \! ₁M , and M satisfies “Every set is OD_\ ”. 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=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ₙ .