Dedekind-infinite characterization ($\omega \hookrightarrow X⟺\exists g:X\hookrightarrow X\text{ nonsurjective}$)

In ZF, an injection $h:\omega \to X$ yields an injective nonsurjective self-map by shifting $h(n)$ to $h(n+1)$ and fixing the complement. Conversely, if an injection $g:X\to X$ omits $a$, the natural-number recursion theorem defines $h(n)=g^n(a)$. Any repetition would, after cancellation, put $a$ in the image of $g$. Thus $h$ is injective. The argument uses no axiom of choice, even when some infinite sets are Dedekind-finite sets.