Theorem pm54.43 5472

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 5779), so that their A e. 1 means, in our notation, A e. {x | (card` x) = 1o} i.e. (card` A) = 1o (by elab 2236) i.e. A ~~ 1o (by carden 5777 and cardnn 5666). 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 5868 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 4993	. . . . . . . 8 |- 1o e. On
2	1	onirri 3587	. . . . . . 7 |- -. 1o e. 1o
3		disjsn 2911	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
4	2, 3	mpbir 206	. . . . . 6 |- (1o i^i {1o}) = (/)
5		unen 5304	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
6	4, 5	mpanr2 773	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
7	6	ex 400	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
8	1	elisseti 2134	. . . . . 6 |- 1o e. _V
9	8	ensn1 5294	. . . . . 6 |- {1o} ~~ 1o
10	8, 9	ensymi 5283	. . . . 5 |- 1o ~~ {1o}
11		entr 5284	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
12	10, 11	mpan2 757	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
13	7, 12	sylan2 498	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 4989	. . . . 5 |- 2o = suc 1o
15		df-suc 3478	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 1745	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 3166	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 229	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		sneq 2878	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
20	19	uneq2d 2585	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
21		unidm 2575	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22	20, 21	syl5reqr 1780	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
23		visset 2128	. . . . . . . . . . . . . . 15 |- x e. _V
24	23	ensn1 5294	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
25		1sdom2 5429	. . . . . . . . . . . . . 14 |- 1o ~< 2o
26		ensdomtr 5345	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
27	24, 25, 26	mp2an 758	. . . . . . . . . . . . 13 |- {x} ~< 2o
28	22, 27	syl6eqbr 3194	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
29		sdomnen 5257	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
30	28, 29	syl 12	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
31	30	necon2ai 1886	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
32		disjsn2 2913	. . . . . . . . . 10 |- (x =/= y -> ({x} i^i {y}) = (/))
33	31, 32	syl 12	. . . . . . . . 9 |- (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/))
34	33	a1i 8	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/)))
35		uneq12 2580	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
36	35	breq1d 3168	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
37		ineq12 2618	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
38	37	eqeq1d 1729	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
39	34, 36, 38	3imtr4d 599	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
40	39	ex 400	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
41	40	19.23adv 1422	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
42	41	19.23aiv 1512	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	imp 375	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
44		en1 5296	. . 3 |- (A ~~ 1o <-> E.x A = {x})
45		en1 5296	. . 3 |- (B ~~ 1o <-> E.y B = {y})
46	43, 44, 45	syl2anb 502	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
47	18, 46	impbid 571	1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 162   /\ wa 239   = wceq 1136   e. wcel 1138  E.wex 1164   =/= wne 1854   u. cun 2424   i^i cin 2425  (/)c0 2701  {csn 2868   class class class wbr 3158  Oncon0 3472  suc csuc 3474  1oc1o 4983  2oc2o 4984   ~~ cen 5234   ~< csdm 5236

This theorem is referenced by:  pm110.643 5868  isprm2lem 13566  unpde2eg2 14136

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-suc 3478  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-1o 4988  df-2o 4989  df-er 5129  df-en 5238  df-dom 5239  df-sdom 5240

Copyright terms: Public domain