Step-indexed separation logic has proven to be a powerful tool for modular reasoning about higher-order stateful programs. However, it has only been used to reason about safety properties, never liveness properties. In this paper, we observe that the inability of step-indexed separation logic to support liveness properties stems fundamentally from its failure to validate what we call the \emph{existential property}, connecting the meaning of existential quantification inside and outside the logic. We show how to validate the existential property—and thus enable liveness reasoning—by moving from finite step-indices (natural numbers) to \emph{transfinite} step-indices (ordinals). Concretely, we transform the Coq-based step-indexed logic Iris to \textbf{Transfinite Iris}, and demonstrate its effectiveness in proving termination and termination-preserving refinement for higher-order stateful programs.