ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isbth GIF version

Theorem isbth 7026
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 7016 through sbthlemi10 7025; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 7025. 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. The proof does require the law of the excluded middle which cannot be avoided as shown at exmidsbthr 15513. (Contributed by NM, 8-Jun-1998.)
Assertion
Ref Expression
isbth ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → 𝐴𝐵)

Proof of Theorem isbth
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 529 . 2 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → 𝐴𝐵)
2 simprr 531 . 2 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → 𝐵𝐴)
3 reldom 6799 . . . . 5 Rel ≼
43brrelex1i 4702 . . . 4 (𝐵𝐴𝐵 ∈ V)
52, 4syl 14 . . 3 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → 𝐵 ∈ V)
6 breq2 4033 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤𝐴𝐵))
7 breq1 4032 . . . . . 6 (𝑤 = 𝐵 → (𝑤𝐴𝐵𝐴))
86, 7anbi12d 473 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤𝑤𝐴) ↔ (𝐴𝐵𝐵𝐴)))
9 breq2 4033 . . . . 5 (𝑤 = 𝐵 → (𝐴𝑤𝐴𝐵))
108, 9imbi12d 234 . . . 4 (𝑤 = 𝐵 → (((𝐴𝑤𝑤𝐴) → 𝐴𝑤) ↔ ((𝐴𝐵𝐵𝐴) → 𝐴𝐵)))
1110adantl 277 . . 3 (((EXMID ∧ (𝐴𝐵𝐵𝐴)) ∧ 𝑤 = 𝐵) → (((𝐴𝑤𝑤𝐴) → 𝐴𝑤) ↔ ((𝐴𝐵𝐵𝐴) → 𝐴𝐵)))
123brrelex1i 4702 . . . . 5 (𝐴𝐵𝐴 ∈ V)
131, 12syl 14 . . . 4 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → 𝐴 ∈ V)
14 breq1 4032 . . . . . . 7 (𝑧 = 𝐴 → (𝑧𝑤𝐴𝑤))
15 breq2 4033 . . . . . . 7 (𝑧 = 𝐴 → (𝑤𝑧𝑤𝐴))
1614, 15anbi12d 473 . . . . . 6 (𝑧 = 𝐴 → ((𝑧𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝐴)))
17 breq1 4032 . . . . . 6 (𝑧 = 𝐴 → (𝑧𝑤𝐴𝑤))
1816, 17imbi12d 234 . . . . 5 (𝑧 = 𝐴 → (((𝑧𝑤𝑤𝑧) → 𝑧𝑤) ↔ ((𝐴𝑤𝑤𝐴) → 𝐴𝑤)))
1918adantl 277 . . . 4 (((EXMID ∧ (𝐴𝐵𝐵𝐴)) ∧ 𝑧 = 𝐴) → (((𝑧𝑤𝑤𝑧) → 𝑧𝑤) ↔ ((𝐴𝑤𝑤𝐴) → 𝐴𝑤)))
20 vex 2763 . . . . . . 7 𝑧 ∈ V
21 sseq1 3202 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
22 imaeq2 5001 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑓𝑦) = (𝑓𝑥))
2322difeq2d 3277 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝑤 ∖ (𝑓𝑦)) = (𝑤 ∖ (𝑓𝑥)))
2423imaeq2d 5005 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓𝑥))))
25 difeq2 3271 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑧𝑦) = (𝑧𝑥))
2624, 25sseq12d 3210 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥)))
2721, 26anbi12d 473 . . . . . . . 8 (𝑦 = 𝑥 → ((𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦)) ↔ (𝑥𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥))))
2827cbvabv 2318 . . . . . . 7 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))} = {𝑥 ∣ (𝑥𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑥))) ⊆ (𝑧𝑥))}
29 eqid 2193 . . . . . . 7 ((𝑓 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}) ∪ (𝑔 ↾ (𝑧 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}))) = ((𝑓 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))}) ∪ (𝑔 ↾ (𝑧 {𝑦 ∣ (𝑦𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓𝑦))) ⊆ (𝑧𝑦))})))
30 vex 2763 . . . . . . 7 𝑤 ∈ V
3120, 28, 29, 30sbthlemi10 7025 . . . . . 6 ((EXMID ∧ (𝑧𝑤𝑤𝑧)) → 𝑧𝑤)
3231ex 115 . . . . 5 (EXMID → ((𝑧𝑤𝑤𝑧) → 𝑧𝑤))
3332adantr 276 . . . 4 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → ((𝑧𝑤𝑤𝑧) → 𝑧𝑤))
3413, 19, 33vtocld 2812 . . 3 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → ((𝐴𝑤𝑤𝐴) → 𝐴𝑤))
355, 11, 34vtocld 2812 . 2 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → ((𝐴𝐵𝐵𝐴) → 𝐴𝐵))
361, 2, 35mp2and 433 1 ((EXMID ∧ (𝐴𝐵𝐵𝐴)) → 𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1364  wcel 2164  {cab 2179  Vcvv 2760  cdif 3150  cun 3151  wss 3153   cuni 3835   class class class wbr 4029  EXMIDwem 4223  ccnv 4658  cres 4661  cima 4662  cen 6792  cdom 6793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-exmid 4224  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-en 6795  df-dom 6796
This theorem is referenced by:  exmidsbth  15514
  Copyright terms: Public domain W3C validator