Formal Proof of the Cantor-Bernstein-Schroeder Theorem

Georg Cantor
1845 – 1918

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

If set X can be mapped one-to-one into set Y (an injection), and set Y can be mapped one-to-one into set X (an injection), then X can be mapped one-to-one onto 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 the 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.