The class of well-founded sets satisfies the axiom of foundation and the axiom of choice

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?

• Where you wrote "a family of non-empty well-ordered sets" did you mean "a family of non-empty well-founded sets"? – Michael Hardy Feb 8 '17 at 4:07
• And instead of a family of well-founded sets, might you need a well-founded set of well-founded sets? – Michael Hardy Feb 8 '17 at 4:08
• So $(W_i)_{i\in I}$ is a well-founded family of well-founded sets, and the axiom of choice says there is some set that is a function assigning to each value of $i$ a member of $W_i$, and you'd need to prove that that set is itself well-founded. – Michael Hardy Feb 8 '17 at 4:27
• BTW, an occurrence of the concept in the world in which non-mathematicians live is when the Catholic Church and the Eastern Orthodox Church claim their episcopates are well-founded. I.e. you're not a validly ordained bishop unless either you're one of the original apostles or you were validly ordained a bishop by someone who was already a bishop. – Michael Hardy Feb 8 '17 at 4:32
• @MichaelHardy Yes, I meant to write "well-founded" instead of "well-ordered". I've edited my post. And yes, the index set is also well-founded in this case. – Jacob Errington Feb 8 '17 at 15:36

Doesn't this proof use the axiom of choice, namely in selecting the member $y$ of minimal rank?

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.

Is this proof okay?

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.)

• I see. So the ambient axiom of choice tells us that the choice function exists, but the (graph of) this function might not be a well-founded set. To see that it is, is it enough to say that the graph of the function is simply a subset of the cartesian product of the domain and the codomain? The index set is well-founded by assumption and the union of the sets in the family is also well-founded. Their product is well-founded. (Since the rank is simply the maximum of the ranks of the components in the product.) – Jacob Errington Feb 8 '17 at 3:52
• The axiom of choice actually says that in each instance in which it is applied, a certain set exists. For the axiom of choice to be true in a particular model, that set would have to be a member of that model. – Michael Hardy Feb 8 '17 at 4:25
• @MichaelHardy Yes, the OP should be looking at a well-founded set of well-founded sets. – Noah Schweber Feb 8 '17 at 4:28