Wikipedia wrote:A choice function is a function f, defined on a collection X of nonempty sets, such that for every set s in X, f(s) is an element of s. With this concept, the axiom can be stated:

For any set of non-empty sets, X, there exists a choice function f defined on X.

Thus the negation of the axiom of choice states that there exists a set of nonempty sets which has no choice function.

Each choice function on a collection X of nonempty sets can be viewed as (or identified with) an element of the Cartesian product of the sets in X. This leads to an equivalent statement of the axiom of choice:

An arbitrary Cartesian product of non-empty sets is non-empty.

Not once in that article are there any references to attempted proofs of this "axiom", which I find astounding. Thus, I attempt to do so now:

Everyone knows that the size of a Cartesian product is the product of the size of the sets in the product, right? I shouldn't need to prove that one, but it's an easy induction. Now, since the size of a set is a natural number, we can trivially prove the AoC, since within the naturals, the product of two (or more, by extension) numbers is zero iff at least one of them is zero to begin with. Finally, in case there's any doubt that those two statements of the AoC are indeed equivalent, i.e. how to identify choice functions with tuples in the Cartesian product: you can create a relation from each set in X to each element of one of the Cartesian tuples, and that relation is in fact a function, because we constructed its domain from a set X, and thus it can contain no duplicates, making one-to-many impossible (although it may be many-to-one, since its range is a tuple).

Why, then, are we still calling it an axiom? I think I know why: because mathematicians are lazy, and don't want to be bothered with the idea that there may be a set of sets for which no choice function is definable, even if many may exist. So, if we call it an axiom, we can just ignore it wherever it makes things too complicated for our poor little brains. First of all, I think it's baloney, since a choice function would only be undefinable over X if X itself was not well-defined enough. Second, if it's really too much hassle, you can just ignore the theorem, but you don't have to call a theorem an axiom and point to Gödel when questioned just to get your way. You miss out on a lot of other interesting things.