Table of Contents - 2.6.14. Cardinal number arithmetic
For cardinal arithmetic, we follow [Mendelson] p. 258. Rather than
defining operations restricted to cardinal numbers, we use disjoint
union df-dju () for cardinal addition, Cartesian product
df-xp () for cardinal multiplication, and set exponentiation
df-map () for cardinal exponentiation. Equinumerosity and
dominance serve the roles of equality and ordering. If we wanted to,
we could easily convert our theorems to actual cardinal number
operations via carden, carddom, and cardsdom. The advantage
of Mendelson's approach is that we can directly use many equinumerosity
theorems that we already have available.