Theorem pm54.43 6364

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 6340), 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 6363. 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 6458 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 5468	. . . . . . 7 |- 1o e. On
2	1	elexi 2331	. . . . . 6 |- 1o e. _V
3	2	ensn1 5809	. . . . . 6 |- {1o} ~~ 1o
4	2, 3	ensymi 5798	. . . . 5 |- 1o ~~ {1o}
5		entr 5799	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
6	4, 5	mpan2 646	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
7	1	onirri 3784	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3117	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
9	7, 8	mpbir 197	. . . . . 6 |- (1o i^i {1o}) = (/)
10		unen 5825	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
11	9, 10	mpanr2 659	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
12	11	ex 418	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
13	6, 12	sylan2 452	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 5462	. . . . 5 |- 2o = suc 1o
15		df-suc 3685	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 1937	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 3366	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 215	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		en1 5812	. . 3 |- (A ~~ 1o <-> E.x A = {x})
20		en1 5812	. . 3 |- (B ~~ 1o <-> E.y B = {y})
21		unidm 2772	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22		sneq 3084	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
23	22	uneq2d 2783	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
24	21, 23	syl5reqr 1964	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25		vex 2325	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 5809	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
27		1sdom2 5978	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 5866	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
29	26, 27, 28	mp2an 647	. . . . . . . . . . . . 13 |- {x} ~< 2o
30	24, 29	syl6eqbr 3395	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31		sdomnen 5769	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
32	30, 31	syl 14	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
33	32	necon2ai 2077	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34		disjsn2 3119	. . . . . . . . . 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 2778	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
38	37	breq1d 3368	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39		ineq12 2815	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
40	39	eqeq1d 1925	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
41	36, 38, 40	3imtr4d 256	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
42	41	ex 418	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	exlimdv 1634	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
44	43	exlimiv 1717	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
45	44	imp 413	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
46	19, 20, 45	syl2anb 457	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
47	18, 46	impbid 180	1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 173   /\ wa 356  E.wex 1334   = wceq 1413   e. wcel 1415   =/= wne 2034   u. cun 2630   i^i cin 2631  (/)c0 2898  {csn 3073   class class class wbr 3358  Oncon0 3679  suc csuc 3681  1oc1o 5454  2oc2o 5455   ~~ cen 5746   ~< csdm 5748

This theorem is referenced by:  pr2nelem 6365  pm110.643 6458  isprm2lem 9855

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797

This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  df-uni 3214  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3650  df-we 3666  df-ord 3682  df-on 3683  df-suc 3685  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 5461  df-2o 5462  df-er 5598  df-en 5750  df-dom 5751  df-sdom 5752

Copyright terms: Public domain