Theorem pm54.43 7629

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 7597), so that their A e. 1 means, in our notation, A e. { x | ( card ` x ) = 1o } which is the same as A ~~ 1o by pm54.43lem 7628. 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 pm110.643 7799 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)

Assertion

Ref	Expression
pm54.43	|- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) <-> ( A u. B ) ~~ 2o ) )

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

Proof of Theorem pm54.43

Step	Hyp	Ref	Expression
1		1on 6482	. . . . . . . 8 |- 1o e. On
2	1	elexi 2799	. . . . . . 7 |- 1o e. _V
3	2	ensn1 6921	. . . . . 6 |- { 1o } ~~ 1o
4	3	ensymi 6907	. . . . 5 |- 1o ~~ { 1o }
5		entr 6909	. . . . 5 |- ( ( B ~~ 1o /\ 1o ~~ { 1o } ) -> B ~~ { 1o } )
6	4, 5	mpan2 654	. . . 4 |- ( B ~~ 1o -> B ~~ { 1o } )
7	1	onirri 4499	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3695	. . . . . . 7 |- ( ( 1o i^i { 1o } ) = (/) <-> -. 1o e. 1o )
9	7, 8	mpbir 202	. . . . . 6 |- ( 1o i^i { 1o } ) = (/)
10		unen 6939	. . . . . 6 |- ( ( ( A ~~ 1o /\ B ~~ { 1o } ) /\ ( ( A i^i B ) = (/) /\ ( 1o i^i { 1o } ) = (/) ) ) -> ( A u. B ) ~~ ( 1o u. { 1o } ) )
11	9, 10	mpanr2 667	. . . . 5 |- ( ( ( A ~~ 1o /\ B ~~ { 1o } ) /\ ( A i^i B ) = (/) ) -> ( A u. B ) ~~ ( 1o u. { 1o } ) )
12	11	ex 425	. . . 4 |- ( ( A ~~ 1o /\ B ~~ { 1o } ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ ( 1o u. { 1o } ) ) )
13	6, 12	sylan2 462	. . 3 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ ( 1o u. { 1o } ) ) )
14		df-2o 6476	. . . . 5 |- 2o = suc 1o
15		df-suc 4398	. . . . 5 |- suc 1o = ( 1o u. { 1o } )
16	14, 15	eqtri 2305	. . . 4 |- 2o = ( 1o u. { 1o } )
17	16	breq2i 4033	. . 3 |- ( ( A u. B ) ~~ 2o <-> ( A u. B ) ~~ ( 1o u. { 1o } ) )
18	13, 17	syl6ibr 220	. 2 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ 2o ) )
19		en1 6924	. . 3 |- ( A ~~ 1o <-> E. x A = { x } )
20		en1 6924	. . 3 |- ( B ~~ 1o <-> E. y B = { y } )
21		unidm 3320	. . . . . . . . . . . . . 14 |- ( { x } u. { x } ) = { x }
22		sneq 3653	. . . . . . . . . . . . . . 15 |- ( x = y -> { x } = { y } )
23	22	uneq2d 3331	. . . . . . . . . . . . . 14 |- ( x = y -> ( { x } u. { x } ) = ( { x } u. { y } ) )
24	21, 23	syl5reqr 2332	. . . . . . . . . . . . 13 |- ( x = y -> ( { x } u. { y } ) = { x } )
25		vex 2793	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 6921	. . . . . . . . . . . . . 14 |- { x } ~~ 1o
27		1sdom2 7057	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 6993	. . . . . . . . . . . . . 14 |- ( ( { x } ~~ 1o /\ 1o ~< 2o ) -> { x } ~< 2o )
29	26, 27, 28	mp2an 655	. . . . . . . . . . . . 13 |- { x } ~< 2o
30	24, 29	syl6eqbr 4062	. . . . . . . . . . . 12 |- ( x = y -> ( { x } u. { y } ) ~< 2o )
31		sdomnen 6886	. . . . . . . . . . . 12 |- ( ( { x } u. { y } ) ~< 2o -> -. ( { x } u. { y } ) ~~ 2o )
32	30, 31	syl 17	. . . . . . . . . . 11 |- ( x = y -> -. ( { x } u. { y } ) ~~ 2o )
33	32	necon2ai 2493	. . . . . . . . . 10 |- ( ( { x } u. { y } ) ~~ 2o -> x =/= y )
34		disjsn2 3696	. . . . . . . . . 10 |- ( x =/= y -> ( { x } i^i { y } ) = (/) )
35	33, 34	syl 17	. . . . . . . . 9 |- ( ( { x } u. { y } ) ~~ 2o -> ( { x } i^i { y } ) = (/) )
36	35	a1i 12	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( { x } u. { y } ) ~~ 2o -> ( { x } i^i { y } ) = (/) ) )
37		uneq12 3326	. . . . . . . . 9 |- ( ( A = { x } /\ B = { y } ) -> ( A u. B ) = ( { x } u. { y } ) )
38	37	breq1d 4035	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( A u. B ) ~~ 2o <-> ( { x } u. { y } ) ~~ 2o ) )
39		ineq12 3367	. . . . . . . . 9 |- ( ( A = { x } /\ B = { y } ) -> ( A i^i B ) = ( { x } i^i { y } ) )
40	39	eqeq1d 2293	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( A i^i B ) = (/) <-> ( { x } i^i { y } ) = (/) ) )
41	36, 38, 40	3imtr4d 261	. . . . . . 7 |- ( ( A = { x } /\ B = { y } ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
42	41	ex 425	. . . . . 6 |- ( A = { x } -> ( B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
43	42	exlimdv 1665	. . . . 5 |- ( A = { x } -> ( E. y B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
44	43	exlimiv 1667	. . . 4 |- ( E. x A = { x } -> ( E. y B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
45	44	imp 420	. . 3 |- ( ( E. x A = { x } /\ E. y B = { y } ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
46	19, 20, 45	syl2anb 467	. 2 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
47	18, 46	impbid 185	1 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) <-> ( A u. B ) ~~ 2o ) )

Syntax hints:   -. wn 5   -> wi 6   <-> wb 178   /\ wa 360   E.wex 1529   = wceq 1624   e. wcel 1685   =/= wne 2448   u. cun 3152   i^i cin 3153   (/)c0 3457   {csn 3642   class class class wbr 4025   Oncon0 4392   suc csuc 4394   1oc1o 6468   2oc2o 6469   ~~ cen 6856   ~< csdm 6858

This theorem is referenced by:  pr2nelem  7630  pm110.643  7799  isprm2lem  12760

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4188  ax-pr 4214  ax-un 4512

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5224  df-fn 5225  df-f 5226  df-f1 5227  df-fo 5228  df-f1o 5229  df-fv 5230  df-1o 6475  df-2o 6476  df-er 6656  df-en 6860  df-dom 6861  df-sdom 6862