In set theory, a branch of mathematics, a rank-into-rank embedding is a large cardinal property defined by one of the following four axioms given in order of increasing consistency strength. (A set of rank < \lambda is one of the elements of the set V_\lambda of the von Neumann hierarchy.) These are essentially the strongest known large cardinal axioms not known to be inconsistent in ZFC; the axiom for Reinhardt cardinals is stronger, but is not consistent with the axiom of choice. If j is the elementary embedding mentioned in one of these axioms and \kappa is its critical point, then \lambda is the limit of j^n(\kappa) as n goes to \omega. More generally, if the axiom of choice holds, it is provable that if there is a nontrivial elementary embedding of V_\alpha into itself then \alpha is either a limit ordinal of cofinality \omega or the successor of such an ordinal. The axioms I0, I1, I2, and I3 were at first suspected to be inconsistent (in ZFC) as it was thought possible that Kunen's inconsistency theorem that Reinhardt cardinals are inconsistent with the axiom of choice could be extended to them, but this has not yet happened and they are now usually believed to be consistent. Every I0 cardinal \kappa (speaking here of the critical point of j) is an I1 cardinal. Every I1 cardinal \kappa (sometimes called ω-huge cardinals) is an I2 cardinal and has a stationary set of I2 cardinals below it. Every I2 cardinal \kappa is an I3 cardinal and has a stationary set of I3 cardinals below it. Every I3 cardinal \kappa has another I3 cardinal above it and is an n-huge cardinal for every n< \omega. Axiom I1 implies that (equivalently, ) does not satisfy V=HOD. There is no set definable in (even from parameters V_\lambda and ordinals <\lambda^+) with S cofinal in \lambda and, that is, no such S witnesses that \lambda is singular. And similarly for Axiom I0 and ordinal definability in (even from parameters in V_\lambda). However globally, and even in V_\lambda, V=HOD is relatively consistent with Axiom I1. Notice that I0 is sometimes strengthened further by adding an "Icarus set", so that it would be The Icarus set should be in but chosen to avoid creating an inconsistency. So for example, it cannot encode a well-ordering of. See section 10 of Dimonte for more details. Woodin defined a sequence of sets for use as Icarus sets.