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 ), so that their A e. 1 means, in our notation, A e. { x | ( cardx ) = 1o } which is the same as A ~1o by pm54.43lem . 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 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | pm54.43 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1oex | ||
2 | 1 | ensn1 | |
3 | 2 | ensymi | |
4 | entr | ||
5 | 3 4 | mpan2 | |
6 | 1on | ||
7 | 6 | onirri | |
8 | disjsn | ||
9 | 7 8 | mpbir | |
10 | unen | ||
11 | 9 10 | mpanr2 | |
12 | 11 | ex | |
13 | 5 12 | sylan2 | |
14 | df-2o | ||
15 | df-suc | ||
16 | 14 15 | eqtri | |
17 | 16 | breq2i | |
18 | 13 17 | syl6ibr | |
19 | en1 | ||
20 | en1 | ||
21 | unidm | ||
22 | sneq | ||
23 | 22 | uneq2d | |
24 | 21 23 | syl5reqr | |
25 | vex | ||
26 | 25 | ensn1 | |
27 | 1sdom2 | ||
28 | ensdomtr | ||
29 | 26 27 28 | mp2an | |
30 | 24 29 | eqbrtrdi | |
31 | sdomnen | ||
32 | 30 31 | syl | |
33 | 32 | necon2ai | |
34 | disjsn2 | ||
35 | 33 34 | syl | |
36 | 35 | a1i | |
37 | uneq12 | ||
38 | 37 | breq1d | |
39 | ineq12 | ||
40 | 39 | eqeq1d | |
41 | 36 38 40 | 3imtr4d | |
42 | 41 | ex | |
43 | 42 | exlimdv | |
44 | 43 | exlimiv | |
45 | 44 | imp | |
46 | 19 20 45 | syl2anb | |
47 | 18 46 | impbid |