Theorem pm54.43 6303

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 6280), 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 6302. 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 6397 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 5420	. . . . . . 7 |- 1o e. On
2	1	elexi 2344	. . . . . 6 |- 1o e. _V
3	2	ensn1 5754	. . . . . 6 |- {1o} ~~ 1o
4	2, 3	ensymi 5743	. . . . 5 |- 1o ~~ {1o}
5		entr 5744	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
6	4, 5	mpan2 651	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
7	1	onirri 3786	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3122	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
9	7, 8	mpbir 198	. . . . . 6 |- (1o i^i {1o}) = (/)
10		unen 5769	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
11	9, 10	mpanr2 664	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
12	11	ex 423	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
13	6, 12	sylan2 457	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 5414	. . . . 5 |- 2o = suc 1o
15		df-suc 3688	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 1949	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 3370	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 217	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		en1 5757	. . 3 |- (A ~~ 1o <-> E.x A = {x})
20		en1 5757	. . 3 |- (B ~~ 1o <-> E.y B = {y})
21		unidm 2778	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22		sneq 3089	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
23	22	uneq2d 2789	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
24	21, 23	syl5reqr 1976	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25		vex 2338	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 5754	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
27		1sdom2 5921	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 5809	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
29	26, 27, 28	mp2an 652	. . . . . . . . . . . . 13 |- {x} ~< 2o
30	24, 29	syl6eqbr 3399	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31		sdomnen 5714	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
32	30, 31	syl 14	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
33	32	necon2ai 2090	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34		disjsn2 3124	. . . . . . . . . 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 2784	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
38	37	breq1d 3372	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39		ineq12 2821	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
40	39	eqeq1d 1937	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
41	36, 38, 40	3imtr4d 258	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
42	41	ex 423	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	exlimdv 1646	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
44	43	exlimiv 1729	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
45	44	imp 418	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
46	19, 20, 45	syl2anb 462	. 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 360  E.wex 1346   = wceq 1425   e. wcel 1427   =/= wne 2047   u. cun 2636   i^i cin 2637  (/)c0 2903  {csn 3078   class class class wbr 3362  Oncon0 3682  suc csuc 3684  1oc1o 5406  2oc2o 5407   ~~ cen 5691   ~< csdm 5693

This theorem is referenced by:  pr2nelem 6304  pm110.643 6397  isprm2lem 9754

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3448  ax-sep 3458  ax-nul 3467  ax-pow 3503  ax-pr 3527  ax-un 3799

This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-dif 2641  df-un 2643  df-in 2645  df-ss 2647  df-pss 2649  df-nul 2904  df-pw 3067  df-sn 3084  df-pr 3085  df-tp 3086  df-op 3087  df-uni 3218  df-br 3363  df-opab 3417  df-tr 3432  df-eprel 3612  df-id 3615  df-po 3620  df-so 3634  df-fr 3653  df-we 3669  df-ord 3685  df-on 3686  df-suc 3688  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-1o 5413  df-2o 5414  df-er 5550  df-en 5695  df-dom 5696  df-sdom 5697

Copyright terms: Public domain