The Cantor–Schroeder–Bernstein theorem says that the usual order relation on cardinalities of sets is antisymmetric. In other words, define an order on sets by $X \leq Y$ if there exists a monomorphism $f\colon X \to Y$. Then, if both $X \leq Y$ and $Y \leq X$, there exists an isomorphism of sets $X \cong Y$.
The result is really only interesting in the absence of the axiom of choice ($AC$). With $AC$, it is a trivial corollary of the well-ordering theorem. However, the theorem actually requires only excluded middle, although it does not hold in constructive mathematics.
We prove that the Cantor–Schroeder–Bernstein theorem holds in a Boolean topos. The theorem is not however intuitionistically valid, in that it fails in some toposes, such as the topos $Set^{\bullet \to \bullet}$ (the arrow category of $Set$); see Example 2 below.
Throughout we use ordinary set-theoretic reasoning which can be translated into the formal theory of toposes. (This can be formalized via the Mitchell–Benabou language, for instance.)
Let $f\colon P X \to P X$ be an order-preserving map. Then there exists $S$ in $P X$ for which $f(S) = S$.
Let $S$ be the (internal) intersection of $U = \{T \in P X : f(T) \leq T\}$. Since $S \leq T$ for every $T$ in $U$, we have $f(S) \leq f(T) \leq T$ for every $T$ in $U$. Hence $f(S) \leq S$ by definition of $S$. Applying $f$ again, we get $f f(S) \leq f(S)$. Hence $f(S)$ belongs to $U$. But then $S \leq f(S)$ by definition of $S$.
The preceding proof is valid in any topos (and so holds for $Set$ even intuitionistically). It can be seen as a special case of a result of Lambek on the initial algebra of an endofunctor.
Suppose given two monos $f\colon X \to Y$, $g\colon Y \to X$. Let $\exists_f\colon P X \to P Y$ denote existential quantification along $f$, and let $\neg_X\colon P X \to P X$ denote negation. Then the composite
is order-preserving, and so has a fixed point $S$ by the lemma. Now define $h\colon X \to Y$ by the rule
(the multi-line definition is where we use the Boolean condition). The second line makes sense because $\neg S$ is in the image of $g$. The inverse of $h$ is
That $j$ is inverse to h uses the fact that $\neg S = \exists_g \neg \exists_f(S)$. The rest is obvious.
This classic proof is substantially the proof given in Johnstone’s Elephant, D4.1.11. The Boolean condition is not strictly speaking necessary, i.e., the principle of excluded middle ($EM$) does not logically follow from the Cantor–Schroeder–Bernstein statement since, for example, the latter holds vacuously (every mono is an iso) in the non-Boolean topos
where $C$ is any nontrivial finite category. But $EM$ is certainly the most natural supposition to make.
Counterexample 4 below shows that the CSB theorem fails in Brouwer's intuitionistic mathematics even for $Set$ (since every function between the sets $[0, 1]$ and $\mathbb{R}$ must be continuous by Brouwer's continuity principle!). See also the discussion in Mac Lane-Moerdijk, VI.9, on toposes that realize Brouwer’s theorem.
As mentioned above, the Cantor-Schroeder-Bernstein theorem fails in the arrow category $Set^\to$, whose objects are functions $X_0 \to X_1$ between sets and whose morphisms are commutative squares. For example, let $X$ be the object $f: \mathbb{N} \to \mathbb{N}$ that takes $n \in \mathbb{N}$ to $\mathrm{int}(n/2)$, where $\mathrm{int}(x)$ is the greatest integer less than or equal to $x$; let $Y$ be the object $g: \mathbb{N} \to \mathbb{N}$ that takes $n$ to $\mathrm{Int}((n+1)/2)$, where $\mathrm{Int}(x)$ is the least integer greater than or equal to $x$. Pretty clearly $X$ and $Y$ are non-isomorphic, because $g^{-1}(0)$ has cardinality $1$ whereas all fibers of $f$ have cardinality $2$. But, just by drawing pictures of these objects, it is easy to construct monomophisms $i: X \to Y$ and $j: Y \to X$ (e.g., define $i_0(n) = n+1$ and $i_1(n) = n+1$ for all $n$, and define $j_0(n) = n+1$ for $n \gt 0$, $j_0(0) = 0$, and $j_1(n) = n$ for all $n$).
Nor can one have internal existence of an isomorphism between $X$ and $Y$ in this last example, since internal existence implies external existence as soon as the terminal object is (externally) projective.
The CSB property holds in many other categories of interest. For example:
The CSB property holds in the category of vector spaces and in the category of algebraically closed fields. See also this MO post, where model-theoretic criteria come into play, sometimes under strengthenings of the notion of monomorphism (e.g., elementary embedding, split monomorphism).
On the other hand, the CSB property fails in Top, since we have embeddings $\mathbb{R} \cong (0,1) \to [0,1] \to \mathbb{R}$, yet $[0,1] \ncong \mathbb{R}$.
More examples and discussion can be found at this Secret Blogging Seminar post.
In a celebrated work, Timothy Gowers gave a negative solution in the case of Banach spaces.
The CSB theorem was first stated by Georg Cantor, but his proof relied on the well-ordering theorem. The modern (choice-free) theorem was proved (independently) by Felix Bernstein? and Ernst Schröder?. It has been variously named after two or three of these in almost every possible combination, although Cantor (when mentioned at all) seems always to be mentioned first.
Wikipedia reports that Richard Dedekind had an (unpublished) proof in 1887, well before any announced proofs by Cantor, Schroeder, or Bernstein in 1895, 1896, 1897 respectively.
Peter Johnstone, Sketches of an Elephant: A Topos Theory Conpendium, Vol. I, Clarendon Press, Oxford (2002)
Timothy Gowers, A Solution to the Schroeder-Bernstein Problem for Banach Spaces, Bulletin of the London Mathematical Society, Volume 28, Issue 3 (1996), 297-304 (abstract)