= Dedekind-infinite characterization
{c}
{title2=$\omega\hookrightarrow X\iff\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>.
Back to article page
