MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbth Structured version   Visualization version   GIF version

Theorem sbth 8025
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, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 8015 through sbthlem10 8024; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 8024. 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. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.)
Assertion
Ref Expression
sbth ((𝐴𝐵𝐵𝐴) → 𝐴𝐵)

Proof of Theorem sbth
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 7906 . . . 4 Rel ≼
21brrelexi 5123 . . 3 (𝐴𝐵𝐴 ∈ V)
31brrelexi 5123 . . 3 (𝐵𝐴𝐵 ∈ V)
4 breq1 4621 . . . . . 6 (𝑧 = 𝐴 → (𝑧𝑤𝐴𝑤))
5 breq2 4622 . . . . . 6 (𝑧 = 𝐴 → (𝑤𝑧𝑤𝐴))
64, 5anbi12d 746 . . . . 5 (𝑧 = 𝐴 → ((𝑧𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝐴)))
7 breq1 4621 . . . . 5 (𝑧 = 𝐴 → (𝑧𝑤𝐴𝑤))
86, 7imbi12d 334 . . . 4 (𝑧 = 𝐴 → (((𝑧𝑤𝑤𝑧) → 𝑧𝑤) ↔ ((𝐴𝑤𝑤𝐴) → 𝐴𝑤)))
9 breq2 4622 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤𝐴𝐵))
10 breq1 4621 . . . . . 6 (𝑤 = 𝐵 → (𝑤𝐴𝐵𝐴))
119, 10anbi12d 746 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤𝑤𝐴) ↔ (𝐴𝐵𝐵𝐴)))
12 breq2 4622 . . . . 5 (𝑤 = 𝐵 → (𝐴𝑤𝐴𝐵))
1311, 12imbi12d 334 . . . 4 (𝑤 = 𝐵 → (((𝐴𝑤𝑤𝐴) → 𝐴𝑤) ↔ ((𝐴𝐵𝐵𝐴) → 𝐴𝐵)))
14 vex 3194 . . . . 5 𝑧 ∈ V
15 sseq1 3610 . . . . . . 7 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
16 imaeq2 5425 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑓𝑦) = (𝑓𝑥))
1716difeq2d 3711 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑤 ∖ (𝑓𝑦)) = (𝑤 ∖ (𝑓𝑥)))
1817imaeq2d 5429 . . . . . . . 8 (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓𝑥))))
19 difeq2 3705 . . . . . . . 8 (𝑦 = 𝑥 → (𝑧𝑦) = (𝑧𝑥))
2018, 19sseq12d 3618 . . . . . . 7 (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥)))
2115, 20anbi12d 746 . . . . . 6 (𝑦 = 𝑥 → ((𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦)) ↔ (𝑥𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥))))
2221cbvabv 2750 . . . . 5 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))} = {𝑥 ∣ (𝑥𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥))}
23 eqid 2626 . . . . 5 ((𝑓 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}) ∪ (𝑔 ↾ (𝑧 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}))) = ((𝑓 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}) ∪ (𝑔 ↾ (𝑧 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))})))
24 vex 3194 . . . . 5 𝑤 ∈ V
2514, 22, 23, 24sbthlem10 8024 . . . 4 ((𝑧𝑤𝑤𝑧) → 𝑧𝑤)
268, 13, 25vtocl2g 3261 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐵𝐵𝐴) → 𝐴𝐵))
272, 3, 26syl2an 494 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐴𝐵𝐵𝐴) → 𝐴𝐵))
2827pm2.43i 52 1 ((𝐴𝐵𝐵𝐴) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1992  {cab 2612  Vcvv 3191  cdif 3557  cun 3558  wss 3560   cuni 4407   class class class wbr 4618  ccnv 5078  cres 5081  cima 5082  cen 7897  cdom 7898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-en 7901  df-dom 7902
This theorem is referenced by:  sbthb  8026  sdomnsym  8030  domtriord  8051  xpen  8068  limenpsi  8080  php  8089  onomeneq  8095  unbnn  8161  infxpenlem  8781  fseqen  8795  infpwfien  8830  inffien  8831  alephdom  8849  mappwen  8880  infcdaabs  8973  infunabs  8974  infcda  8975  infdif  8976  infxpabs  8979  infmap2  8985  gchaleph  9438  gchhar  9446  inttsk  9541  inar1  9542  znnen  14861  qnnen  14862  rpnnen  14876  rexpen  14877  mreexfidimd  16227  acsinfdimd  17098  fislw  17956  opnreen  22537  ovolctb2  23162  vitali  23283  aannenlem3  23984  basellem4  24705  lgsqrlem4  24969  upgrex  25878  phpreu  32992  poimirlem26  33034  pellexlem4  36843  pellexlem5  36844  idomsubgmo  37224
  Copyright terms: Public domain W3C validator