Theorem pm54.43 6389

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 6366), 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 6388. 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 6493 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 5507	. . . . . . 7 |- 1o e. On
2	1	elisseti 2509	. . . . . 6 |- 1o e. _V
3	2	ensn1 5812	. . . . . 6 |- {1o} ~~ 1o
4	2, 3	ensymi 5801	. . . . 5 |- 1o ~~ {1o}
5		entr 5802	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
6	4, 5	mpan2 755	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
7	1	onirri 3934	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3275	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
9	7, 8	mpbir 238	. . . . . 6 |- (1o i^i {1o}) = (/)
10		unen 5827	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
11	9, 10	mpanr2 770	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
12	11	ex 485	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
13	6, 12	sylan2 526	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 5501	. . . . 5 |- 2o = suc 1o
15		df-suc 3835	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 2112	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 3517	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 263	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		en1 5815	. . 3 |- (A ~~ 1o <-> E.x A = {x})
20		en1 5815	. . 3 |- (B ~~ 1o <-> E.y B = {y})
21		unidm 2940	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22		sneq 3242	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
23	22	uneq2d 2951	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
24	21, 23	syl5reqr 2142	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25		visset 2502	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 5812	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
27		1sdom2 5981	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 5866	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
29	26, 27, 28	mp2an 756	. . . . . . . . . . . . 13 |- {x} ~< 2o
30	24, 29	syl6eqbr 3550	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31		sdomnen 5771	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
32	30, 31	syl 13	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
33	32	necon2ai 2262	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34		disjsn2 3276	. . . . . . . . . 10 |- (x =/= y -> ({x} i^i {y}) = (/))
35	33, 34	syl 13	. . . . . . . . 9 |- (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/))
36	35	a1i 9	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> (({x} u. {y}) ~~ 2o -> ({x} i^i {y}) = (/)))
37		uneq12 2946	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
38	37	breq1d 3519	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39		ineq12 2983	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
40	39	eqeq1d 2100	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
41	36, 38, 40	3imtr4d 310	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
42	41	ex 485	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	exlimdv 1809	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
44	43	exlimiv 1892	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
45	44	imp 480	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
46	19, 20, 45	syl2anb 531	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
47	18, 46	impbid 216	1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 209   /\ wa 418  E.wex 1520   = wceq 1592   e. wcel 1594   =/= wne 2218   u. cun 2799   i^i cin 2800  (/)c0 3065  {csn 3233   class class class wbr 3509  Oncon0 3829  suc csuc 3831  1oc1o 5493  2oc2o 5494   ~~ cen 5748   ~< csdm 5750

This theorem is referenced by:  pr2nelem 6390  pm110.643 6493  isprm2lem 9898

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-13 1600  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-rep 3599  ax-sep 3609  ax-nul 3619  ax-pow 3655  ax-pr 3679  ax-un 3947

This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3or 1038  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-reu 2316  df-rab 2317  df-v 2501  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-pss 2812  df-nul 3066  df-pw 3222  df-sn 3237  df-pr 3238  df-tp 3240  df-op 3241  df-uni 3365  df-br 3510  df-opab 3568  df-tr 3583  df-eprel 3762  df-id 3765  df-po 3770  df-so 3782  df-fr 3800  df-we 3816  df-ord 3832  df-on 3833  df-suc 3835  df-xp 4151  df-rel 4152  df-cnv 4153  df-co 4154  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fun 4159  df-fn 4160  df-f 4161  df-f1 4162  df-fo 4163  df-f1o 4164  df-fv 4165  df-1o 5500  df-2o 5501  df-er 5637  df-en 5752  df-dom 5753  df-sdom 5754

Copyright terms: Public domain