This isn't a direct answer to the question, but a way to think about the axiom of choice.
The axiom of choice is a generalization of finiteness. It's related (by, for instance, the compactness theorem in logic, and Tychonoff's theorem in topology) to topological compactness, which is another generalization of finiteness.
Without the axiom of choice, you can sometimes specify a choice: "Pick the left shoe from each pair." If you can make (read: define) such a specification, you don't need the axiom of choice, because you can point to that specification as your choice.
Consider how each equivalent definition of Choice is true in the finite setting:
- "Every finite product of non-empty sets has at least one element."
If you're given a few sets, you can select one from each, one step at a time. (If you have an infinite number of sets, you'd need an infinite number of steps.)
- "Every finite set can be well-ordered."
If you pull elements out one at a time, that's a well-ordering. (Again, you'd need an infinite number of steps for an infinite set.)
- "Every finite vector space has a basis."
Choose a non-zero vector. Then take a vector not in the linear subspace generated by the first vector. Then take a vector not in the span of the first two vectors. Eventually, you'll run out of vectors.
- "Every two finite cardinals are comparable."
Count up from 0 until you get to the first one. That's the smaller one. If you get to both at once, they're equal.
In an informal sense, the axiom of choice says you can always take an infinite number of (certain kinds of) steps in finite time. And you can only follow a statement/proof that takes finite time to read. The axiom of choice is also non-constructive: you can't use it to make a "real" example, because you'd need infinite construction time.
More on finiteness and statements:
Let $X = X_0 \times X_1 \times X_2 \times \dots$ be a product of sets. Then the axiom of choice says
$$\exists x_0 \in X_0 \ \exists x_1 \in X_1 \ \exists x_2 \in X_2 \ \exists \dots \ \text{s.t.} (x_0, x_1,x_2, \dots) \in X$$
But the first ellipsis doesn't actually make sense in logic. No mathematical logic rules allow an infinite number of quantifiers. The axiom of choice sort of says, "That's okay, it still works."
On the other hand, you can define the "left shoe" choice with only a finite number of quantifiers. Let $I$ be the index set for the product. Then
$$\{\text{left}_i \in X_i | i \in I\} \in X$$
is a choice of all the left shoes, with one implicit quantifier over the index set.