I have read many related questions about wrong proof of Axiom of Choice(AC), especially this. I have the same problem like that. Then, I read Asaf's answer, something he metioned bothered me.
The first question: Is it true that we can only have finite application of EI(Existential Instantiation) in $\textbf{ZF}$.
The second question: I don't know what his means about this sentence
There is a family of finite sets indexed by $\textbf{X}$ which will not admit a choice function.
Is it a theroem in $\textbf{ZF}$?
The last question is about my explanation of wrong proof of AC after read his answer.My explanation is: we know that a function $f:X\rightarrow Y$ must declare which $y\in Y$ corresponds to $x\in X$. However, if for every non-empty sets $A\in \{\textbf{X}_\lambda\}_{\lambda\in I}$ contains at least two elements, by our definition, we can't get a function, since we actually don't know which elements $x\in A$ corresponds to $A$. But we can eliminate this problem in this sense:fix $x\in A$, and let $f(A)=x$, for finite family of sets, it is finite steps; for infinite family of sets, it is infinite steps, but a valid proof in $\textbf{ZF}$, we require it will terminate by finite steps(Is that so?). So, the method we used is vaild for finite family of sets, and not vaild for infinite family of sets.
I also consider an example $g(x)=x(x\in\mathbb{R})$, it seems like I defined $g$ with infinite steps like this: $g(1)=1, g(2)=2,...$, but by $g(x)=x$ we actucally for each $x\in\mathbb{R}$ have a exact real number correspond to $x$.It is different from the method we used in our wrong proff, because we can't say every $A$ have an exact element $x\in A$ correspond to $x$. We can just define step by step, however, it is infinite, which is not vaild proof in $\textbf{ZF}$. Is my understanding correct? Thanks for your answer!
The first question is yes, but it has nothing to do with $\sf ZF$ and everything to do with the fact that proofs are by definition finite. At least in the classical, first-order logic style setting. Since a proof is finite, we can only apply any inference rule finitely many times. In particular, we can only apply EI finitely many times.
For the second question, you're quoting only half the sentence.
In other words: (1) this is not provable from $\sf ZF$, so it is not a theorem, as it would outright disprove $\sf AC$; but (2) it is consistent, so it isn't even a theorem of $\sf ZF+\lnot AC$, but rather just a possible scenario.
Finally, it is possible to describe a choice function from some infinite families of non-empty sets. For example, $\{A\subseteq\mathbb R\mid |A|=1\}$ is an infinite family of non-empty sets, but we can easily describe a choice function: $F(\{a\})=a$.
It is also not accurate that this is just about an iterated application of EI. This will, of course, prove that $\{A_0,\dots,A_n\}$ admits a choice function. But we also need to contend with the possibility that our universe has non-standard integers. If you're not familiar with that, this is a minefield of conceptual difficulties that may exist, but the take from is this: it is certainly possible that there are "more natural numbers" inside the universe [of set theory] than outside. Since the concept of "finite" is internal to the universe of set theory, iterating EI will not be sufficient in that case, and we need to get a better result. However, luckily, $\sf ZF$ is a fairly strong theory, it proves an internal version of induction, so we can write the proof by induction where we apply EI only twice.