Theorem pm54.43 6243

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 6220), 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 6242. 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 6346 shows the derivation of 1+1=2 for cardinal numbers from this theorem.

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 5364	. . . . . . 7 |- 1o e. On
2	1	elexi 2374	. . . . . 6 |- 1o e. _V
3	2	ensn1 5698	. . . . . 6 |- {1o} ~~ 1o
4	2, 3	ensymi 5687	. . . . 5 |- 1o ~~ {1o}
5		entr 5688	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
6	4, 5	mpan2 678	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
7	1	onirri 3798	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3137	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
9	7, 8	mpbir 218	. . . . . 6 |- (1o i^i {1o}) = (/)
10		unen 5712	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
11	9, 10	mpanr2 691	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
12	11	ex 448	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
13	6, 12	sylan2 483	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 5358	. . . . 5 |- 2o = suc 1o
15		df-suc 3700	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 1980	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 3384	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 237	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		en1 5701	. . 3 |- (A ~~ 1o <-> E.x A = {x})
20		en1 5701	. . 3 |- (B ~~ 1o <-> E.y B = {y})
21		unidm 2802	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22		sneq 3104	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
23	22	uneq2d 2813	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
24	21, 23	syl5reqr 2007	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25		vex 2368	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 5698	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
27		1sdom2 5864	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 5752	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
29	26, 27, 28	mp2an 679	. . . . . . . . . . . . 13 |- {x} ~< 2o
30	24, 29	syl6eqbr 3413	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31		sdomnen 5658	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
32	30, 31	syl 14	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
33	32	necon2ai 2121	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34		disjsn2 3138	. . . . . . . . . 10 |- (x =/= y -> ({x} i^i {y}) = (/))
35	33, 34	syl 14	. . . . . . . . 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 2808	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
38	37	breq1d 3386	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39		ineq12 2845	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
40	39	eqeq1d 1968	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
41	36, 38, 40	3imtr4d 278	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
42	41	ex 448	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	exlimdv 1677	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
44	43	exlimiv 1760	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
45	44	imp 443	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
46	19, 20, 45	syl2anb 488	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
47	18, 46	impbid 196	1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 189   /\ wa 382  E.wex 1380   = wceq 1457   e. wcel 1459   =/= wne 2078   u. cun 2660   i^i cin 2661  (/)c0 2926  {csn 3095   class class class wbr 3376  Oncon0 3694  suc csuc 3696  1oc1o 5350  2oc2o 5351   ~~ cen 5635   ~< csdm 5637

This theorem is referenced by:  pr2nelem 6244  pm110.643 6346  isprm2lem 9627

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-13 1465  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-rep 3462  ax-sep 3472  ax-nul 3481  ax-pow 3517  ax-pr 3541  ax-un 3811

This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3or 947  df-3an 948  df-tru 1354  df-ex 1381  df-sb 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-reu 2175  df-rab 2176  df-v 2367  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-pw 3084  df-sn 3099  df-pr 3100  df-tp 3102  df-op 3103  df-uni 3232  df-br 3377  df-opab 3431  df-tr 3446  df-eprel 3624  df-id 3627  df-po 3632  df-so 3646  df-fr 3665  df-we 3681  df-ord 3697  df-on 3698  df-suc 3700  df-xp 4014  df-rel 4015  df-cnv 4016  df-co 4017  df-dm 4018  df-rn 4019  df-res 4020  df-ima 4021  df-fun 4022  df-fn 4023  df-f 4024  df-f1 4025  df-fo 4026  df-f1o 4027  df-fv 4028  df-1o 5357  df-2o 5358  df-er 5494  df-en 5639  df-dom 5640  df-sdom 5641

Copyright terms: Public domain