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

Theorem pm54.43 9644
Description: Theorem *54.43 of [WhiteheadRussell] p. 360. "From this proposition it will follow, when arithmetical addition has been defined, that 1+1=2." See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations. This theorem states that two sets of cardinality 1 are disjoint iff their union has cardinality 2.

Whitehead and Russell define 1 as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 9611), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 9643. We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.)

Theorem dju1p1e2 9814 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)

Assertion
Ref Expression
pm54.43 ((𝐴 ≈ 1o𝐵 ≈ 1o) → ((𝐴𝐵) = ∅ ↔ (𝐴𝐵) ≈ 2o))

Proof of Theorem pm54.43
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1oex 8238 . . . . . . 7 1o ∈ V
21ensn1 8719 . . . . . 6 {1o} ≈ 1o
32ensymi 8703 . . . . 5 1o ≈ {1o}
4 entr 8705 . . . . 5 ((𝐵 ≈ 1o ∧ 1o ≈ {1o}) → 𝐵 ≈ {1o})
53, 4mpan2 691 . . . 4 (𝐵 ≈ 1o𝐵 ≈ {1o})
6 1on 8232 . . . . . . . 8 1o ∈ On
76onirri 6340 . . . . . . 7 ¬ 1o ∈ 1o
8 disjsn 4643 . . . . . . 7 ((1o ∩ {1o}) = ∅ ↔ ¬ 1o ∈ 1o)
97, 8mpbir 234 . . . . . 6 (1o ∩ {1o}) = ∅
10 unen 8748 . . . . . 6 (((𝐴 ≈ 1o𝐵 ≈ {1o}) ∧ ((𝐴𝐵) = ∅ ∧ (1o ∩ {1o}) = ∅)) → (𝐴𝐵) ≈ (1o ∪ {1o}))
119, 10mpanr2 704 . . . . 5 (((𝐴 ≈ 1o𝐵 ≈ {1o}) ∧ (𝐴𝐵) = ∅) → (𝐴𝐵) ≈ (1o ∪ {1o}))
1211ex 416 . . . 4 ((𝐴 ≈ 1o𝐵 ≈ {1o}) → ((𝐴𝐵) = ∅ → (𝐴𝐵) ≈ (1o ∪ {1o})))
135, 12sylan2 596 . . 3 ((𝐴 ≈ 1o𝐵 ≈ 1o) → ((𝐴𝐵) = ∅ → (𝐴𝐵) ≈ (1o ∪ {1o})))
14 df-2o 8226 . . . . 5 2o = suc 1o
15 df-suc 6239 . . . . 5 suc 1o = (1o ∪ {1o})
1614, 15eqtri 2767 . . . 4 2o = (1o ∪ {1o})
1716breq2i 5077 . . 3 ((𝐴𝐵) ≈ 2o ↔ (𝐴𝐵) ≈ (1o ∪ {1o}))
1813, 17syl6ibr 255 . 2 ((𝐴 ≈ 1o𝐵 ≈ 1o) → ((𝐴𝐵) = ∅ → (𝐴𝐵) ≈ 2o))
19 en1 8723 . . 3 (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
20 en1 8723 . . 3 (𝐵 ≈ 1o ↔ ∃𝑦 𝐵 = {𝑦})
21 sneq 4567 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → {𝑥} = {𝑦})
2221uneq2d 4093 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ({𝑥} ∪ {𝑥}) = ({𝑥} ∪ {𝑦}))
23 unidm 4082 . . . . . . . . . . . . . 14 ({𝑥} ∪ {𝑥}) = {𝑥}
2422, 23eqtr3di 2795 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) = {𝑥})
25 vex 3426 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2625ensn1 8719 . . . . . . . . . . . . . 14 {𝑥} ≈ 1o
27 1sdom2 8904 . . . . . . . . . . . . . 14 1o ≺ 2o
28 ensdomtr 8807 . . . . . . . . . . . . . 14 (({𝑥} ≈ 1o ∧ 1o ≺ 2o) → {𝑥} ≺ 2o)
2926, 27, 28mp2an 692 . . . . . . . . . . . . 13 {𝑥} ≺ 2o
3024, 29eqbrtrdi 5108 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) ≺ 2o)
31 sdomnen 8682 . . . . . . . . . . . 12 (({𝑥} ∪ {𝑦}) ≺ 2o → ¬ ({𝑥} ∪ {𝑦}) ≈ 2o)
3230, 31syl 17 . . . . . . . . . . 11 (𝑥 = 𝑦 → ¬ ({𝑥} ∪ {𝑦}) ≈ 2o)
3332necon2ai 2972 . . . . . . . . . 10 (({𝑥} ∪ {𝑦}) ≈ 2o𝑥𝑦)
34 disjsn2 4644 . . . . . . . . . 10 (𝑥𝑦 → ({𝑥} ∩ {𝑦}) = ∅)
3533, 34syl 17 . . . . . . . . 9 (({𝑥} ∪ {𝑦}) ≈ 2o → ({𝑥} ∩ {𝑦}) = ∅)
3635a1i 11 . . . . . . . 8 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (({𝑥} ∪ {𝑦}) ≈ 2o → ({𝑥} ∩ {𝑦}) = ∅))
37 uneq12 4088 . . . . . . . . 9 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴𝐵) = ({𝑥} ∪ {𝑦}))
3837breq1d 5079 . . . . . . . 8 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴𝐵) ≈ 2o ↔ ({𝑥} ∪ {𝑦}) ≈ 2o))
39 ineq12 4138 . . . . . . . . 9 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴𝐵) = ({𝑥} ∩ {𝑦}))
4039eqeq1d 2741 . . . . . . . 8 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴𝐵) = ∅ ↔ ({𝑥} ∩ {𝑦}) = ∅))
4136, 38, 403imtr4d 297 . . . . . . 7 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴𝐵) ≈ 2o → (𝐴𝐵) = ∅))
4241ex 416 . . . . . 6 (𝐴 = {𝑥} → (𝐵 = {𝑦} → ((𝐴𝐵) ≈ 2o → (𝐴𝐵) = ∅)))
4342exlimdv 1941 . . . . 5 (𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴𝐵) ≈ 2o → (𝐴𝐵) = ∅)))
4443exlimiv 1938 . . . 4 (∃𝑥 𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴𝐵) ≈ 2o → (𝐴𝐵) = ∅)))
4544imp 410 . . 3 ((∃𝑥 𝐴 = {𝑥} ∧ ∃𝑦 𝐵 = {𝑦}) → ((𝐴𝐵) ≈ 2o → (𝐴𝐵) = ∅))
4619, 20, 45syl2anb 601 . 2 ((𝐴 ≈ 1o𝐵 ≈ 1o) → ((𝐴𝐵) ≈ 2o → (𝐴𝐵) = ∅))
4718, 46impbid 215 1 ((𝐴 ≈ 1o𝐵 ≈ 1o) → ((𝐴𝐵) = ∅ ↔ (𝐴𝐵) ≈ 2o))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wex 1787  wcel 2112  wne 2942  cun 3880  cin 3881  c0 4253  {csn 4557   class class class wbr 5069  suc csuc 6235  1oc1o 8218  2oc2o 8219  cen 8646  csdm 8648
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-br 5070  df-opab 5132  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-om 7666  df-1o 8225  df-2o 8226  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652
This theorem is referenced by:  pr2nelem  9645  dju1p1e2  9814
  Copyright terms: Public domain W3C validator