"First" in this case was just getting the first element of the iterator, it wasn't related to choosing a value from the set.

The Axiom of Choice is equivalent to the following:

1) "For any set A, there exists a function from non-empty elements of the power set of A to elements of A."

Which is equivalent to:

2) "There exists a function that takes a non-empty set as input, and returns an element of that set"

2 -> 1, since we can take the function 2 defines, and use it to define the function from 1.

1 -> 2 since we can define 2 as such:

For a set A, take the power set of A. Then take the function that 1 claims exists. Use that function to get an element of A, since A is an element of its power set.

But back to your core point:

But I agree that Iterator is a bad fit for the axiom of choice, since we have an (uncountable) number of sets to pick from.

Here's a way to phrase it programmatically that allows for uncountable sets-of-sets:

The axiom of choice claims that given a set of non-empty sets, you can construct a new set which contains an element from each of the sets.

pickOneFromEach :: Set (NonEmptySet a) -> NonEmptySet a

If you have a function:

choose :: NonEmptySet a -> a

And a function:

map :: (a -> b) -> Set a -> Set b

then you can define pickOneFromEach as follows:

pickOneFromEach setOfSets = map choose setOfSets