Theorem pm54.43 7159

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 7127), 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 7158. 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 7310 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 ) )

Proof of Theorem pm54.43

Step	Hyp	Ref	Expression
1		1on 5985	. . . . . . . 8 |- 1o e. On
2	1	elexi 2521	. . . . . . 7 |- 1o e. _V
3	2	ensn1 6406	. . . . . 6 |- { 1o } ~~ 1o
4	3	ensymi 6393	. . . . 5 |- 1o ~~ { 1o }
5		entr 6394	. . . . 5 |- ( ( B ~~ 1o /\ 1o ~~ { 1o } ) -> B ~~ { 1o } )
6	4, 5	mpan2 647	. . . 4 |- ( B ~~ 1o -> B ~~ { 1o } )
7	1	onirri 4092	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3347	. . . . . . 7 |- ( ( 1o i^i { 1o } ) = (/) <-> -. 1o e. 1o )
9	7, 8	mpbir 198	. . . . . 6 |- ( 1o i^i { 1o } ) = (/)
10		unen 6424	. . . . . 6 |- ( ( ( A ~~ 1o /\ B ~~ { 1o } ) /\ ( ( A i^i B ) = (/) /\ ( 1o i^i { 1o } ) = (/) ) ) -> ( A u. B ) ~~ ( 1o u. { 1o } ) )
11	9, 10	mpanr2 660	. . . . 5 |- ( ( ( A ~~ 1o /\ B ~~ { 1o } ) /\ ( A i^i B ) = (/) ) -> ( A u. B ) ~~ ( 1o u. { 1o } ) )
12	11	ex 420	. . . 4 |- ( ( A ~~ 1o /\ B ~~ { 1o } ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ ( 1o u. { 1o } ) ) )
13	6, 12	sylan2 455	. . 3 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ ( 1o u. { 1o } ) ) )
14		df-2o 5979	. . . . 5 |- 2o = suc 1o
15		df-suc 3993	. . . . 5 |- suc 1o = ( 1o u. { 1o } )
16	14, 15	eqtri 2120	. . . 4 |- 2o = ( 1o u. { 1o } )
17	16	breq2i 3638	. . 3 |- ( ( A u. B ) ~~ 2o <-> ( A u. B ) ~~ ( 1o u. { 1o } ) )
18	13, 17	syl6ibr 216	. 2 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ 2o ) )
19		en1 6409	. . 3 |- ( A ~~ 1o <-> E. x A = { x } )
20		en1 6409	. . 3 |- ( B ~~ 1o <-> E. y B = { y } )
21		unidm 2977	. . . . . . . . . . . . . 14 |- ( { x } u. { x } ) = { x }
22		sneq 3305	. . . . . . . . . . . . . . 15 |- ( x = y -> { x } = { y } )
23	22	uneq2d 2988	. . . . . . . . . . . . . 14 |- ( x = y -> ( { x } u. { x } ) = ( { x } u. { y } ) )
24	21, 23	syl5reqr 2147	. . . . . . . . . . . . 13 |- ( x = y -> ( { x } u. { y } ) = { x } )
25		vex 2515	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 6406	. . . . . . . . . . . . . 14 |- { x } ~~ 1o
27		1sdom2 6589	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 6478	. . . . . . . . . . . . . 14 |- ( ( { x } ~~ 1o /\ 1o ~< 2o ) -> { x } ~< 2o )
29	26, 27, 28	mp2an 648	. . . . . . . . . . . . 13 |- { x } ~< 2o
30	24, 29	syl6eqbr 3667	. . . . . . . . . . . 12 |- ( x = y -> ( { x } u. { y } ) ~< 2o )
31		sdomnen 6372	. . . . . . . . . . . 12 |- ( ( { x } u. { y } ) ~< 2o -> -. ( { x } u. { y } ) ~~ 2o )
32	30, 31	syl 15	. . . . . . . . . . 11 |- ( x = y -> -. ( { x } u. { y } ) ~~ 2o )
33	32	necon2ai 2263	. . . . . . . . . 10 |- ( ( { x } u. { y } ) ~~ 2o -> x =/= y )
34		disjsn2 3348	. . . . . . . . . 10 |- ( x =/= y -> ( { x } i^i { y } ) = (/) )
35	33, 34	syl 15	. . . . . . . . 9 |- ( ( { x } u. { y } ) ~~ 2o -> ( { x } i^i { y } ) = (/) )
36	35	a1i 10	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( { x } u. { y } ) ~~ 2o -> ( { x } i^i { y } ) = (/) ) )
37		uneq12 2983	. . . . . . . . 9 |- ( ( A = { x } /\ B = { y } ) -> ( A u. B ) = ( { x } u. { y } ) )
38	37	breq1d 3640	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( A u. B ) ~~ 2o <-> ( { x } u. { y } ) ~~ 2o ) )
39		ineq12 3022	. . . . . . . . 9 |- ( ( A = { x } /\ B = { y } ) -> ( A i^i B ) = ( { x } i^i { y } ) )
40	39	eqeq1d 2108	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( A i^i B ) = (/) <-> ( { x } i^i { y } ) = (/) ) )
41	36, 38, 40	3imtr4d 257	. . . . . . 7 |- ( ( A = { x } /\ B = { y } ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
42	41	ex 420	. . . . . 6 |- ( A = { x } -> ( B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
43	42	exlimdv 1793	. . . . 5 |- ( A = { x } -> ( E. y B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
44	43	exlimiv 1879	. . . 4 |- ( E. x A = { x } -> ( E. y B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
45	44	imp 415	. . 3 |- ( ( E. x A = { x } /\ E. y B = { y } ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
46	19, 20, 45	syl2anb 460	. 2 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
47	18, 46	impbid 181	1 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) <-> ( A u. B ) ~~ 2o ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 174   /\ wa 356   E.wex 1456   = wceq 1531   e. wcel 1533   =/= wne 2218   u. cun 2828   i^i cin 2829   (/)c0 3110   {csn 3294   class class class wbr 3630   Oncon0 3987   suc csuc 3989   1oc1o 5971   2oc2o 5972   ~~ cen 6342   ~< csdm 6344

This theorem is referenced by:  pr2nelem  7160  pm110.643  7310  isprm2lem  11924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-13 1537  ax-14 1538  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-sep 3745  ax-nul 3753  ax-pow 3789  ax-pr 3813  ax-un 4105

This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 901  df-3an 902  df-tru 1265  df-ex 1457  df-sb 1748  df-eu 1970  df-mo 1971  df-clab 2088  df-cleq 2093  df-clel 2096  df-ne 2220  df-ral 2315  df-rex 2316  df-reu 2317  df-rab 2318  df-v 2514  df-sbc 2688  df-dif 2833  df-un 2835  df-in 2837  df-ss 2841  df-pss 2843  df-nul 3111  df-if 3221  df-pw 3282  df-sn 3300  df-pr 3301  df-tp 3302  df-op 3303  df-uni 3469  df-br 3631  df-opab 3685  df-tr 3718  df-eprel 3900  df-id 3904  df-po 3909  df-so 3910  df-fr 3947  df-we 3949  df-ord 3990  df-on 3991  df-lim 3992  df-suc 3993  df-om 4268  df-xp 4314  df-rel 4315  df-cnv 4316  df-co 4317  df-dm 4318  df-rn 4319  df-res 4320  df-ima 4321  df-fun 4322  df-fn 4323  df-f 4324  df-f1 4325  df-fo 4326  df-f1o 4327  df-fv 4328  df-1o 5978  df-2o 5979  df-er 6159  df-en 6346  df-dom 6347  df-sdom 6348