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

Theorem sbth 8239
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 8229 through sbthlem10 8238; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 8238. 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 8118 . . . 4 Rel ≼
21brrelexi 5297 . . 3 (𝐴𝐵𝐴 ∈ V)
31brrelexi 5297 . . 3 (𝐵𝐴𝐵 ∈ V)
4 breq1 4790 . . . . . 6 (𝑧 = 𝐴 → (𝑧𝑤𝐴𝑤))
5 breq2 4791 . . . . . 6 (𝑧 = 𝐴 → (𝑤𝑧𝑤𝐴))
64, 5anbi12d 616 . . . . 5 (𝑧 = 𝐴 → ((𝑧𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝐴)))
7 breq1 4790 . . . . 5 (𝑧 = 𝐴 → (𝑧𝑤𝐴𝑤))
86, 7imbi12d 333 . . . 4 (𝑧 = 𝐴 → (((𝑧𝑤𝑤𝑧) → 𝑧𝑤) ↔ ((𝐴𝑤𝑤𝐴) → 𝐴𝑤)))
9 breq2 4791 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤𝐴𝐵))
10 breq1 4790 . . . . . 6 (𝑤 = 𝐵 → (𝑤𝐴𝐵𝐴))
119, 10anbi12d 616 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤𝑤𝐴) ↔ (𝐴𝐵𝐵𝐴)))
12 breq2 4791 . . . . 5 (𝑤 = 𝐵 → (𝐴𝑤𝐴𝐵))
1311, 12imbi12d 333 . . . 4 (𝑤 = 𝐵 → (((𝐴𝑤𝑤𝐴) → 𝐴𝑤) ↔ ((𝐴𝐵𝐵𝐴) → 𝐴𝐵)))
14 vex 3354 . . . . 5 𝑧 ∈ V
15 sseq1 3775 . . . . . . 7 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
16 imaeq2 5602 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑓𝑦) = (𝑓𝑥))
1716difeq2d 3879 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑤 ∖ (𝑓𝑦)) = (𝑤 ∖ (𝑓𝑥)))
1817imaeq2d 5606 . . . . . . . 8 (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓𝑥))))
19 difeq2 3873 . . . . . . . 8 (𝑦 = 𝑥 → (𝑧𝑦) = (𝑧𝑥))
2018, 19sseq12d 3783 . . . . . . 7 (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥)))
2115, 20anbi12d 616 . . . . . 6 (𝑦 = 𝑥 → ((𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦)) ↔ (𝑥𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥))))
2221cbvabv 2896 . . . . 5 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))} = {𝑥 ∣ (𝑥𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥))}
23 eqid 2771 . . . . 5 ((𝑓 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}) ∪ (𝑔 ↾ (𝑧 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}))) = ((𝑓 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}) ∪ (𝑔 ↾ (𝑧 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))})))
24 vex 3354 . . . . 5 𝑤 ∈ V
2514, 22, 23, 24sbthlem10 8238 . . . 4 ((𝑧𝑤𝑤𝑧) → 𝑧𝑤)
268, 13, 25vtocl2g 3421 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐵𝐵𝐴) → 𝐴𝐵))
272, 3, 26syl2an 583 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐴𝐵𝐵𝐴) → 𝐴𝐵))
2827pm2.43i 52 1 ((𝐴𝐵𝐵𝐴) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  {cab 2757  Vcvv 3351  cdif 3720  cun 3721  wss 3723   cuni 4575   class class class wbr 4787  ccnv 5249  cres 5252  cima 5253  cen 8109  cdom 8110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-en 8113  df-dom 8114
This theorem is referenced by:  sbthb  8240  sdomnsym  8244  domtriord  8265  xpen  8282  limenpsi  8294  php  8303  onomeneq  8309  unbnn  8375  infxpenlem  9039  fseqen  9053  infpwfien  9088  inffien  9089  alephdom  9107  mappwen  9138  infcdaabs  9233  infunabs  9234  infcda  9235  infdif  9236  infxpabs  9239  infmap2  9245  gchaleph  9698  gchhar  9706  inttsk  9801  inar1  9802  znnen  15146  qnnen  15147  rpnnen  15161  rexpen  15162  mreexfidimd  16517  acsinfdimd  17389  fislw  18246  opnreen  22853  ovolctb2  23479  vitali  23600  aannenlem3  24304  basellem4  25030  lgsqrlem4  25294  upgrex  26207  phpreu  33725  poimirlem26  33767  pellexlem4  37922  pellexlem5  37923  idomsubgmo  38302
  Copyright terms: Public domain W3C validator