[Math] Finite axiom of choice: how do you prove it from just ZF

axiom-of-choicelo.logicset-theory

The axiom of choice asserts the existence of a choice function for any family of sets F. Suppose, however, that F is finite, or even that F just has one set. Then how do we prove the existence of a choice function?

The usual answer is that we just go from set to set, picking an element from each set. Since F is finite, this process will terminate. What I'm really wondering is how we can always choose from a single set. The informal answer seems to be just that it's possible… but this isn't an axiom, so it must be justified some other way.

So: how do you prove from the axioms of just ZF without choice, that for any nonempty x there exists a function f:{x}->x?

Best Answer

Although the answers already given are correct, let me add some information (essentially just rephrasing the bracketed part of Thomas Scanlon's answer) that I've found useful for students who raised this question. Consider the problem, at the end of the original question, of "choosing" from a single set $x$. As several people have pointed out, we are given the existential statement, "There is an element in $x$." What should be noticed in addition is that what we want to prove is also an existential statement, "There is a choice function." We have an explicit construction, which I'll call $C$, that will convert any element of $x$ into a choice function, namely sending any $y$ to $\{(x,y)\}$ (as in Charles Staats's comment on the original question). If we can't explicitly define any particular $y$, then we won't be able to define any particular choice function either, but the problem doesn't require us to explicitly define a choice function; we need only prove that one exists. And that follows, thanks to $C$, from the existence of elements in $x$.