Theorem sbth 9073

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 9063 through sbthlem10 9072; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9072. 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 9072. 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 8937	. . . 4 ⊢ Rel ≼
2	1	brrelex1i 5707	. . 3 ⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V)
3	1	brrelex1i 5707	. . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V)
4		breq1 5107	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ≼ 𝑤 ↔ 𝐴 ≼ 𝑤))
5		breq2 5108	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑤 ≼ 𝑧 ↔ 𝑤 ≼ 𝐴))
6	4, 5	anbi12d 643	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) ↔ (𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴)))
7		breq1 5107	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑧 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤))
8	6, 7	imbi12d 347	. . . 4 ⊢ (𝑧 = 𝐴 → (((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) ↔ ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤)))
9		breq2 5108	. . . . . 6 ⊢ (𝑤 = 𝐵 → (𝐴 ≼ 𝑤 ↔ 𝐴 ≼ 𝐵))
10		breq1 5107	. . . . . 6 ⊢ (𝑤 = 𝐵 → (𝑤 ≼ 𝐴 ↔ 𝐵 ≼ 𝐴))
11	9, 10	anbi12d 643	. . . . 5 ⊢ (𝑤 = 𝐵 → ((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) ↔ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)))
12		breq2 5108	. . . . 5 ⊢ (𝑤 = 𝐵 → (𝐴 ≈ 𝑤 ↔ 𝐴 ≈ 𝐵))
13	11, 12	imbi12d 347	. . . 4 ⊢ (𝑤 = 𝐵 → (((𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤) ↔ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)))
14		vex 3461	. . . . 5 ⊢ 𝑧 ∈ V
15		sseq1 3964	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝑧))
16		imaeq2 6048	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑓 “ 𝑦) = (𝑓 “ 𝑥))
17	16	difeq2d 4083	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑤 ∖ (𝑓 “ 𝑦)) = (𝑤 ∖ (𝑓 “ 𝑥)))
18	17	imaeq2d 6052	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))))
19		difeq2 4077	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑧 ∖ 𝑦) = (𝑧 ∖ 𝑥))
20	18, 19	sseq12d 3972	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥)))
21	15, 20	anbi12d 643	. . . . . 6 ⊢ (𝑦 = 𝑥 → ((𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦)) ↔ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))))
22	21	cbvabv 2835	. . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))} = {𝑥 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))}
23		eqid 2765	. . . . 5 ⊢ ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) = ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))})))
24		vex 3461	. . . . 5 ⊢ 𝑤 ∈ V
25	14, 22, 23, 24	sbthlem10 9072	. . . 4 ⊢ ((𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤)
26	8, 13, 25	vtocl2g 3541	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵))
27	2, 3, 26	syl2an 607	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵))
28	27	pm2.43i 53	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {cab 2743  Vcvv 3457   ∖ cdif 3904   ∪ cun 3905   ⊆ wss 3907  ∪ cuni 4867   class class class wbr 5104  ^◡ccnv 5650   ↾ cres 5653   “ cima 5654   ≈ cen 8928   ≼ cdom 8929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-en 8932  df-dom 8933

This theorem is referenced by:  sbthb  9074  sdomnsym  9078  domtriord  9099  xpen  9116  limenpsi  9128  unbnn  9244  infxpenlem  9985  fseqen  9999  infpwfien  10034  inffien  10035  alephdom  10053  mappwen  10084  infdjuabs  10176  infunabs  10177  infdju  10178  infdif  10179  infxpabs  10182  infmap2  10188  gchaleph  10644  gchhar  10652  inttsk  10747  inar1  10748  znnen  16256  qnnen  16257  rpnnen  16271  rexpen  16272  mreexfidimd  17694  acsinfdimd  18602  fislw  19683  opnreen  24946  ovolctb2  25608  vitali  25729  aannenlem3  26448  basellem4  27202  lgsqrlem4  27467  upgrex  29347  iccioo01  37828  ctbssinf  37907  phpreu  38110  poimirlem26  38152  pellexlem4  43416  pellexlem5  43417  idomsubgmo  43777