Metamath Proof Explorer


Theorem sbth

Description: Schroeder-Bernstein Theorem. Theorem 18 of Suppes p. 95. This theorem states that if set A is smaller (has lower cardinality) than B and vice-versa, then A and B are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here. The theorem can also be proved from the axiom of choice and the linear order of the cardinal numbers, but our development does not provide the linear order of cardinal numbers until much later and in ways that depend on Schroeder-Bernstein.

The main proof consists of lemmas sbthlem1 through sbthlem10 ; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 . We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity. In the Intuitionistic Logic Explorer (ILE) the Schroeder-Bernstein Theorem has been proven equivalent to the law of the excluded middle (LEM), and in ILE the LEM is not accepted as necessarily true; see https://us.metamath.org/ileuni/exmidsbth.html . This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998)

Ref Expression
Assertion sbth ABBAAB

Proof

Step Hyp Ref Expression
1 reldom Rel
2 1 brrelex1i ABAV
3 1 brrelex1i BABV
4 breq1 z=AzwAw
5 breq2 z=AwzwA
6 4 5 anbi12d z=AzwwzAwwA
7 breq1 z=AzwAw
8 6 7 imbi12d z=AzwwzzwAwwAAw
9 breq2 w=BAwAB
10 breq1 w=BwABA
11 9 10 anbi12d w=BAwwAABBA
12 breq2 w=BAwAB
13 11 12 imbi12d w=BAwwAAwABBAAB
14 vex zV
15 sseq1 y=xyzxz
16 imaeq2 y=xfy=fx
17 16 difeq2d y=xwfy=wfx
18 17 imaeq2d y=xgwfy=gwfx
19 difeq2 y=xzy=zx
20 18 19 sseq12d y=xgwfyzygwfxzx
21 15 20 anbi12d y=xyzgwfyzyxzgwfxzx
22 21 cbvabv y|yzgwfyzy=x|xzgwfxzx
23 eqid fy|yzgwfyzyg-1zy|yzgwfyzy=fy|yzgwfyzyg-1zy|yzgwfyzy
24 vex wV
25 14 22 23 24 sbthlem10 zwwzzw
26 8 13 25 vtocl2g AVBVABBAAB
27 2 3 26 syl2an ABBAABBAAB
28 27 pm2.43i ABBAAB