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.
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.