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 10037

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 10004), so that their means, in our notation, which is the same as by pm54.43lem 10036. 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 10210 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 8512	. . . . . . 7
2	1	ensn1 9057	. . . . . 6
3	2	ensymi 9040	. . . . 5
4	entr 9042	. . . . 5
5	3, 4	mpan2 691	. . . 4
6	1on 8514	. . . . . . . 8
7	6	onirri 6495	. . . . . . 7
8	disjsn 4709	. . . . . . 7
9	7, 8	mpbir 231	. . . . . 6
10	unen 9082	. . . . . 6
11	9, 10	mpanr2 704	. . . . 5
12	11	ex 412	. . . 4
13	5, 12	sylan2 593	. . 3
14	df-2o 8503	. . . . 5
15	df-suc 6388	. . . . 5
16	14, 15	eqtri 2764	. . . 4
17	16	breq2i 5149	. . 3
18	13, 17	imbitrrdi 252	. 2
19	en1 9060	. . 3
20	en1 9060	. . 3
21	sneq 4634	. . . . . . . . . . . . . . 15
22	21	uneq2d 4167	. . . . . . . . . . . . . 14
23	unidm 4156	. . . . . . . . . . . . . 14
24	22, 23	eqtr3di 2791	. . . . . . . . . . . . 13
25	vex 3483	. . . . . . . . . . . . . . 15
26	25	ensn1 9057	. . . . . . . . . . . . . 14
27	1sdom2 9272	. . . . . . . . . . . . . 14
28	ensdomtr 9149	. . . . . . . . . . . . . 14
29	26, 27, 28	mp2an 692	. . . . . . . . . . . . 13
30	24, 29	eqbrtrdi 5180	. . . . . . . . . . . 12
31	sdomnen 9017	. . . . . . . . . . . 12
32	30, 31	syl 17	. . . . . . . . . . 11
33	32	necon2ai 2969	. . . . . . . . . 10
34	disjsn2 4710	. . . . . . . . . 10
35	33, 34	syl 17	. . . . . . . . 9
36	35	a1i 11	. . . . . . . 8
37	uneq12 4162	. . . . . . . . 9
38	37	breq1d 5151	. . . . . . . 8
39	ineq12 4214	. . . . . . . . 9
40	39	eqeq1d 2738	. . . . . . . 8
41	36, 38, 40	3imtr4d 294	. . . . . . 7
42	41	ex 412	. . . . . 6
43	42	exlimdv 1933	. . . . 5
44	43	exlimiv 1930	. . . 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 1540 wex 1779 wcel 2108 wne 2939 cun 3948 cin 3949 c0 4332 csn 4624 class class class wbr 5141 csuc 6384 c1o 8495 c2o 8496 cen 8978 csdm 8980

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5294 ax-nul 5304 ax-pow 5363 ax-pr 5430 ax-un 7751

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4906 df-br 5142 df-opab 5204 df-tr 5258 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-ord 6385 df-on 6386 df-suc 6388 df-iota 6512 df-fun 6561 df-fn 6562 df-f 6563 df-f1 6564 df-fo 6565 df-f1o 6566 df-fv 6567 df-1o 8502 df-2o 8503 df-er 8741 df-en 8982 df-dom 8983 df-sdom 8984

This theorem is referenced by: pr2nelemOLD 10039 dju1p1e2 10210