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 | ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reldom | ⊢ Rel ≼ | |
| 2 | 1 | brrelex1i | ⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V ) |
| 3 | 1 | brrelex1i | ⊢ ( 𝐵 ≼ 𝐴 → 𝐵 ∈ V ) |
| 4 | breq1 | ⊢ ( 𝑧 = 𝐴 → ( 𝑧 ≼ 𝑤 ↔ 𝐴 ≼ 𝑤 ) ) | |
| 5 | breq2 | ⊢ ( 𝑧 = 𝐴 → ( 𝑤 ≼ 𝑧 ↔ 𝑤 ≼ 𝐴 ) ) | |
| 6 | 4 5 | anbi12d | ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧 ) ↔ ( 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) ) ) |
| 7 | breq1 | ⊢ ( 𝑧 = 𝐴 → ( 𝑧 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤 ) ) | |
| 8 | 6 7 | imbi12d | ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧 ) → 𝑧 ≈ 𝑤 ) ↔ ( ( 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) → 𝐴 ≈ 𝑤 ) ) ) |
| 9 | breq2 | ⊢ ( 𝑤 = 𝐵 → ( 𝐴 ≼ 𝑤 ↔ 𝐴 ≼ 𝐵 ) ) | |
| 10 | breq1 | ⊢ ( 𝑤 = 𝐵 → ( 𝑤 ≼ 𝐴 ↔ 𝐵 ≼ 𝐴 ) ) | |
| 11 | 9 10 | anbi12d | ⊢ ( 𝑤 = 𝐵 → ( ( 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) ↔ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) ) |
| 12 | breq2 | ⊢ ( 𝑤 = 𝐵 → ( 𝐴 ≈ 𝑤 ↔ 𝐴 ≈ 𝐵 ) ) | |
| 13 | 11 12 | imbi12d | ⊢ ( 𝑤 = 𝐵 → ( ( ( 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) → 𝐴 ≈ 𝑤 ) ↔ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) ) ) |
| 14 | vex | ⊢ 𝑧 ∈ V | |
| 15 | sseq1 | ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝑧 ) ) | |
| 16 | imaeq2 | ⊢ ( 𝑦 = 𝑥 → ( 𝑓 “ 𝑦 ) = ( 𝑓 “ 𝑥 ) ) | |
| 17 | 16 | difeq2d | ⊢ ( 𝑦 = 𝑥 → ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) = ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) |
| 18 | 17 | imaeq2d | ⊢ ( 𝑦 = 𝑥 → ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) = ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) ) |
| 19 | difeq2 | ⊢ ( 𝑦 = 𝑥 → ( 𝑧 ∖ 𝑦 ) = ( 𝑧 ∖ 𝑥 ) ) | |
| 20 | 18 19 | sseq12d | ⊢ ( 𝑦 = 𝑥 → ( ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ↔ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝑧 ∖ 𝑥 ) ) ) |
| 21 | 15 20 | anbi12d | ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) ↔ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝑧 ∖ 𝑥 ) ) ) ) |
| 22 | 21 | cbvabv | ⊢ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } = { 𝑥 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝑧 ∖ 𝑥 ) ) } |
| 23 | eqid | ⊢ ( ( 𝑓 ↾ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ∪ ( ◡ 𝑔 ↾ ( 𝑧 ∖ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ) ) = ( ( 𝑓 ↾ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ∪ ( ◡ 𝑔 ↾ ( 𝑧 ∖ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ) ) | |
| 24 | vex | ⊢ 𝑤 ∈ V | |
| 25 | 14 22 23 24 | sbthlem10 | ⊢ ( ( 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧 ) → 𝑧 ≈ 𝑤 ) |
| 26 | 8 13 25 | vtocl2g | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) ) |
| 27 | 2 3 26 | syl2an | ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) ) |
| 28 | 27 | pm2.43i | ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) |