I'm trying to. understand the proof in Halmos's book of the Schröder-Bernstein theorem. Here is my best attempt to replicate it.
Statement: If there exist injections $f: X \to Y$ and $g: Y \to X$, then there is a bijection $h: X \to Y$.
Let $f: X \hookrightarrow Y$ and $g: Y \hookrightarrow X$ be injections. Without loss of generality, assume $X \cap Y = \emptyset$. If not, we replace $X$ and $Y'$ with isomorphic copies $X', Y'$ with $X' \cap Y' = \emptyset$. If $f: X \to Y$ is surjective, $f$ is bijective and we have $|X| = |Y|$. If $g: Y \to X$ is surjective, then there exists $g^{-1} : X \to Y$ which is bijective. We proceed under the assumption that neither $f$ nor $g$ are surjective. We call $x \in X$ the parent of the element $f(x) \in Y$, and $y \in Y$ the parent if $g(y) \in X$. Each element $x \in X$ has an infinite sequence of descendants, $$f(x), g(f(x)), f(g(f(x)), \ldots,$$ as does each $y \in Y$, $$g(y), f(g(y)), g(f(g(y))), \ldots $$ Each term in these sequences is, by construction, a descendant of all preceding terms and an \emph{ancestor} of all following terms. For each element in $X \cup Y$, we have three mutually exclusive and exhaustive possibilities. First, an element $x \in X$ may have no parent in $Y$, i.e., $x \neq g(y)$ for any $y \in Y$, so we have $x \in X - g(Y)$. We call such an $x$ an \emph{orphan}. Second, an element $y \in Y$ may have no parent in $X$, i.e., we have $y \neq f(x)$ for any $x \in X$, so we have $y \in Y - f(X)$. Third, the lineage may regress infinitely.
Define $X_X$ to be the set of elements $x \in X - g(Y)$ and their descendants in $X$. Let $X_Y$ be the set of elements of descendants in $X$ of the elements of $Y - f(X)$. Let $X_{\infty}$ be the set of elements of $X$ without a parentless ancestor. So $X = X_X \sqcup X_Y \sqcup X_{\infty}$. Similarly, let $Y_X$ as the descendants in $Y$ of the elements in $X - f(X)$, let $Y_Y$ be the set of elements in $Y - g(Y)$ and their descendants in $Y$, and let $Y_{\infty}$ be the set of elements of $Y$ with no parentless ancestor. So $Y = Y_X \sqcup Y_Y \sqcup Y_{\infty}$.
Notice that, by definition, $Y_X$ consists of the descendents in $Y$ of all $x \in X_X$. So if $x \in X_X$, we have $f(x) \in Y_X$. Furthermore, $f$ is injective, so if $x \neq x'$ in $X_X$, there is exactly one corresponding element in $Y_X$. Furthermore, each element in $Y_X$ is the parent of exactly one child $x \in X_X$. So the restriction $f \mid_{X_X} : X_X \to Y_X$ is a bijection.
Second, if $x \in X_Y$, then $x$ is a descendant of an element $y \in Y - g(Y)$. That is, $x = g(y)$ for some $y \in Y_Y$. We then have $g^{-1} (x) = y \in Y_Y$, where $g^{-1}$ is the left inverse $Y \to X$, the existence of which is guaranteed by virtue of the fact that $g$ is injective. I claim that $g^{-1} \mid_{X_Y}: X_Y \to Y_Y$ is a bijection. First, we have $g^{-1} \circ g = \mathrm{Id}_Y$, $g$ is a right inverse of $g^{-1}$, so $g^{-1}$ is surjective. Furthermore, given $a,b \in X_Y$, assume $g^{-1} (a) = g^{-1} (b)$. By the definition of $X_Y$, we have $a = g(s)$ and $b = g(t)$ for some $s,t \in Y$. So $g^{-1} (g(s)) = g^{-1} (g(t))$, so $s = t$. As $g$ is a well-defined function $g(s) = g(t)$, so $a = b$, so $g^{-1}$ is a bijection.
Finally, if $x \in X_{\infty}$, then its lineage regressed as infinitum, so we must have $x \in Y_{\infty}$. I claim that $f \mid_{X_{\infty}} : X_{\infty} \to Y_{\infty}$ is a bijection. Given $y \in Y_{\infty}$, there must exist a parent $x \in X_{\infty}$. Furthermore, given $a,b \in X_{\infty}$ for which $f(a) = f(b)$, we have $a = b$ since $f$ is injective.
Therefore, we define the map $\varphi: X \to Y$ by $$\varphi(x) = \begin{cases} f(x), \; & \text{ if $x \in X_X \cup X_{\infty}$} \\ g^{-1} (x), \; & \text{ if $x \in X_Y$} \end{cases} $$ Since $f_{X_X}: X_X \to Y_X$, $g_{-1}: X_Y \to Y_Y$, and $f \mid _{X_{\infty}}: X_{\infty} \to Y_{\infty}$ are bijections, $\varphi$ is a bijection $X \to Y$, so we have $|X| = |Y|$, as desired.
How does this proof look? Have I missed anything?
