Why is AC needed to assert the existence of some infinite sets but not others? In my undergraduate review for topology, we use axiom of choice to prove a result about the surjectivity of projection mappings. I have also read through a number of posts about AC on the site, and have encountered it in a book on axiomatic set theory (though not in detail).
In particular, my takeaway from reading through various questions and sources is that it is essential when dealing with infinite sets to actually be sure the choice function $f$ exists. Particularly: Axiom of Choice: Where does my argument for proving the axiom of choice fail? Help me understand why this is an axiom, and not a theorem.. While I don't know the details from goblin's answer (why the statements are proveable/not proveable), I think I have appreciated the overall point that there is a fundamental difference between the two statements.
From the same question in the accepted answer by Asaf, he states:
"When you move from ∃∈
∃
s
∈
S
, to specifying "Let 
s
 be an element of 
S
" you are using what is known as existential instantiation. This is an inference rule of the underlying logic, stating that if there are objects satisfying some property, we can add a new symbol to the language with the statement that this symbol satisfies our property.
So you can apply it once, or twice, or thrice, and if you live long enough and all you do is apply it, then maybe even a few trillion times. Sure, all that is fun and games. But how can you apply it to each and every set of real numbers?"
I am not sure I fully comprehend what this means, but my current takeaway is that to construct the choice function would require an infinite number of steps in first order logic, something that is obviously not possible.
But my question then comes down to commonly used sets and definitions about cartesian products. For example consider the cartesian product on $\mathbb{R}$: $$\mathbb{R}^2 = \{(x,y) : x \in \mathbb{R} \wedge y \in \mathbb{R}\}$$ 
Why doesn't the issue of existence of this function apply as in cases where the axiom of choice is required? In particular, this is an infinite set, and it would not be possible to list out the contents of this set explicitly. What is the reason this is fundamentally different from explicitly listing out elements of sets in an indexed family? Similarly for functions such as $f = \{(x,y) \in \mathbb{R}^2 : x = y\}$.
How does this set-builder notation side-step the issue of requiring infinite first-order logic steps to specify the set, given that the sets themselves have an infinite number of elements? In other words, why is the existence of some infinite sets problematic, but not others?
My grasp on logic and set theory is very weak, so I am sure I have a major misunderstanding of the situation. I expect it may also not be possible for me to appreciate any answer without a lot more work on both, but I hope the question at least makes sense.
 A: Mathematics is not computation.
We are not "building everything one step at a time". You are given a universe, and you study the truths of that universe. Either from an axiomatic point of view (we assume something holds) or from an investigative point of view (we prove that something holds based on our assumptions).
The axioms of $\sf ZF$ provide us with fairly straightforward recipes that encapsulates our intuition. For example, if $A$ is a set, then we can collect all of its subsets into another set, the power set of $A$. The idea is that this is useful, because this is how we think about mathematics. If we have a reasonable property, then we want this reasonable property to define a set. Naively that meant every property, but we know that's impossible due to the many paradoxes of naive set theory.
But it turns out that for the power set axiom, and so on, these paradoxes do not hold. So we assume these axioms are true.
So when we write $\Bbb R^2=\{(a,b)\mid a,b\in\Bbb R\}$, we are not trying to compute this set one element at a time. This collection is given by a property, and we can now prove that this collection is indeed a set (which one depends on how you interpret $\Bbb R$ and $(a,b)$ as sets, of course).
On the other hand, the Axiom of Choice is an axiom that does not provide us with a descriptive construction of a set. It says, "trust me, I've checked, there's a set that does this thing". But without an explicit description we can't really apply our Separation or Replacement axioms. We just have to contend with the fact that the set we want exists.
Now, we have experience with things existing without a description. When I say "let $x\in X$" I did not provide you with any description of $x$, just with the fact that it lies in $X$. Sometimes it's enough to know exactly what is $x$, but in general, there is no telling which element of $X$ this might be. Here we are not invoking the Axiom of Choice, but rather the rules of logic: existential instantiation.
Naively people try to prove the Axiom of Choice by reversing the quantifiers: if $X=\{X_i\mid i\in I\}$ is family of non-empty sets, then pick some $X_i\in X$, and pick some $x_i\in X_i$, and we have a choice function! But there is no rule letting us move from choosing one element of one set, to choosing one element of every set.
This is really what you'd do in the finite case, from the naive point of view as well. If I tell you that $A,B,C$ are non-empty sets, you're not going to immediately jump to a choice function. You're going to choose some $a\in A$, then some $b\in B$, and then some $c\in C$. You're going to do it "by hand".
When you collection of sets is finite, that's fine and dandy. But when the collection is infinite, this does not fit into a finitary proof anymore. It's just not going to work. Which is why we need the Axiom of Choice.
