Theorem sbth 9129

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 9119 through sbthlem10 9128; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9128. 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 9128. 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.

Step	Hyp	Ref	Expression
1		reldom 8987	. . . 4 ⊢ Rel ≼
2	1	brrelex1i 5739	. . 3 ⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V)
3	1	brrelex1i 5739	. . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V)
4		breq1 5144	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ≼ 𝑤 ↔ 𝐴 ≼ 𝑤))
5		breq2 5145	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑤 ≼ 𝑧 ↔ 𝑤 ≼ 𝐴))
6	4, 5	anbi12d 632	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) ↔ (𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴)))
7		breq1 5144	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑧 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑧 = 𝐴 → (((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) ↔ ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤)))
9		breq2 5145	. . . . . 6 ⊢ (𝑤 = 𝐵 → (𝐴 ≼ 𝑤 ↔ 𝐴 ≼ 𝐵))
10		breq1 5144	. . . . . 6 ⊢ (𝑤 = 𝐵 → (𝑤 ≼ 𝐴 ↔ 𝐵 ≼ 𝐴))
11	9, 10	anbi12d 632	. . . . 5 ⊢ (𝑤 = 𝐵 → ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) ↔ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)))
12		breq2 5145	. . . . 5 ⊢ (𝑤 = 𝐵 → (𝐴 ≈ 𝑤 ↔ 𝐴 ≈ 𝐵))
13	11, 12	imbi12d 344	. . . 4 ⊢ (𝑤 = 𝐵 → (((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤) ↔ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)))
14		vex 3483	. . . . 5 ⊢ 𝑧 ∈ V
15		sseq1 4008	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝑧))
16		imaeq2 6072	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑓 “ 𝑦) = (𝑓 “ 𝑥))
17	16	difeq2d 4125	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑤 ∖ (𝑓 “ 𝑦)) = (𝑤 ∖ (𝑓 “ 𝑥)))
18	17	imaeq2d 6076	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))))
19		difeq2 4119	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑧 ∖ 𝑦) = (𝑧 ∖ 𝑥))
20	18, 19	sseq12d 4016	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥)))
21	15, 20	anbi12d 632	. . . . . 6 ⊢ (𝑦 = 𝑥 → ((𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦)) ↔ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))))
22	21	cbvabv 2811	. . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))} = {𝑥 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))}
23		eqid 2736	. . . . 5 ⊢ ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) = ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))})))
24		vex 3483	. . . . 5 ⊢ 𝑤 ∈ V
25	14, 22, 23, 24	sbthlem10 9128	. . . 4 ⊢ ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤)
26	8, 13, 25	vtocl2g 3573	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵))
27	2, 3, 26	syl2an 596	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵))
28	27	pm2.43i 52	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2713  Vcvv 3479   ∖ cdif 3947   ∪ cun 3948   ⊆ wss 3950  ∪ cuni 4905   class class class wbr 5141  ^◡ccnv 5682   ↾ cres 5685   “ cima 5686   ≈ cen 8978   ≼ cdom 8979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-en 8982  df-dom 8983

This theorem is referenced by:  sbthb  9130  sdomnsym  9134  domtriord  9159  xpen  9176  limenpsi  9188  phpOLD  9255  onomeneqOLD  9262  unbnn  9328  infxpenlem  10049  fseqen  10063  infpwfien  10098  inffien  10099  alephdom  10117  mappwen  10148  infdjuabs  10241  infunabs  10242  infdju  10243  infdif  10244  infxpabs  10247  infmap2  10253  gchaleph  10707  gchhar  10715  inttsk  10810  inar1  10811  znnen  16244  qnnen  16245  rpnnen  16259  rexpen  16260  mreexfidimd  17689  acsinfdimd  18599  fislw  19639  opnreen  24843  ovolctb2  25517  vitali  25638  aannenlem3  26362  basellem4  27117  lgsqrlem4  27383  upgrex  29099  iccioo01  37306  ctbssinf  37385  phpreu  37589  poimirlem26  37631  pellexlem4  42821  pellexlem5  42822  idomsubgmo  43183