A countable elementary submodel need not be transitive

Hartogs: an ordinal that does not inject into a given set: For every set $A$ there is an ordinal (def-ordinal) that does not inject into $A$, that is, admits no injective function into $A$. The least such ordinal is the Hartogs number $\mathrm{\aleph }(A)$, and it is exactly

$\mathrm{\aleph }(A)=\{\mathrm{o}\mathrm{t}(S,R):S\subseteq A\text{ and }R\text{ well-orders }S\},$

the set of order types (thm-mostowski-collapse) of the well-ordered subsets of $A$.

The proof is choice free. That is the whole point of the theorem: in ZF alone, with no assumption that $A$ can be well ordered, one still gets an ordinal too long to be laid inside $A$.

Countable elementary submodels and their collapses: In ZFC, if an infinite set membership structure $M$ satisfies Extensionality, then for every at most countable $A\subseteq M$ there is a countably infinite $X\prec M$ containing $A$, and $X$ has a countable transitive collapse. To retain a set $a\in M$ as one parameter, use $A=\{a\}$.

What the collapse fixes: Let $\pi :X\to \bar{X}$ be a collapse of actual membership as above. It fixes every transitive subset $A\subseteq X$ pointwise. If $\alpha \in X$ is an actual ordinal, $\pi (\alpha )$ is the order type of $X\cap \alpha$. In particular, if $X\cap \alpha$ is transitive, $\pi (\alpha )=X\cap \alpha$.

The Axiom of Choice: Every family of nonempty sets has a choice function