Theorem pm54.43 4498

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), so that their A e. 1 means, in our notation, A e. {x | (card` x) = 1o} i.e. (card` A) = 1o (by elab 1869) i.e. A ~~ 1o (by carden 4755 and cardnn 4748). 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 4846 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 4076	. . . . . . . 8 |- 1o e. On
2	1	onirr 3060	. . . . . . 7 |- -. 1o e. 1o
3		disjsn 2412	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
4	2, 3	mpbir 190	. . . . . 6 |- (1o i^i {1o}) = (/)
5		unen 4368	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
6	4, 5	mpanr2 707	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
7	6	ex 373	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
8	1	elisseti 1793	. . . . . 6 |- 1o e. V
9	8	ensn1 4359	. . . . . 6 |- {1o} ~~ 1o
10	8, 9	ensymi 4348	. . . . 5 |- 1o ~~ {1o}
11		entrt 4349	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
12	10, 11	mpan2 693	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
13	7, 12	sylan2 451	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 4072	. . . . 5 |- 2o = suc 1o
15		df-suc 2917	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtr 1471	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 2595	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 213	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		sneq 2388	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
20	19	uneq2d 2155	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
21		unidm 2146	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22	20, 21	syl5reqr 1498	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
23		visset 1788	. . . . . . . . . . . . . . 15 |- x e. V
24	23	ensn1 4359	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
25		1sdom2 4457	. . . . . . . . . . . . . 14 |- 1o ~< 2o
26		ensdomtr 4405	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
27	24, 25, 26	mp2an 694	. . . . . . . . . . . . 13 |- {x} ~< 2o
28	22, 27	syl6eqbr 2620	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
29		sdomnen 4322	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
30	28, 29	syl 10	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
31	30	necon2ai 1587	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
32		disjsn2 2413	. . . . . . . . . 10 |- (x =/= y -> ({x} i^i {y}) = (/))
33	31, 32	syl 10	. . . . . . . . 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 2150	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
36	35	breq1d 2597	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
37		ineq12 2183	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
38	37	eqeq1d 1459	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
39	34, 36, 38	3imtr4d 541	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
40	39	ex 373	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
41	40	19.23adv 1198	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
42	41	19.23aiv 1277	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	imp 350	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
44		en1 4361	. . 3 |- (A ~~ 1o <-> E.x A = {x})
45		en1 4361	. . 3 |- (B ~~ 1o <-> E.y B = {y})
46	43, 44, 45	syl2anb 455	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
47	18, 46	impbid 514	1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  E.wex 956   = wceq 1099   e. wcel 1105   =/= wne 1561   u. cun 2016   i^i cin 2017  (/)c0 2251  {csn 2380   class class class wbr 2587  Oncon0 2911  suc csuc 2913  1oc1o 4066  2oc2o 4067   ~~ cen 4302   ~< csdm 4304

This theorem is referenced by:  pm110.643 4846

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-suc 2917  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-f1 3158  df-fo 3159  df-f1o 3160  df-fv 3161  df-1o 4071  df-2o 4072  df-er 4199  df-en 4305  df-dom 4306  df-sdom 4307

Copyright terms: Public domain