![]() |
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 9153 through sbthlem10 9162; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9162. 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 9162. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.) |
Ref | Expression |
---|---|
sbth | ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldom 9013 | . . . 4 ⊢ Rel ≼ | |
2 | 1 | brrelex1i 5758 | . . 3 ⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
3 | 1 | brrelex1i 5758 | . . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V) |
4 | breq1 5171 | . . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ≼ 𝑤 ↔ 𝐴 ≼ 𝑤)) | |
5 | breq2 5172 | . . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑤 ≼ 𝑧 ↔ 𝑤 ≼ 𝐴)) | |
6 | 4, 5 | anbi12d 631 | . . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) ↔ (𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴))) |
7 | breq1 5171 | . . . . 5 ⊢ (𝑧 = 𝐴 → (𝑧 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) | |
8 | 6, 7 | imbi12d 344 | . . . 4 ⊢ (𝑧 = 𝐴 → (((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) ↔ ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤))) |
9 | breq2 5172 | . . . . . 6 ⊢ (𝑤 = 𝐵 → (𝐴 ≼ 𝑤 ↔ 𝐴 ≼ 𝐵)) | |
10 | breq1 5171 | . . . . . 6 ⊢ (𝑤 = 𝐵 → (𝑤 ≼ 𝐴 ↔ 𝐵 ≼ 𝐴)) | |
11 | 9, 10 | anbi12d 631 | . . . . 5 ⊢ (𝑤 = 𝐵 → ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) ↔ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
12 | breq2 5172 | . . . . 5 ⊢ (𝑤 = 𝐵 → (𝐴 ≈ 𝑤 ↔ 𝐴 ≈ 𝐵)) | |
13 | 11, 12 | imbi12d 344 | . . . 4 ⊢ (𝑤 = 𝐵 → (((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤) ↔ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵))) |
14 | vex 3493 | . . . . 5 ⊢ 𝑧 ∈ V | |
15 | sseq1 4035 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝑧)) | |
16 | imaeq2 6089 | . . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑓 “ 𝑦) = (𝑓 “ 𝑥)) | |
17 | 16 | difeq2d 4150 | . . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑤 ∖ (𝑓 “ 𝑦)) = (𝑤 ∖ (𝑓 “ 𝑥))) |
18 | 17 | imaeq2d 6093 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥)))) |
19 | difeq2 4144 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑧 ∖ 𝑦) = (𝑧 ∖ 𝑥)) | |
20 | 18, 19 | sseq12d 4043 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))) |
21 | 15, 20 | anbi12d 631 | . . . . . 6 ⊢ (𝑦 = 𝑥 → ((𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦)) ↔ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥)))) |
22 | 21 | cbvabv 2815 | . . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))} = {𝑥 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))} |
23 | eqid 2740 | . . . . 5 ⊢ ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) = ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) | |
24 | vex 3493 | . . . . 5 ⊢ 𝑤 ∈ V | |
25 | 14, 22, 23, 24 | sbthlem10 9162 | . . . 4 ⊢ ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) |
26 | 8, 13, 25 | vtocl2g 3587 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)) |
27 | 2, 3, 26 | syl2an 595 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)) |
28 | 27 | pm2.43i 52 | 1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2108 {cab 2717 Vcvv 3489 ∖ cdif 3974 ∪ cun 3975 ⊆ wss 3977 ∪ cuni 4933 class class class wbr 5168 ◡ccnv 5701 ↾ cres 5704 “ cima 5705 ≈ cen 9004 ≼ cdom 9005 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-12 2178 ax-ext 2711 ax-sep 5319 ax-nul 5326 ax-pow 5385 ax-pr 5449 ax-un 7774 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-ral 3068 df-rex 3077 df-rab 3445 df-v 3491 df-dif 3980 df-un 3982 df-in 3984 df-ss 3994 df-nul 4354 df-if 4550 df-pw 4625 df-sn 4650 df-pr 4652 df-op 4656 df-uni 4934 df-br 5169 df-opab 5231 df-id 5595 df-xp 5708 df-rel 5709 df-cnv 5710 df-co 5711 df-dm 5712 df-rn 5713 df-res 5714 df-ima 5715 df-fun 6579 df-fn 6580 df-f 6581 df-f1 6582 df-fo 6583 df-f1o 6584 df-en 9008 df-dom 9009 |
This theorem is referenced by: sbthb 9164 sdomnsym 9168 domtriord 9193 xpen 9210 limenpsi 9222 phpOLD 9289 onomeneqOLD 9296 unbnn 9364 infxpenlem 10086 fseqen 10100 infpwfien 10135 inffien 10136 alephdom 10154 mappwen 10185 infdjuabs 10278 infunabs 10279 infdju 10280 infdif 10281 infxpabs 10284 infmap2 10290 gchaleph 10744 gchhar 10752 inttsk 10847 inar1 10848 znnen 16278 qnnen 16279 rpnnen 16293 rexpen 16294 mreexfidimd 17729 acsinfdimd 18649 fislw 19688 opnreen 24893 ovolctb2 25567 vitali 25688 aannenlem3 26411 basellem4 27166 lgsqrlem4 27432 upgrex 29148 iccioo01 37313 ctbssinf 37392 phpreu 37594 poimirlem26 37636 pellexlem4 42817 pellexlem5 42818 idomsubgmo 43183 |
Copyright terms: Public domain | W3C validator |