I am reading a book on NBG (von Neumann-Barnays-Godel set theory) by Taras Banakh (https://arxiv.org/abs/2006.01613) and I encountered on page 26 well-founded relations. In this book, a relation $R$ is well-founded if every nonempty class $X$ contains an element $x\in X$ such that $\overleftarrow{R}(x)\cap X=\emptyset$. Here, $\overleftarrow R(x)$ is the initial $R$-interval of $x$ defined as $\overleftarrow R(x)=\{z\mid (z,x)\in R\}\backslash\{x\}$.
I want to prove that the membership relation $\mathbf E=\{(x,y)\mid x\in y\}$ is well-founded without using the axiom of choice. The axiom of foundation as worded in this book is
$$\forall x\in\mathbf U\,(x\ne\emptyset\implies\exists y\in x\,\forall z\in y\,(z\notin x)).$$
I managed to prove that $\mathbf E$ is well-founded, but I had to assume both the axiom of choice and the axiom of foundation. A sketch of that proof is as follows.
Under the axiom of foundation, for every $x\in\mathbf U$ we have $\overleftarrow{\mathbf E}(x)=x$. Assume $\mathbf E$ is not well-founded. Then there is a class $X$ such that for every $x\in X$, there is $y\in x\cap X$. Define a function $f:X\to\mathbf U$ such that for each $x\in X$, we choose $f(x)\in x\cap X$. Then we create a sequence $x_n$ such that for each $n\in\mathbb N$ we have $x_{n+1}\in x_n$. Then the set $\{x_n\mid n\in\mathbb N\}$ will fail the axiom of foundation, so we have a contradiction.
I had some ideas on proving this without the axiom of choice by using the following proposition for the subset relation (the proposition in the book right after the definition of a well-founded relation states that a transitive set-like relation is well-founded if and only if every nonempty set $a\subseteq\text{rng}[R]$ contains an element $y\in a$ such that $\overleftarrow R(y)\cap y=\emptyset$, but I didn't manage to do this.
Is there a way to do this without assuming the axiom of choice? I have no trouble assuming it, but the name "well-founded" makes me think that it is a generalized statement of the axiom of foundation, but for every relation. So if we have to assume the axiom of choice for it, then the name doesn't quite capture its intent from what I can understand.
EDIT: Scanning the book above further along, I see that there is a very difficult proof of this fact without using the axiom of choice. It involves defining the von Neumann universe $\mathbf V$ and proving that $\mathbf E\cap(\mathbf V\cap\mathbf V)$ is well-founded, and then proving that $\mathbf V=\mathbf U$. I will study this approach, but I would still like to see if anyone has a less convoluted proof.
Best Answer
Of course we don't need the axiom of choice. In fact, there is nothing to prove.
Since you are considering $\bf E$ to be a class of ordered pairs, you are implicitly requiring that both $x$ and $y$ are sets, i.e. members of $\bf U$, otherwise they cannot be elements of an ordered pair.
Moreover, since $\overleftarrow{\bf E}(x)=x$ follows immediately from the Axiom of Extensionality, the Axiom of Foundation just tells you that $\bf E$ is well-founded.
To prove that $\in$ is also well-founded on classes, suppose that $X$ is a class, note that if $X$ is a set, then we have nothing to check, so we can assume it is a proper class, and so it is also non-empty.
Next, let $x_0\in X$ be some set, and now define $x_{n+1}=\bigcup x_n\cap X$, then $x_{n+1}$ is a set, by Union and Separation, and by Replacement, $\{x_n\mid n<\omega\}$ is also a set. Let $x=\bigcup\{x_n\mid n<\omega\}$, then it is a set, $x\subseteq X$, and so we have two options:
$x=\varnothing$, in which case we have that $x_0\subseteq x$, so $x_0=\varnothing$, so $x_0\cap X=\varnothing$.
Otherwise, by Foundation, there is some $y\in x$ such that $y\cap x=\varnothing$. However, if $y\in x$, then $y\in X$, and moreover, since $y\in x$ means $y\in x_n$ for some $n$, if $z\in y\cap X$, then $z\in x_{n+1}$. Therefore, since $y\cap x=\varnothing$, it must be that $y\cap X=\varnothing$ as well.
In either case, we found an element of $X$ which is disjoint from it.
Alternatively, you can just prove that assuming $\sf NBG$, we can write $\bf U$ as the union of its von Neumann hierarchy, $\{V_\alpha\mid\alpha\in\rm Ord\}$, so if $X$ is a proper class, there is a least $\alpha$ such that $X\cap V_\alpha$ is non-empty, and by minimality, any member of that intersection must be disjoint from $X$.