A proof that a countable product of countable sets is non-empty that does not use the axiom of choice. Is the proof correct? Let $I$ be some non-empty set of indexes and for every $i \in I$ let $A_i$ be a set with cardinality $\aleph_0$.
Is the following proof that the cartesian product $\prod_{i \in I}A_i$ is non-empty valid without the axiom of choice?
By definition, since $|A_i| = \aleph_0$ for every $i \in I$, then there are bijections $f_i: \mathbb{N} \rightarrow A_i$ for every $i \in I$. Let’s define explicitly the function of choice $g: I \rightarrow \bigcup_{i \in I}A_i$ by: $g(i) = f_i(0)$. It’s clearly a function of choice, hence $\prod_{i \in I} A_i \ne \emptyset$. QED.
If it is valid, can it be generalized to any cartesian product of sets with equal cardinality? If it is not valid, why?
 A: There is absolutely no general way to pick a canonical bijection $f_i$. Sure, it's possible when all your sets are in fact sets of natural numbers or something. But in general, why would you prefer $f_0$ over a different bijection which maybe maps $f_i(0)$ to $f_i(1)$ and vice versa?
This is where you used the axiom of choice. You said that for all $i$, the set of bijections is non-empty, and therefore you can choose one from each of these sets, and that's how you got an element of the product.
Of course, it is consistent without the axiom of choice that a countable product of sets of size $2$ can be empty.
A: Your argument does invoke choice, albeit in a subtle way: when you choose a family of bijections $\{f_i: i\in I\}$. Just because, for each $i$, the set $F_i$ of bijections from $A_i$ to $\mathbb{N}$ is nonempty, doesn't mean that you can pick one for each $i$; this is exactly the axiom of choice applied to the family $\{F_i: i\in I\}$. In order to define $g(i)$, you need to refer to a specific $f_i$, so this use of choice is not easy to remove from your argument; and in fact it can be proved that the statement you are seeking to prove is not provable in ZF (= set theory without choice) alone. 
In fact, this holds in the most powerful way possible: even choice for families of two-element sets is not provable in ZF!
A: When you think you're defining g 'explicitly' , well, in fact you are not. You can do such 'explicit' definitions'  e.g. when you give an explicit formula on real numbers because you're manipulating only one or a few symbols (usually just 'x').
Here you're manipulating an arbitrary number of symbols $f_i$. Just because you think of them as indexed by i does not mean you really can refer to them all... until you have an axiom which says that you can do so. That's AC. It allows you to use an arbitrary number of symbols in that specific situation. In fact, it's more of a workaround than really using arbitrary number of symbols.
Remember that g is an object of set theory, which must be constructed using axioms. There's no such axiom as 'explicitly define a function'.
