If $j$ is an iterable elementary embedding of a model of ZFC into one of its submodels, and, for $\gamma: \omega\to\omega$, one defines $j_\gamma$ to be the sequence whose $n$th entry is the $\gamma(n)$th iterate of $j$, then the family of all sequences $j_\gamma$ is $\Pi_1^1$-complete.