Theorem pm54.43 6367

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 6344), 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 6366. 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 6471 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 5490	. . . . . . 7 |- 1o e. On
2	1	elisseti 2504	. . . . . 6 |- 1o e. _V
3	2	ensn1 5795	. . . . . 6 |- {1o} ~~ 1o
4	2, 3	ensymi 5784	. . . . 5 |- 1o ~~ {1o}
5		entr 5785	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
6	4, 5	mpan2 739	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
7	1	onirri 3927	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3268	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
9	7, 8	mpbir 238	. . . . . 6 |- (1o i^i {1o}) = (/)
10		unen 5810	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
11	9, 10	mpanr2 754	. . . . 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 5484	. . . . 5 |- 2o = suc 1o
15		df-suc 3828	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 2107	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 3510	. . 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 5798	. . 3 |- (A ~~ 1o <-> E.x A = {x})
20		en1 5798	. . 3 |- (B ~~ 1o <-> E.y B = {y})
21		unidm 2934	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22		sneq 3235	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
23	22	uneq2d 2945	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
24	21, 23	syl5reqr 2137	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25		visset 2497	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 5795	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
27		1sdom2 5964	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 5849	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
29	26, 27, 28	mp2an 740	. . . . . . . . . . . . 13 |- {x} ~< 2o
30	24, 29	syl6eqbr 3543	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31		sdomnen 5754	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
32	30, 31	syl 13	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
33	32	necon2ai 2257	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34		disjsn2 3269	. . . . . . . . . 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 2940	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
38	37	breq1d 3512	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39		ineq12 2976	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
40	39	eqeq1d 2095	. . . . . . . 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 1804	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
44	43	exlimiv 1887	. . . 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 1517   = wceq 1588   e. wcel 1590   =/= wne 2213   u. cun 2793   i^i cin 2794  (/)c0 3058  {csn 3226   class class class wbr 3502  Oncon0 3822  suc csuc 3824  1oc1o 5476  2oc2o 5477   ~~ cen 5731   ~< csdm 5733

This theorem is referenced by:  pr2nelem 6368  pm110.643 6471  isprm2lem 9847

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1513  ax-6 1514  ax-7 1515  ax-gen 1516  ax-8 1592  ax-10 1593  ax-11 1594  ax-12 1595  ax-13 1596  ax-14 1597  ax-17 1604  ax-9 1615  ax-4 1621  ax-16 1798  ax-ext 2069  ax-rep 3592  ax-sep 3602  ax-nul 3612  ax-pow 3648  ax-pr 3672  ax-un 3940

This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3or 1036  df-3an 1037  df-ex 1518  df-sb 1760  df-eu 1987  df-mo 1988  df-clab 2075  df-cleq 2080  df-clel 2083  df-ne 2215  df-ral 2309  df-rex 2310  df-reu 2311  df-rab 2312  df-v 2496  df-dif 2798  df-un 2800  df-in 2802  df-ss 2804  df-pss 2806  df-nul 3059  df-pw 3215  df-sn 3230  df-pr 3231  df-tp 3233  df-op 3234  df-uni 3358  df-br 3503  df-opab 3561  df-tr 3576  df-eprel 3755  df-id 3758  df-po 3763  df-so 3775  df-fr 3793  df-we 3809  df-ord 3825  df-on 3826  df-suc 3828  df-xp 4144  df-rel 4145  df-cnv 4146  df-co 4147  df-dm 4148  df-rn 4149  df-res 4150  df-ima 4151  df-fun 4152  df-fn 4153  df-f 4154  df-f1 4155  df-fo 4156  df-f1o 4157  df-fv 4158  df-1o 5483  df-2o 5484  df-er 5620  df-en 5735  df-dom 5736  df-sdom 5737

Copyright terms: Public domain