Theorem pm54.43 4713

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 4979), so that their A e. 1 means, in our notation, A e. {x | (card` x) = 1o} i.e. (card` A) = 1o (by elab 1942) i.e. A ~~ 1o (by carden 4977 and cardnn 4968). 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 5072 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 4272	. . . . . . . 8 |- 1o e. On
2	1	onirri 3075	. . . . . . 7 |- -. 1o e. 1o
3		disjsn 2501	. . . . . . 7 |- ((1o i^i {1o}) = (/) <-> -. 1o e. 1o)
4	2, 3	mpbir 188	. . . . . 6 |- (1o i^i {1o}) = (/)
5		unen 4573	. . . . . 6 |- (((A ~~ 1o /\ B ~~ {1o}) /\ ((A i^i B) = (/) /\ (1o i^i {1o}) = (/))) -> (A u. B) ~~ (1o u. {1o}))
6	4, 5	mpanr2 713	. . . . 5 |- (((A ~~ 1o /\ B ~~ {1o}) /\ (A i^i B) = (/)) -> (A u. B) ~~ (1o u. {1o}))
7	6	ex 371	. . . 4 |- ((A ~~ 1o /\ B ~~ {1o}) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
8	1	elisseti 1863	. . . . . 6 |- 1o e. V
9	8	ensn1 4563	. . . . . 6 |- {1o} ~~ 1o
10	8, 9	ensymi 4552	. . . . 5 |- 1o ~~ {1o}
11		entr 4553	. . . . 5 |- ((B ~~ 1o /\ 1o ~~ {1o}) -> B ~~ {1o})
12	10, 11	mpan2 699	. . . 4 |- (B ~~ 1o -> B ~~ {1o})
13	7, 12	sylan2 453	. . 3 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ (1o u. {1o})))
14		df-2o 4268	. . . . 5 |- 2o = suc 1o
15		df-suc 2980	. . . . 5 |- suc 1o = (1o u. {1o})
16	14, 15	eqtri 1537	. . . 4 |- 2o = (1o u. {1o})
17	16	breq2i 2699	. . 3 |- ((A u. B) ~~ 2o <-> (A u. B) ~~ (1o u. {1o}))
18	13, 17	syl6ibr 211	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) -> (A u. B) ~~ 2o))
19		sneq 2474	. . . . . . . . . . . . . . 15 |- (x = y -> {x} = {y})
20	19	uneq2d 2235	. . . . . . . . . . . . . 14 |- (x = y -> ({x} u. {x}) = ({x} u. {y}))
21		unidm 2226	. . . . . . . . . . . . . 14 |- ({x} u. {x}) = {x}
22	20, 21	syl5reqr 1564	. . . . . . . . . . . . 13 |- (x = y -> ({x} u. {y}) = {x})
23		visset 1858	. . . . . . . . . . . . . . 15 |- x e. V
24	23	ensn1 4563	. . . . . . . . . . . . . 14 |- {x} ~~ 1o
25		1sdom2 4670	. . . . . . . . . . . . . 14 |- 1o ~< 2o
26		ensdomtr 4614	. . . . . . . . . . . . . 14 |- (({x} ~~ 1o /\ 1o ~< 2o) -> {x} ~< 2o)
27	24, 25, 26	mp2an 700	. . . . . . . . . . . . 13 |- {x} ~< 2o
28	22, 27	syl6eqbr 2724	. . . . . . . . . . . 12 |- (x = y -> ({x} u. {y}) ~< 2o)
29		sdomnen 4526	. . . . . . . . . . . 12 |- (({x} u. {y}) ~< 2o -> -. ({x} u. {y}) ~~ 2o)
30	28, 29	syl 10	. . . . . . . . . . 11 |- (x = y -> -. ({x} u. {y}) ~~ 2o)
31	30	necon2ai 1653	. . . . . . . . . 10 |- (({x} u. {y}) ~~ 2o -> x =/= y)
32		disjsn2 2502	. . . . . . . . . 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 2230	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A u. B) = ({x} u. {y}))
36	35	breq1d 2701	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o <-> ({x} u. {y}) ~~ 2o))
37		ineq12 2263	. . . . . . . . 9 |- ((A = {x} /\ B = {y}) -> (A i^i B) = ({x} i^i {y}))
38	37	eqeq1d 1525	. . . . . . . 8 |- ((A = {x} /\ B = {y}) -> ((A i^i B) = (/) <-> ({x} i^i {y}) = (/)))
39	34, 36, 38	3imtr4d 545	. . . . . . 7 |- ((A = {x} /\ B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
40	39	ex 371	. . . . . 6 |- (A = {x} -> (B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
41	40	19.23adv 1250	. . . . 5 |- (A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
42	41	19.23aiv 1332	. . . 4 |- (E.x A = {x} -> (E.y B = {y} -> ((A u. B) ~~ 2o -> (A i^i B) = (/))))
43	42	imp 348	. . 3 |- ((E.x A = {x} /\ E.y B = {y}) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
44		en1 4565	. . 3 |- (A ~~ 1o <-> E.x A = {x})
45		en1 4565	. . 3 |- (B ~~ 1o <-> E.y B = {y})
46	43, 44, 45	syl2anb 457	. 2 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A u. B) ~~ 2o -> (A i^i B) = (/)))
47	18, 46	impbid 518	1 |- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221   = wceq 991   e. wcel 993  E.wex 1015   =/= wne 1627   u. cun 2096   i^i cin 2097  (/)c0 2331  {csn 2466   class class class wbr 2691  Oncon0 2974  suc csuc 2976  1oc1o 4262  2oc2o 4263   ~~ cen 4503   ~< csdm 4505

This theorem is referenced by:  pm110.643 5072  unpde2eg2 11010

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-9 1000  ax-10 1001  ax-11 1002  ax-12 1003  ax-13 1004  ax-14 1005  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499  ax-rep 2766  ax-sep 2776  ax-nul 2783  ax-pow 2817  ax-pr 2854  ax-un 3088

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 781  df-3an 782  df-ex 1016  df-sb 1208  df-eu 1420  df-mo 1421  df-clab 1505  df-cleq 1510  df-clel 1513  df-ne 1629  df-ral 1694  df-rex 1695  df-reu 1696  df-rab 1697  df-v 1857  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2458  df-sn 2469  df-pr 2470  df-tp 2472  df-op 2473  df-uni 2569  df-br 2692  df-opab 2740  df-tr 2754  df-eprel 2909  df-id 2912  df-po 2917  df-so 2928  df-fr 2946  df-we 2961  df-ord 2977  df-on 2978  df-suc 2980  df-xp 3264  df-rel 3265  df-cnv 3266  df-co 3267  df-dm 3268  df-rn 3269  df-res 3270  df-ima 3271  df-fun 3272  df-fn 3273  df-f 3274  df-f1 3275  df-fo 3276  df-f1o 3277  df-fv 3278  df-1o 4267  df-2o 4268  df-er 4399  df-en 4507  df-dom 4508  df-sdom 4509

Copyright terms: Public domain