Description: 1+1=2 for cardinal number addition, derived from pm54.43 as promised.
Theorem *110.643 ofPrincipia Mathematica, vol. II, p. 86, which adds
the remark, "The above proposition is occasionally useful." 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 ), but after applying definitions, our theorem is equivalent.
Because we use a disjoint union for cardinal addition (as explained in the
comment at the top of this section), we use ~ instead of =. See
dju1p1e2ALT for a shorter proof that doesn't use pm54.43 .
(Contributed by NM, 5-Apr-2007)(Proof modification is discouraged.)