Schroeder - Bernstein Theorem's proof I'm trying to understand a proof about this theorem:

Suposse that there exist a inyective function from the set $A$ into $B$ and an injective function from $B$ into $A$. Then $A\cong B$.

proof:
The first injection lead to an identification $B\cong C\uplus A$ for some set $C$, while the second leads to an identification $A\cong C\uplus B$. Iterating this we can conclude that 
$$A\cong C\uplus D\uplus C\uplus D\uplus\cdots \uplus X  $$
and
$$B\cong D\uplus C\uplus D\uplus C\uplus\cdots \uplus X  $$
for some set $X$. Since $C\uplus D\cong D\uplus C$ we can conclude that $A\cong B$.
How can be the "iteration" formalize? 
I do not understand why the set $X$ appears. It is confusing to me the central part of the proof. Any comment? 
Thanks! 
 A: This is probably much longer and uglier than it needs to be, but I kind of fail at shortening it right now.
You can construct $X$ as follows: Let $f \colon A \to B$ and $g \colon B \to A$ be injective, set
$$
 h = g \circ f \colon A \to A
 \quad\text{and}\quad
 k = f \circ g \colon B \to B,
$$
both of which are injective. Then set
$$
 X = \bigcap_{n \geq 0} h^n(A)
 \quad\text{and}\quad
 Y = \bigcap_{n \geq 0} k^n(A).
$$
Notice that
$$
 A = h^0(A) \supseteq h^1(A) \supseteq h^2(A) \supseteq \dotso
$$
and
$$
 B = k^0(A) \supseteq k^1(A) \supseteq k^2(A) \supseteq \dotso
$$
are descreasing sequences, so $X = \bigcap_{n \geq m} h^n(A)$ and $Y= \bigcap_{n \geq m} k^m(B)$ for every $m \geq 0$.
For every $n \geq 0$ we have
$$
 f \circ h^n
 = f \underbrace{(g f) \dotsm (g f)}_n
 = \underbrace{(f g) \dotsm (f g)}_n f
 = k^n \circ f.
$$
Therefore
$$
 f(X)
= f\left( \bigcap_{n \geq 1} h^n(A) \right)
= \bigcap_{n \geq 0}  f(h^n(A))
= \bigcap_{n \geq 0} k^n(f(A)).
$$
Because
$$
 \bigcap_{n \geq 0} k^n(f(A))
 \subseteq \bigcap_{n \geq 0} k^n(B)
 = Y
$$
and
$$
 \bigcap_{n \geq 0} k^n(f(A))
 \supseteq \bigcap_{n \geq 0} k^n(f(g(B)))
 = \bigcap_{n \geq 0} k^{n+1}(B)
 = \bigcap_{n \geq 1} k^n(B)
 = Y
$$
it follows that $f(X) = Y$. Similary $g(Y) = X$.
Also notice that
$$
 (g \circ f)(X)
 = h(X)
 = h\left( \bigcap_{n \geq 0} h^n(A) \right)
 = \bigcap_{n \geq 0} h^{n+1}(A)
 = \bigcap_{n \geq 1} h^n(A)
 = X
$$
and similarly $(f \circ g)(Y) = Y$. So $f$ maps $X = g(Y)$ bijectively into $f(X) = f(g(Y)) = Y$, and the inverse is given by $g$ mapping $Y$ bijectively into $X$.
Now let $C = g(B)^C$ and $D = f(A)^C$, i.e. $A = C \uplus g(B)$ and $B = D \uplus f(A)$. Then
$$
 A
 = C \uplus g(B)
 = C \uplus g(D) \uplus g(f(A))
 = C \uplus g(D) \uplus h(A)
$$
By inserting the left side of the above equation into the right side we find inductively that
$$
 A = \left(
  \biguplus_{i=0}^n h^i(C) \uplus h^i(g(D))
 \right)
 \uplus h^{n+1}(A)
$$
for all $n \geq 0$. In particular we have that
$$
 X'
 = \bigcup_{n \geq 0} h^n(C) \cup h^n(g(D))
 = \biguplus_{n \geq 0} h^n(C) \uplus h^n(g(D)).
$$
Notice that
\begin{align*}
 (X')^C
 &= \left( \bigcup_{n \geq 0} h^n(C) \cup h^n(g(D)) \right)^C
 = \left( \bigcup_{n \geq 0} \bigcup_{i=0}^n h^i(C) \cup h^i(g(D)) \right)^C \\
 &= \bigcap_{n \geq 0} \left( \bigcup_{i=0}^n h^i(C) \cup h^i(g(D)) \right)^C
 = \bigcap_{n \geq 0} h^{n+1}(A)
 = X.
\end{align*}
Thus we have a decomposition
$$
 A
 = X' \uplus X
 = \biguplus_{n \geq 0} h^n(C) \uplus h^n(g(D)) \uplus X.
$$
Similary we have a decomposition
$$
 B
 = Y' \uplus Y
 = \biguplus_{n \geq 0} k^n(D) \uplus k^n(f(C)) \uplus Y.
$$
where
$$
 Y'
 = \bigcup_{n \geq 0} k^n(D) \cup k^n(f(C))
 = \biguplus_{n \geq 0} k^n(D) \uplus k^n(f(C)).
$$
We now have $h^n(C) \cong C \cong f(C) \cong k^n(f(C))$ and similar $k^n(D) \cong h^n(g(D))$ for all $n \geq 0$, as well as $X \cong Y$. Combining these we get that $A \cong B$.
It is maybe interesting to notice that in this proof we used a limit-like approach, i.e. we first approximate the wanted partitions of $A$ and $B$ and then we take a limit by intersections. Just like in analysis we can replace approximations by describing functions as solutions to fitting equations we can replace the above construction by using fix point theorems. For example Bredon’s Topology and Geometry, Appendix B features a very nice proof of the theorem by using some nice statements about the existence of fixpoints of monotone functions on complete lattices (e.g. power sets).
