I'm reviewing a theorem we saw in class.
The class $WF$ satisfies the axiom of foundation. Furthermore, if the axiom of choice is true, then $WF$ satisfies the axiom of choice.
$WF$ here is such that for any element $x \in WF$, there is a least ordinal $\alpha$ such that $x \in V_\alpha$ where $V_\alpha$ is a set in the von Neumann hierarchy.
The first part of the proof is this.
Suppose $x \in WF$ is nonempty. Let $y$ be a member of $x$ of minimal rank. Suppose $z \in x \cap y$. Then $z \in x$, but $\operatorname{rank} z < \operatorname{rank} y$; this contradicts the minimality of the rank of $y$.
Doesn't this proof use the axiom of choice, namely in selecting the member $y$ of minimal rank? Otherwise, this proves that for all $y \in x$ of minimal rank we reach a contradiction. Eliminating this "for all" would require the axiom of choice, no?
Note that this part of the proof given by my professor. The proof of satisfaction of the axiom of choice was left as an exercise. Here is what I came up with.
Suppose $(W_i)_{i \in I}$ is a well-founded family of non-empty well-founded sets. Each has some elements of minimal rank. Choose one of them. This identifies unique element in each $W_i$. Applying the axiom of replacement forms a set $(w_i)_{i \in I}$ such for all $i \in I$, $w_i \in W_i$.
Is this proof okay?
No. Basically, choice is not needed to make a single choice, but rather a collection of choices: if $A$ is nonempty, I can always say "let $a\in A$" in a proof. The only difficulty comes when I want to make lots of choices at once, that is, assert the existence of a choice function $f:I\rightarrow\bigcup_{i\in I}A_i$ with $f(i)\in A_i$ for a large index set $I$. There are a few questions on this site which address this issue in more detail, e.g. this one.
Not really. When you write "Choose one of them," you're hiding some work that's worth doing explicitly; this goes back to my previous point. You need to make a lot of choices simultaneously here, so how are you going to do it? The point is that you will use the Axiom of Choice to show that a choice function $f$ exists.
But more importantly, that only gets you partway: you need to argue that a choice function $f$ exists, and then argue that this $f$ is in fact already in $WF$. The axiom of choice does this first bit immediately (do you see why?), so the real meat of the problem is: show that any resulting choice function is itself a member of $WF$. This is not hard to do, but you haven't done it.
(Also, the axiom (scheme) of replacement won't play a role here.)