= Solution
Here the <power set> notation gives $xEy\iff\mathcal P(x)\subseteq y$. Suppose a nonempty <set> $A$ has no $E$-minimal member. Form its <intersection> $b=\bigcap A$. This is a set: for any one $a_0\in A$, use the <axiom schema of separation> inside $a_0$ to define the elements common to all members of $A$. Selecting a single witness to nonemptiness is not an application of the <axiom of choice>.
For an arbitrary $y\in A$, lack of minimality supplies some $x\in A$ with $\mathcal P(x)\subseteq y$. Since $b\subseteq x$, every <subset> of $b$ is a subset of $x$, so
$$
\mathcal P(b)\subseteq\mathcal P(x)\subseteq y.
$$
This conclusion holds for each $y\in A$, without choosing all the corresponding $x$ simultaneously. Intersecting over $y$ gives $\mathcal P(b)\subseteq b$.
For completeness, the contradiction in <Cantor's theorem> is completely explicit here. By the <axiom schema of separation> put $d=\{u\in b:u\notin u\}$. Then $d\in\mathcal P(b)\subseteq b$, and consequently
$$
d\in d\quad\Longleftrightarrow\quad d\notin d,
$$
which is impossible. Thus no such $A$ exists:
$$
\boxed{E\text{ is well-founded, without Choice or Foundation}.}
$$
This <power-set-predecessor relation> proof uses neither a descending sequence nor a comparison of possibly non-well-orderable <cardinalities>. It proves <well-foundedness> directly from the minimal-member definition.
Back to article page