Theorem pm110.643 4988

Description: 1+1=2 for cardinal number addition. Theorem *110.643 of Principia Mathematica, vol. II, p. 86, which adds the remark, "The above proposition is occasionally useful." Unlike us, Whitehead and Russell define cardinal addition on collections of all sets equinumerous to 1 and 2 (which for us are proper classes unless we restrict them as in karden 4788), but after applying definitions, our theorem is equivalent. See also the comment for pm54.43 4632. The comment for cdavali 4985 explains why we use ~~ instead of =.

Assertion

Ref	Expression
pm110.643	|- (1o +c 1o) ~~ 2o

Proof of Theorem pm110.643

Step	Hyp	Ref	Expression
1		1on 4196	. . . 4 |- 1o e. On
2	1	elisseti 1865	. . 3 |- 1o e. V
3	2, 2	cdavali 4985	. 2 |- (1o +c 1o) = ((1o X. {(/)}) u. (1o X. {1o}))
4		xp01disj 4201	. . 3 |- ((1o X. {(/)}) i^i (1o X. {1o})) = (/)
5		0ex 2766	. . . . 5 |- (/) e. V
6	2, 5	xpsnen 4498	. . . 4 |- (1o X. {(/)}) ~~ 1o
7	2, 2	xpsnen 4498	. . . 4 |- (1o X. {1o}) ~~ 1o
8		pm54.43 4632	. . . 4 |- (((1o X. {(/)}) ~~ 1o /\ (1o X. {1o}) ~~ 1o) -> (((1o X. {(/)}) i^i (1o X. {1o})) = (/) <-> ((1o X. {(/)}) u. (1o X. {1o})) ~~ 2o))
9	6, 7, 8	mp2an 709	. . 3 |- (((1o X. {(/)}) i^i (1o X. {1o})) = (/) <-> ((1o X. {(/)}) u. (1o X. {1o})) ~~ 2o)
10	4, 9	mpbi 196	. 2 |- ((1o X. {(/)}) u. (1o X. {1o})) ~~ 2o
11	3, 10	eqbrtri 2689	1 |- (1o +c 1o) ~~ 2o

Syntax hints:   <-> wb 153   = wceq 997   u. cun 2096   i^i cin 2097  (/)c0 2331  {csn 2461   class class class wbr 2674  Oncon0 3005   X. cxp 3225  (class class class)co 4021  1oc1o 4186  2oc2o 4187   ~~ cen 4425   +c ccda 4982

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-suc 3011  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-f1 3252  df-fo 3253  df-f1o 3254  df-fv 3255  df-opr 4023  df-oprab 4024  df-1o 4191  df-2o 4192  df-er 4319  df-en 4429  df-dom 4430  df-sdom 4431  df-cda 4983

Copyright terms: Public domain