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 ﬁnis, 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).