Theorem·T17
The Cantor-Schröder-Bernstein theorem
If each of two sets injects into the other, then the two are equinumerous.
If
and
(domination), then
(equinumerous). Concretely, from an injection
and an injection
one builds a bijection
.
In words
If there is an injective function from A into B and an injective function from B into A, then there is a bijection between A and B: the two sets have exactly the same size.
Never needed: F05 · F10 · F12 · F13 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Setup. Let and be injections. Viewing as a map onto its image , it is surjective onto and injective, hence a bijection ; by L03 it has an inverse with for every and for every .
- 2
- 3The map. Define by It is well defined: if then , so (D009) and exists. Exactly one clause applies to each (excluded middle) and both values lie in , so is a function .
- 4
- 5Injective. Suppose . If : then , so ( injective). If : then , and applying gives (Setup). The mixed case cannot occur: if and with , then (Setup, since ), so by the Key inclusion, contradicting . Hence is injective.
- 6Surjective. Let and look at . If then (Setup). If : as we have , so with , hence (L15 (vii)) and . Thus for some ; injectivity of gives , and gives . Either way is a value of , so is surjective onto .
- 7
∎
Remarks
Stated by Cantor, first proved without choice by Felix Bernstein (1897) and, independently, Ernst Schröder and Richard Dedekind; the fixed-point construction of the critical sets
is Banach's. No choice is used: the bijection is built explicitly. The theorem is the antisymmetry law for domination and the workhorse for proving two sets equinumerous (exhibit injections both ways rather than a bijection directly). It stands beside Cantor's theorem, which supplies the strict inequalities the order needs to be interesting.