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 ( ( 𝐴𝐵𝐵𝐴 ) → 𝐴𝐵 )

Proof

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 ( ( 𝐴𝐵𝐵𝐴 ) → 𝐴𝐵 )