Every set model of first-order ZF has infinitely many elements

For $a\in M$, Pairing with both inputs $a$ gives $s\in M$ such that for all $t\in M$, $tEs$ iff $t=a$. Thus $aEs$, and $s$ has an $E$-member. Foundation applied inside $\mathcal{M}$ to $s$ gives $bEs$ with no $u\in M$ satisfying both $uEb$ and $uEs$. Necessarily $b=a$. If $aEa$, choosing $u=a$ would satisfy both relations, a contradiction. Therefore $aEa$ fails for every $a\in M$. This derives irreflexivity internally from actual axiom instances, without asserting that $E$ is externally well founded.

Infinity gives $I,e\in M$ with $eEI$, with no $tEe$, and such that for every $yEI$ some $sEI$ has $tEs$ iff $(tEy\text{ or }t=y)$ for all $t\in M$. Extensionality makes this $s$ unique: any two choices have exactly the same $E$-members. Let $D=\{y\in M:yEI\}$. Separation forms $D$, which contains $e$, and the displayed unique-successor relation defines a total function $S:D\to D$ by Separation and Replacement. F3 yields an external sequence $x:\omega \to D$ with $x_0=e$ and $x_{n+1}=S(x_n)$. No sequence of arbitrary choices is taken.

For every $i<j<\omega$, $x_{i}E{x}_j$. To prove this, induct on $j$. There is nothing to check at $j=0$. At $j+1$, the successor clause gives $x_{j}E{x}_{j+1}$ via equality to $x_j$. If $i<j$, induction gives $x_{i}E{x}_j$, and the same clause gives $x_{i}E{x}_{j+1}$. These cases exhaust $i<j+1$.

If $i<j$ and $x_i=x_j$, step 2.1 would give $x_{i}E{x}_i$, contrary to step 1.1. Distinct naturals are comparable, so $i\mathrm{\ne }j$ implies $x_i\mathrm{\ne }{x}_j$. Thus $n\mapsto x_n$ is an injection $\omega \to D\subseteq M$, and $M$ cannot be finite: if a bijection $M\to n$ existed, its composition with the first $n+1$ sequence values would contradict F5. For each $n$, its first $n$ distinct values exhibit the finite lower bound $\mathrm{\mid }M\mathrm{\mid }\ge n$; at $n=0$ this is vacuous, and $x_0=e$ supplies the bound $1$.