pm54.43 - Metamath Proof Explorer

MPE Home Metamath Proof Explorer < Previous Next >
Nearby theorems

Mirrors > Home > MPE Home > Th. List > pm54.43 Structured version Visualization version Unicode version

Theorem pm54.43 10008

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 9975), so that their means, in our notation, which is the same as by pm54.43lem 10007. 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 10181 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)

**Assertion**
Ref	Expression
pm54.43

Proof of Theorem pm54.43

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1	1oex 8485	. . . . . . 7
2	1	ensn1 9030	. . . . . 6
3	2	ensymi 9013	. . . . 5
4	entr 9015	. . . . 5
5	3, 4	mpan2 691	. . . 4
6	1on 8487	. . . . . . . 8
7	6	onirri 6464	. . . . . . 7
8	disjsn 4685	. . . . . . 7
9	7, 8	mpbir 231	. . . . . 6
10	unen 9055	. . . . . 6
11	9, 10	mpanr2 704	. . . . 5
12	11	ex 412	. . . 4
13	5, 12	sylan2 593	. . 3
14	df-2o 8476	. . . . 5
15	df-suc 6356	. . . . 5
16	14, 15	eqtri 2757	. . . 4
17	16	breq2i 5125	. . 3
18	13, 17	imbitrrdi 252	. 2
19	en1 9033	. . 3
20	en1 9033	. . 3
21	sneq 4609	. . . . . . . . . . . . . . 15
22	21	uneq2d 4141	. . . . . . . . . . . . . 14
23	unidm 4130	. . . . . . . . . . . . . 14
24	22, 23	eqtr3di 2784	. . . . . . . . . . . . 13
25	vex 3461	. . . . . . . . . . . . . . 15
26	25	ensn1 9030	. . . . . . . . . . . . . 14
27	1sdom2 9243	. . . . . . . . . . . . . 14
28	ensdomtr 9122	. . . . . . . . . . . . . 14
29	26, 27, 28	mp2an 692	. . . . . . . . . . . . 13
30	24, 29	eqbrtrdi 5156	. . . . . . . . . . . 12
31	sdomnen 8990	. . . . . . . . . . . 12
32	30, 31	syl 17	. . . . . . . . . . 11
33	32	necon2ai 2960	. . . . . . . . . 10
34	disjsn2 4686	. . . . . . . . . 10
35	33, 34	syl 17	. . . . . . . . 9
36	35	a1i 11	. . . . . . . 8
37	uneq12 4136	. . . . . . . . 9
38	37	breq1d 5127	. . . . . . . 8
39	ineq12 4188	. . . . . . . . 9
40	39	eqeq1d 2736	. . . . . . . 8
41	36, 38, 40	3imtr4d 294	. . . . . . 7
42	41	ex 412	. . . . . 6
43	42	exlimdv 1932	. . . . 5
44	43	exlimiv 1929	. . . 4
45	44	imp 406	. . 3
46	19, 20, 45	syl2anb 598	. 2
47	18, 46	impbid 212	1

Colors of variables: wff setvar class

Syntax hints: wn 3 wi 4 wb 206 wa 395 wceq 1539 wex 1778 wcel 2107 wne 2931 cun 3922 cin 3923 c0 4306 csn 4599 class class class wbr 5117 csuc 6352 c1o 8468 c2o 8469 cen 8951 csdm 8953

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-sep 5264 ax-nul 5274 ax-pow 5333 ax-pr 5400 ax-un 7724

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-reu 3358 df-rab 3414 df-v 3459 df-dif 3927 df-un 3929 df-in 3931 df-ss 3941 df-pss 3944 df-nul 4307 df-if 4499 df-pw 4575 df-sn 4600 df-pr 4602 df-op 4606 df-uni 4882 df-br 5118 df-opab 5180 df-tr 5228 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-ord 6353 df-on 6354 df-suc 6356 df-iota 6481 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-1o 8475 df-2o 8476 df-er 8714 df-en 8955 df-dom 8956 df-sdom 8957

This theorem is referenced by: pr2nelemOLD 10010 dju1p1e2 10181