Canonical copies of sets Sometimes one needs two disjoint copies of a given set $X$. This can be canonically done by taking $\{0\} × X$ and $\{1\} × X$. Sometimes we want to identify one of the copies with the original set $X$. So I wonder, is it possible to take a disjoint copy of $X$ straight ahead? And can this be done canonically? More precisely, are the following claims true?
$
\def\dom{\operatorname{dom}}
\def\rng{\operatorname{rng}}
\def\On{\mathbf{On}}
$


*

*For every $X$ there is a one-to-one function $f$ such that $\dom(f) = X$ and $\rng(X) ∩ X = ∅$.

*There is an explicit formula $φ(X, f)$ such that for every $X$ there is exactly one $f$ satisfying $φ(X, f)$ and this $f$ satisfies 1. for $X$.


Since such construction of a disjoint copy is intuitively trivial, I'm interested in proofs of 1. and 2. without using regularity, choice, or infinity.

Some ideas:


*

*We may simply put $f(x) := (x, X)$, but we need regularity to show that $(x, X) ∉ X$.

*We may consider $α = \sup(X ∩ \On)$ and pair members of $X$ with some ordinals above $α$, but we need AC to well-order $X$, and we need global choice to obtain 2.

*Let $<$ be the transitive hull of $∈$. If the relation $<$ is narrow, i.e. $\{y: y < x\}$ is a set for every $x$, then we may choose $z ∉ ⋃\{(\leftarrow, x)_<: x ∈ X\}$ and put $f(x) := (x, z)$ since $(x, z) = y ∈ X$ would imply $z < y$. Note that we don't need the axiom of infinity to define $<$, but I don't know how to prove its narrowness without infinity.

 A: With only Separation you can easily prove that $\{x\in X\mid x\notin x\}$ is a subset of $X$ which is not an element of $X$. Let $R_X$ be this set, and let $T_X$ be $R_{\operatorname{tcl}(X)}$.
Using that you can now proceed forward with $f(x)=(x,T_X)$ as your definition. And since $f$ now has a uniform and explicit definition, we also get (2). If transitive closures are not your thing, since they somewhat require Infinity, you can just take some finitely many unions from $X$, just to ensure that $T_X$ is not an element of any ordered pair inside $X$ or something like that. Your mileage may vary depending on how you coded ordered pairs.

For the suggestion using $\alpha$ as $\sup(X\cap\mathbf{On})$, you are certainly not using choice to well-order $X$, since well-ordering a set does not suddenly introduce or remove ordinals from it. And you also don't need global choice for choosing an ordinal, just take $\alpha+1$ (but you might want to replace $X$ by its transitive closure, anyway). So that option also works just peachy instead of $T_X$ above.
