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}$.
Best Answer
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
(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.