The Definability of the Extender Sequence From In

Abstract 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ₙ.