Theorem pm54.43 6350

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 6327), 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 6349. 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 6454 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 5476	. . . . . . 7 |- 1o e. On
2	1	elisseti 2553	. . . . . 6 |- 1o e. _V
3	2	ensn1 5779	. . . . . 6 |- {1o} ~~ 1o
4	2, 3	ensymi 5768	. . . . 5 |- 1o ~~ {1o}
5		entr 5769	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
6	4, 5	mpan2 740	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
7	1	onirri 3957	. . . . . . 7 |- -. 1o e. 1o
8		disjsn 3307	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
9	7, 8	mpbir 243	. . . . . 6 |- (1o i^i {1o}) = (/)
10		unen 5794	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
11	9, 10	mpanr2 755	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
12	11	ex 483	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
13	6, 12	sylan2 666	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 5470	. . . . 5 |- 2o = suc 1o
15		df-suc 3858	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 2156	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 3546	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 267	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		en1 5782	. . 3 |- (A ~~ 1o <-> E.x A = {x})
20		en1 5782	. . 3 |- (B ~~ 1o <-> E.y B = {y})
21		unidm 2980	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22		sneq 3274	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
23	22	uneq2d 2991	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
24	21, 23	syl5reqr 2186	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
25		visset 2546	. . . . . . . . . . . . . . 15 |- x e. _V
26	25	ensn1 5779	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
27		1sdom2 5953	. . . . . . . . . . . . . 14 |- 1o ~< 2o
28		ensdomtr 5837	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
29	26, 27, 28	mp2an 741	. . . . . . . . . . . . 13 |- {x} ~< 2o
30	24, 29	syl6eqbr 3579	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
31		sdomnen 5738	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
32	30, 31	syl 13	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
33	32	necon2ai 2306	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
34		disjsn2 3308	. . . . . . . . . 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 2986	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
38	37	breq1d 3548	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
39		ineq12 3022	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
40	39	eqeq1d 2144	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
41	36, 38, 40	3imtr4d 314	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
42	41	ex 483	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	19.23adv 1852	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
44	43	19.23aiv 1936	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
45	44	imp 478	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
46	19, 20, 45	syl2anb 670	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
47	18, 46	impbid 221	1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 214   /\ wa 417  E.wex 1563   = wceq 1634   e. wcel 1636   =/= wne 2262   u. cun 2840   i^i cin 2841  (/)c0 3101  {csn 3265   class class class wbr 3538  Oncon0 3852  suc csuc 3854  1oc1o 5462  2oc2o 5463   ~~ cen 5715   ~< csdm 5717

This theorem is referenced by:  pr2nelem 6351  pm110.643 6454  isprm2lem 9791

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1559  ax-6 1560  ax-7 1561  ax-gen 1562  ax-8 1638  ax-10 1639  ax-11 1640  ax-12 1641  ax-13 1642  ax-14 1643  ax-17 1650  ax-9 1661  ax-4 1666  ax-10o 1778  ax-16 1846  ax-11o 1857  ax-ext 2118  ax-rep 3628  ax-sep 3638  ax-nul 3648  ax-pow 3684  ax-pr 3708  ax-un 3970

This theorem depends on definitions:  df-bi 215  df-or 418  df-an 419  df-3or 1083  df-3an 1084  df-ex 1564  df-sb 1808  df-eu 2036  df-mo 2037  df-clab 2124  df-cleq 2129  df-clel 2132  df-ne 2264  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2361  df-v 2545  df-dif 2845  df-un 2847  df-in 2849  df-ss 2851  df-pss 2853  df-nul 3102  df-pw 3254  df-sn 3269  df-pr 3270  df-tp 3272  df-op 3273  df-uni 3397  df-br 3539  df-opab 3597  df-tr 3612  df-eprel 3785  df-id 3788  df-po 3793  df-so 3805  df-fr 3823  df-we 3839  df-ord 3855  df-on 3856  df-suc 3858  df-xp 4174  df-rel 4175  df-cnv 4176  df-co 4177  df-dm 4178  df-rn 4179  df-res 4180  df-ima 4181  df-fun 4182  df-fn 4183  df-f 4184  df-f1 4185  df-fo 4186  df-f1o 4187  df-fv 4188  df-1o 5469  df-2o 5470  df-er 5606  df-en 5719  df-dom 5720  df-sdom 5721

Copyright terms: Public domain