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.
 A: Yes, it does.
Working in a model $V$ of ZF-AoI, suppose $M$ is a set model of ZF-AoI. Then consider the set $X\subset M$ of $M$-ordinals, ordered by $\in^M$. This is a linear order. 
Of course, it may not be well-founded, but it has a well-founded part. Let $$Y=\{x\in X: \mbox{the suborder of $M$-ordinals $<x$ is well-founded}\}.$$ This is easily checked to be a well-ordering itself with no greatest element. Now, by Replacement, $Y$ intial-segment-embeds into the ordinals of our background model $V$; let $\alpha$ be the supremum of the image of this embedding. Now it's not hard to show that $\alpha$ (that is, the set of ordinals below $\alpha$) is an inductive set.
A: 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$.
