Can ZF-AoI prove that all models of ZF-AoI are at least countable? Do we have:
$${\sf ZF-AoI}\vdash\forall X,(X\text{ is a model of }{\sf ZF-AoI})\implies(X\text{ is at least countable})$$
AoI is the axiom of infinity.
I know that some models of $\sf ZF-AoI$ have no at-least-countable sets, but I'm fairly certain that those models contain no models of $\sf ZF-AoI$, making the statement vacuously true in those models.

In ZF$-$Infinity, you can prove if $X$ is a model of just Extensionality, Pairing, and Union, then $X$ contains a unique element that is isomorphic to each finite ordinal (where a "finite" ordinal is one that is not a superset of any limit ordinal), and these elements are different for different finite ordinals.
By the Axiom of Replacement, we can then (at the metalevel) make a set of all finite ordinals by mapping each element of $X$ to the unique ordinal it represents, if any, and to $\varnothing$ otherwise. This set will then be $\omega$ and inject into $X$.
