"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