Cantor-Schröder-Bernstein theorem (source code)

= Cantor-Schröder-Bernstein theorem
{c}
{title2=$|X|\leq|Y|,\ |Y|\leq|X|\Rightarrow|X|=|Y|$}
{wiki}

If there are injections $X\to Y$ and $Y\to X$, then there is a bijection $X\cong Y$.

For arbitrary <sets> $X$ and $Y$, the precise equivalence is
$$
\bigl(\exists\text{ injection }f:X\to Y\bigr)\ \land\ \bigl(\exists\text{ injection }g:Y\to X\bigr)
\quad\Longleftrightarrow\quad
\exists\text{ bijection }h:X\to Y.
$$
The reverse direction uses the <bijection> $h$ and its <inverse function>. Neither <set> is assumed to be a <subset> of the other: the hypothesis concerns <functions>, rather than containments. The forward direction holds in <ZF> without the <axiom of choice>.<Cantor-Schroeder-Bernstein Theorem by Paul Garrett>[Paul Garrett, Cantor-Schroeder-Bernstein Theorem, p. 1, theorem and paragraph explicitly excluding the axiom of choice]{ref}

This makes <cardinality> comparison an <antisymmetric relation>: if each <set> is no larger than the other in the sense of an <injection>, they have equal <cardinality>. It also gives a practical strategy: build two convenient <injections> and let the theorem supply the <bijection>. The <Injection-chain proof of the Cantor-Schröder-Bernstein theorem> explains how to combine them without losing an output or pairing two inputs with the same output.