![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbth | Structured version Visualization version GIF version |
Description: Schroeder-Bernstein
Theorem. Theorem 18 of [Suppes] p. 95. This
theorem states that if set 𝐴 is smaller (has lower cardinality)
than
𝐵 and vice-versa, then 𝐴 and
𝐵
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 9079 through sbthlem10 9088; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9088. 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 9088. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.) |
Ref | Expression |
---|---|
sbth | ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldom 8941 | . . . 4 ⊢ Rel ≼ | |
2 | 1 | brrelex1i 5730 | . . 3 ⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
3 | 1 | brrelex1i 5730 | . . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V) |
4 | breq1 5150 | . . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ≼ 𝑤 ↔ 𝐴 ≼ 𝑤)) | |
5 | breq2 5151 | . . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑤 ≼ 𝑧 ↔ 𝑤 ≼ 𝐴)) | |
6 | 4, 5 | anbi12d 631 | . . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) ↔ (𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴))) |
7 | breq1 5150 | . . . . 5 ⊢ (𝑧 = 𝐴 → (𝑧 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) | |
8 | 6, 7 | imbi12d 344 | . . . 4 ⊢ (𝑧 = 𝐴 → (((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) ↔ ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤))) |
9 | breq2 5151 | . . . . . 6 ⊢ (𝑤 = 𝐵 → (𝐴 ≼ 𝑤 ↔ 𝐴 ≼ 𝐵)) | |
10 | breq1 5150 | . . . . . 6 ⊢ (𝑤 = 𝐵 → (𝑤 ≼ 𝐴 ↔ 𝐵 ≼ 𝐴)) | |
11 | 9, 10 | anbi12d 631 | . . . . 5 ⊢ (𝑤 = 𝐵 → ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) ↔ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
12 | breq2 5151 | . . . . 5 ⊢ (𝑤 = 𝐵 → (𝐴 ≈ 𝑤 ↔ 𝐴 ≈ 𝐵)) | |
13 | 11, 12 | imbi12d 344 | . . . 4 ⊢ (𝑤 = 𝐵 → (((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤) ↔ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵))) |
14 | vex 3478 | . . . . 5 ⊢ 𝑧 ∈ V | |
15 | sseq1 4006 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝑧)) | |
16 | imaeq2 6053 | . . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑓 “ 𝑦) = (𝑓 “ 𝑥)) | |
17 | 16 | difeq2d 4121 | . . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑤 ∖ (𝑓 “ 𝑦)) = (𝑤 ∖ (𝑓 “ 𝑥))) |
18 | 17 | imaeq2d 6057 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥)))) |
19 | difeq2 4115 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑧 ∖ 𝑦) = (𝑧 ∖ 𝑥)) | |
20 | 18, 19 | sseq12d 4014 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))) |
21 | 15, 20 | anbi12d 631 | . . . . . 6 ⊢ (𝑦 = 𝑥 → ((𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦)) ↔ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥)))) |
22 | 21 | cbvabv 2805 | . . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))} = {𝑥 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))} |
23 | eqid 2732 | . . . . 5 ⊢ ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) = ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) | |
24 | vex 3478 | . . . . 5 ⊢ 𝑤 ∈ V | |
25 | 14, 22, 23, 24 | sbthlem10 9088 | . . . 4 ⊢ ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) |
26 | 8, 13, 25 | vtocl2g 3562 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)) |
27 | 2, 3, 26 | syl2an 596 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)) |
28 | 27 | pm2.43i 52 | 1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2709 Vcvv 3474 ∖ cdif 3944 ∪ cun 3945 ⊆ wss 3947 ∪ cuni 4907 class class class wbr 5147 ◡ccnv 5674 ↾ cres 5677 “ cima 5678 ≈ cen 8932 ≼ cdom 8933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-en 8936 df-dom 8937 |
This theorem is referenced by: sbthb 9090 sdomnsym 9094 domtriord 9119 xpen 9136 limenpsi 9148 phpOLD 9218 onomeneqOLD 9225 unbnn 9295 infxpenlem 10004 fseqen 10018 infpwfien 10053 inffien 10054 alephdom 10072 mappwen 10103 infdjuabs 10197 infunabs 10198 infdju 10199 infdif 10200 infxpabs 10203 infmap2 10209 gchaleph 10662 gchhar 10670 inttsk 10765 inar1 10766 znnen 16151 qnnen 16152 rpnnen 16166 rexpen 16167 mreexfidimd 17590 acsinfdimd 18507 fislw 19487 opnreen 24338 ovolctb2 25000 vitali 25121 aannenlem3 25834 basellem4 26577 lgsqrlem4 26841 upgrex 28341 iccioo01 36196 ctbssinf 36275 phpreu 36460 poimirlem26 36502 pellexlem4 41555 pellexlem5 41556 idomsubgmo 41925 |
Copyright terms: Public domain | W3C validator |