Given $S \hookrightarrow T$ construct $U ≈ T$ disjoint from $S$ in Z set theory?
I was recently thinking about the fact (in ZFC) that, given a (first-order) structure $A$ that embeds into another structure $B$, there is some structure $C$ isomorphic to $B$ such that the domain of $A$ is a subset of the domain of $C$. This is trivial if we can prove the following:
Given any injection from $S$ into $T$, there is some set $U$ disjoint from $S$ that bijects with $T$.
I can prove this within either ZC (using AC) or ZF (using Foundation). My ZC proof uses transfinite induction to pick $U$ out from $(P(T)×2)∖S$. My ZF proof constructs $U = \{ \{S,x\} : x∈T \}$. But I don't see a way to prove it within just Z. In one attempt, I tried to use one of $k$ disjoint copies of $T$ where $k$ is a well-ordered set that does not inject into $S$, but if every copy intersects $S$ then I seem to need a choice function on $S$ to obtain a contradiction. At least this means that I can prove it for countable $S$, but what about uncountable $S$?
I may be missing something easy, because intuitively it cannot be possible that every set that bijects with $T$ has a non-empty intersection with $S$, even in the absence of choice...
Well. Recall that in presence of Separation every set $A$ has a subset which is not an element of $A$. This is given by $\{a\in A\mid a\notin a\}$.
We can utilize a similar trick to get this disjoint copy. Fix your favorite method to code ordered pairs in $\sf Z$. Now consider $S'=\{x\in\operatorname{dom} S\mid x\notin x\}$, where $\operatorname{dom} S$ is the set of all left-coordinates of ordered pairs which are members of $S$.
By the usual argument, $S'$ is not in the domain of $S$. Now take $U=\{S'\}\times T$.