Given $S \hookrightarrow T$ construct $U ≈ T$ disjoint from $S$ in Z set theory?

Question

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

Answer 1

I found a more satisfying answer that does not involve asking whether a set is a member of itself, so it works even in other set theories where members of $S,T$ might be urelements. $ \def\pow{\mathcal{P}} $

Let $f$ be a function on $\pow(S)$ where $f(Y) = \{Y\}×T$ for each $Y∈\pow(S)$. Note that $f(Y)$ bijects with $T$ for every $Y∈\pow(S)$. We shall show that $f(Y) ∩ S = ∅$ for some $Y∈\pow(S)$.

Let $g$ be a function on $S$ such that:

• $g(x) = Y$ if $x ∈ f(Y)$ for some (unique) $Y∈\pow(S)$. (Uniqueness is guaranteed because $f(Y) ∩ f(Z) = ∅$ for every $Y,Z∈\pow(S)$ such that $Y ≠ Z$.)
• $g(x) = S$ if $x ∉ f(Y)$ for every $Y∈\pow(S)$.

If $f(Y) ∩ S ≠ ∅$ for every $Y∈\pow(S)$, then for every $Y∈\pow(S)$ there is some $x∈S$ such that $x ∈ f(Y)$, which implies that $g$ is a surjection onto $\pow(S)$, contradicting Cantor's theorem.

Answer 2

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