**Deep Choice**:
$\forall X \ [\forall a,b \in X \, ( a \neq \emptyset \land (a \neq b \to a \cap b = \emptyset)) \to \\ \exists Y \exists f \,(f: X \rightarrowtail Y \land \forall x \in X \,( f(x) \in \operatorname {tc}(x)))]$


In English: for every family $X$ of pairwise disjoint nonempty sets, there is an injective function that sends each element $x$ of $X$ to an element of the transitive closure of $x$.


Denote this principle “$\mathsf{DpC}$”.


Is the following true?



> 
> $(\mathsf{ZF} + \mathsf{DpC}) \to \mathsf{AC}$.
> 
> 
> 



Can Deep Choice entail Axiom of Choice?
It proves AC. For this, recall it's enough to see that for every ordinal $\alpha$, $\mathcal{P}(\alpha)$ is wellorderable, and for that it's enough to see that $\mathcal{P}(\mathcal{P}(\alpha))\backslash\{\emptyset\}$ has a choice function. Supposing this fails for some $\alpha$, let $\alpha$ be the least such; then $\alpha$ is an infinite cardinal. Let $\pi:3\times\alpha\to\alpha$ be a bijection. Let $\pi^+:\mathcal{P}(\alpha)^3\to\mathcal{P}(\alpha)$ be the induced bijection, i.e. $$\pi^+(x,y,z)=\pi[x]\cup\pi[\alpha+y]\cup\pi[2\times\alpha+z],$$ where $\alpha+y=\{\alpha+\beta\bigm|\beta\in y\}$ etc. Now for $x\in\mathcal{P}(\alpha)$ and $X\in\mathcal{P}(\mathcal{P}(\alpha))$ and $z\in\mathcal{P}(\alpha)$ define $(x,X,z)^\*\in\mathcal{P}(\mathcal{P}(\alpha))$ by $$ (x,X,z)^\*=\{\pi^+(x,y,z)\bigm|y\in X\}.$$
Clearly $(x,X,z)\mapsto(x,X,z)^\*$ is injective in all 3 arguments $x,X,z$. For $x\in\mathcal{P}(\alpha)$ and $X\in\mathcal{P}(\mathcal{P}(\alpha))$ let
$$(x,X)^{\*\*}=\{(x,X,z)^\*\bigm|z\in X\}.$$


Note that if $X,Y\in\mathcal{P}(\mathcal{P}(\alpha))$ and $x,y\in\mathcal{P}(\alpha)$ with $(x,X)\neq(y,Y)$ then $(x,X)^{\*\*}\cap(y,Y)^{\*\*}=\emptyset$.
Also if $X\in\mathcal{P}(\mathcal{P}(\alpha))\backslash\{\emptyset\}$ then $(x,X)^{\*\*}\neq\emptyset$.


Now let $$P=\Big\{(x,X)^{\*\*}\Bigm|x\in\mathcal{P}(\alpha)\wedge X\in\mathcal{P}(\mathcal{P}(\alpha))\backslash\{\emptyset\}\Big\}.$$


So by the remarks above, we can apply Deep Choice to the family $P$. Let $f:P\to V$ be an injection witnessing this.


I claim that for some $x\in\mathcal{P}(\alpha)$, we have $f((x,X)^{\*\*})\notin\alpha$ for all $X\in\mathcal{P}(\mathcal{P}(\alpha))\backslash\{\emptyset\}$. Otherwise, let $\beta\_x$ be the least $\beta$ of form $f((x,X)^{\*\*})$ for some such $X$; then $x\mapsto\beta\_x$ is injective with domain $\mathcal{P}(\alpha)$, so $\mathcal{P}(\alpha)$ is wellorderable, contradiction.


Fix $x$ witnessing the claim. Then note that for each $X\in\mathcal{P}(\mathcal{P}(\alpha))\backslash\{\emptyset\}$, either


* (i) $f((x,X)^{\*\*})=(x,X,z)^\*$ for some $z\in X$, or
* (ii) $f((x,X)^{\*\*})=\pi^+(x,y,z)$ for some $y,z\in X$


(this is because the only other options are further down in the transitive closure of $(x,X)^{\*\*}$, but such objects are in the transitive closure of some $\pi^+(x,y,z)$, but these are only ordinals ${<\alpha}$, which have been ruled out already).


But now we can define a choice function $c$ for $\mathcal{P}(\mathcal{P}(\alpha))\backslash\{\emptyset\}$: given $X\in\mathcal{P}(\mathcal{P}(\alpha))\backslash\{\emptyset\}$, let $c(X)=$ the unique $z\in X$ witnessing (i), if (i) holds; or if (i) is false, then let $c(X)=$ the unique $z\in X$ witnessing (ii). The existence of $c$ contradicts our hypothesis.


