Suppose is an injection. Shift its image by defining
The two pieces have disjoint images, so is injective, but is omitted. Thus is not surjective.
Conversely, let be an injection which omits some . The natural-number recursion theorem defines , . If with , repeated injectivity cancels iterations and gives , putting in the image of , a contradiction. Hence is injective. Therefore
Choosing one witness from a single known nonempty set uses no axiom of choice. This is the Dedekind-infinite characterization.