Skip to content
Axiomatic Wiki

WTThe Cantor-Schröder-Bernstein theorem

Theorem·T17

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.
Rests onF02F03F04F06F08F09F11F14A01A02A03A04A06A08
Never needed: F05 · F10 · F12 · F13 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Setup. 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. 2
    Critical sets. By the recursion theorem define (power set) by with start value (D009) and step , a function because and (D007). Write and let be their union (Union), a subset of .
  3. 3
    The 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. 4
    Key inclusion. If then : for (D004) we have , hence (D007, the step equation).
  5. 5
    Injective. 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.
  6. 6
    Surjective. 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. 7
    Conclusion. is injective and surjective, hence a bijection; therefore (D033).
∎

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.
Wikipedia ↗Function.Embedding.antisymm ↗
Propose an edit1 published revision