# Formal Proof of the Cantor-Bernstein-Schroeder Theorem

The Cantor-Bernstein-Schroeder Theorem (CBST), is one of the most important and widely applied results in set theory:

If set

Xcan be mapped one-to-one into setY(an injection), and setYcan be mapped one-to-one into set X (an injection), then X can be mapped one-to-oneonto Y(a bijection).

Though seemingly self-evident, some proofs of CBST can make your head spin! Every line of my machine-verified, formal proof (updated 2014-09-11) is justified by one of a very limited list of simple axioms and rules of inference (indicated in a grey font at the end of each line).

Such complete rigour does come at a price, however. While it is completely free of any of the sort of the hand-waving that plagues many informal versions of this proof, like most formal proofs of any complexity, it is *very* long. My commentary (indicated by a blue font) is inserted throughout using *DC Proof.* I believe this makes my proof considerably more readable than machine-generated formal proofs in other systems.

This proof was written to demonstrate he capabilities of the *DC Proof* system. Though designed for ease of use by the complete beginner, *DC Proof* is quite capable of some mathematical heavy lifting.