Where do I use finiteness in this proof of: In ZF, the compactness theorem implies the Axiom of Choice for collections of finite sets? Work in ZF, and assume the compactness theorem. Let $\mathsf{AC}^\text{fin}$ be the sentence "every collection of finite non-empty sets has a choice function".
UPDATE: Thank you to the helpful answerers. My proof below is invalid, and has been struck through to avoid confusing future generations of questioneers and maths students.
Here is my proof sketch of $\mathsf{Compactness} \vdash \mathsf{AC}^\text{fin}$: let $\phi_n$ be the sentence "every non-empty collection of $n$ finite sets has a choice function", for each $n\in\omega$. By induction, we show this holds for arbitrarily large finite collections of $\phi_n$s: if $n=0$, then $\varnothing$ is our choice function; if $n=k+1$ and the claim holds for $k$, then we can partition our collection into a $k$-size family and a singleton family, each of which have choice functions. Now we invoke compactness to extend it to the set of all $\phi_n$.
I'm not seeing where we used the finiteness of the individual sets, since each step seems to hold irregardless.
This post, though it names both "compactness" and "axiom of choice", seems not to be relevant.
This post, this post, and this post seem to be more about the act of choosing itself.
 A: Induction won't do you any good, because at the end of the day, nobody said anything about the family of finite sets being well-orderable. Nor would "choose from $n$ sets at once" is going to do you any good.
The "standard" approach is to first prove from compactness that every set can be linearly ordered, and then given a family of finite sets, $\cal A$, we linearly order $\bigcup\cal A$ and then each of these finite sets has a minimum which we can choose.
But, this is a fun exercise. So, how do we apply compactness directly? Well, let $\cal L$ be the language in which we have a predicate for each $A\in\cal A$ and a constant $c_a$ for each $a\in\bigcup\cal A$; and next we add axioms that state:

*

*$c_a\in A$ if and only if $a\in A$, for any $a\in\bigcup\cal A$ and $A\in\cal A$;

*The predicate $A$ has exactly $|A|$ elements, for any $A\in\cal A$; and

*$c_a\neq c_b$ for any pair of distinct $a,b\in\bigcup\cal A$.

Now, add a constant $c_A$ for each $A\in\cal A$ and an axiom stating that $c_A\in A$. This expanded theory is finitely satisfiable, so by compactness it is satisfiable. But since $A$ have exactly $n$ elements, we did not add any new elements to the predicate, so $c_A$ must be equal to some $c_a$ for $a\in A$, for any $A\in\cal A$. And this defines our choice function.
Here we see why we can only apply this logic to families of finite sets. If $A$ was not finite, we can only state, using first-order logic, that it is not finite. So compactness arguments may add "non-standard" elements to our sets $A$, which mean that we cannot use the $c_A$ constants to define an actual choice function.
