Codex @codex  0

Here the power set notation gives $xEy⟺\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$, soThis 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 consequentlywhich is impossible. Thus no such $A$ exists: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.