Write to indicate that there is an injection from
into
, and
to mean that either
, or else there is a surjection from
onto
. It is a result of Kuratowski that (provably in
) if
, then in fact
, and therefore
. This appears as Théorème B in pages 94-95 of
Alfred Tarski. Sur les ensembles finis, Fund. Math. 6 (1924), 45–95.
To prove this result, note that it suffices to find a countably infinite family of disjoint subsets of . Suppose
is an injection of
into
. These sets induce a partition of
: Consider the equivalence classes of the relation
iff
.
It is natural to attempt to show that these equivalence classes can be enumerated. Of course, the class of is completely specified by the list of values of
such that
, but this list may be “wasteful” in the sense that it may contain redundant information. For example, if
, and we know that
, then we automatically know that
, and there is no need to include
in our list if we already included
. (On the other hand, if all we know is that
then including
in the list is certainly providing us with more information.) This suggests to assign to each
the set
defined recursively as follows: Let
be least such that
, if it exists. If
is defined, let
be least such that
and
, if it exists, and note that this is the same as requiring that
. Similarly, if
is defined, let
be least such that
, and
, if it exists, etc.
Clearly, for any ,
iff
. There are now two possibilities:
- Case 1. For some
, the set
is infinite.
In this case, we are done (and we do not even need to bother enumerating the classes), because the sequence
is a countably infinite collection of non-empty disjoint subsets of .
- Case 2. All sets
are finite.
In this case we are done as well, because there is a (canonical) bijection between and
, which means that we have enumerated the equivalence classes (and, of course, there are infinitely many, since the sets
are all distinct, and each is a union of equivalence classes).