Theorem pm54.43 10025

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 9992), 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 10024. 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 10198 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

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

Step	Hyp	Ref	Expression
1		1oex 8502	. . . . . . 7 |- 1o e. _V
2	1	ensn1 9047	. . . . . 6 |- { 1o } ~~ 1o
3	2	ensymi 9030	. . . . 5 |- 1o ~~ { 1o }
4		entr 9032	. . . . 5 |- ( ( B ~~ 1o /\ 1o ~~ { 1o } ) -> B ~~ { 1o } )
5	3, 4	mpan2 691	. . . 4 |- ( B ~~ 1o -> B ~~ { 1o } )
6		1on 8504	. . . . . . . 8 |- 1o e. On
7	6	onirri 6488	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 4715	. . . . . . 7 |- ( ( 1o i^i { 1o } ) = (/) <-> -. 1o e. 1o )
9	7, 8	mpbir 231	. . . . . 6 |- ( 1o i^i { 1o } ) = (/)
10		unen 9072	. . . . . 6 |- ( ( ( A ~~ 1o /\ B ~~ { 1o } ) /\ ( ( A i^i B ) = (/) /\ ( 1o i^i { 1o } ) = (/) ) ) -> ( A u. B ) ~~ ( 1o u. { 1o } ) )
11	9, 10	mpanr2 704	. . . . 5 |- ( ( ( A ~~ 1o /\ B ~~ { 1o } ) /\ ( A i^i B ) = (/) ) -> ( A u. B ) ~~ ( 1o u. { 1o } ) )
12	11	ex 412	. . . 4 |- ( ( A ~~ 1o /\ B ~~ { 1o } ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ ( 1o u. { 1o } ) ) )
13	5, 12	sylan2 593	. . 3 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ ( 1o u. { 1o } ) ) )
14		df-2o 8493	. . . . 5 |- 2o = suc 1o
15		df-suc 6381	. . . . 5 |- suc 1o = ( 1o u. { 1o } )
16	14, 15	eqtri 2762	. . . 4 |- 2o = ( 1o u. { 1o } )
17	16	breq2i 5154	. . 3 |- ( ( A u. B ) ~~ 2o <-> ( A u. B ) ~~ ( 1o u. { 1o } ) )
18	13, 17	imbitrrdi 252	. 2 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) -> ( A u. B ) ~~ 2o ) )
19		en1 9050	. . 3 |- ( A ~~ 1o <-> E. x A = { x } )
20		en1 9050	. . 3 |- ( B ~~ 1o <-> E. y B = { y } )
21		sneq 4640	. . . . . . . . . . . . . . 15 |- ( x = y -> { x } = { y } )
22	21	uneq2d 4177	. . . . . . . . . . . . . 14 |- ( x = y -> ( { x } u. { x } ) = ( { x } u. { y } ) )
23		unidm 4166	. . . . . . . . . . . . . 14 |- ( { x } u. { x } ) = { x }
24	22, 23	eqtr3di 2789	. . . . . . . . . . . . 13 |- ( x = y -> ( { x } u. { y } ) = { x } )
25		vex 3481	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 9047	. . . . . . . . . . . . . 14 |- { x } ~~ 1o
27		1sdom2 9261	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 9139	. . . . . . . . . . . . . 14 |- ( ( { x } ~~ 1o /\ 1o ~< 2o ) -> { x } ~< 2o )
29	26, 27, 28	mp2an 692	. . . . . . . . . . . . 13 |- { x } ~< 2o
30	24, 29	eqbrtrdi 5185	. . . . . . . . . . . 12 |- ( x = y -> ( { x } u. { y } ) ~< 2o )
31		sdomnen 9007	. . . . . . . . . . . 12 |- ( ( { x } u. { y } ) ~< 2o -> -. ( { x } u. { y } ) ~~ 2o )
32	30, 31	syl 17	. . . . . . . . . . 11 |- ( x = y -> -. ( { x } u. { y } ) ~~ 2o )
33	32	necon2ai 2967	. . . . . . . . . 10 |- ( ( { x } u. { y } ) ~~ 2o -> x =/= y )
34		disjsn2 4716	. . . . . . . . . 10 |- ( x =/= y -> ( { x } i^i { y } ) = (/) )
35	33, 34	syl 17	. . . . . . . . 9 |- ( ( { x } u. { y } ) ~~ 2o -> ( { x } i^i { y } ) = (/) )
36	35	a1i 11	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( { x } u. { y } ) ~~ 2o -> ( { x } i^i { y } ) = (/) ) )
37		uneq12 4172	. . . . . . . . 9 |- ( ( A = { x } /\ B = { y } ) -> ( A u. B ) = ( { x } u. { y } ) )
38	37	breq1d 5156	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( A u. B ) ~~ 2o <-> ( { x } u. { y } ) ~~ 2o ) )
39		ineq12 4222	. . . . . . . . 9 |- ( ( A = { x } /\ B = { y } ) -> ( A i^i B ) = ( { x } i^i { y } ) )
40	39	eqeq1d 2736	. . . . . . . 8 |- ( ( A = { x } /\ B = { y } ) -> ( ( A i^i B ) = (/) <-> ( { x } i^i { y } ) = (/) ) )
41	36, 38, 40	3imtr4d 294	. . . . . . 7 |- ( ( A = { x } /\ B = { y } ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
42	41	ex 412	. . . . . 6 |- ( A = { x } -> ( B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
43	42	exlimdv 1930	. . . . 5 |- ( A = { x } -> ( E. y B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
44	43	exlimiv 1927	. . . 4 |- ( E. x A = { x } -> ( E. y B = { y } -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) ) )
45	44	imp 406	. . 3 |- ( ( E. x A = { x } /\ E. y B = { y } ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
46	19, 20, 45	syl2anb 598	. 2 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A u. B ) ~~ 2o -> ( A i^i B ) = (/) ) )
47	18, 46	impbid 212	1 |- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) <-> ( A u. B ) ~~ 2o ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 206   /\ wa 395   = wceq 1536   E.wex 1775   e. wcel 2105   =/= wne 2937   u. cun 3960   i^i cin 3961   (/)c0 4338   {csn 4630   class class class wbr 5146   suc csuc 6377   1oc1o 8485   2oc2o 8486   ~~ cen 8968   ~< csdm 8970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5297  ax-nul 5304  ax-pow 5363  ax-pr 5427  ax-un 7741

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5147  df-opab 5209  df-tr 5264  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5630  df-we 5632  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6378  df-on 6379  df-suc 6381  df-iota 6505  df-fun 6554  df-fn 6555  df-f 6556  df-f1 6557  df-fo 6558  df-f1o 6559  df-fv 6560  df-1o 8492  df-2o 8493  df-er 8731  df-en 8972  df-dom 8973  df-sdom 8974

This theorem is referenced by:  pr2nelemOLD  10027  dju1p1e2  10198