Skip to content
Axiomatic Wiki
Lemma·L26

Cardinality of a disjoint union

Counting two separate piles: sizes add.

If and are finite and disjoint ( ), then is finite and with from D035 and binary union as in D004.
In words
If two finite sets are disjoint, sharing no element, then their union is finite and the size of the union equals the sum of their sizes.
Rests onF02F03F04F05F06F08F09F11F12F14A01A02A06A08
Never needed: F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Let and , with bijections and (D035). Define on by a set by Separation inside , and a function: each lies in exactly one of (disjointness, D008, excluded middle), so exactly one clause fires.
  2. 2
    lands in : for : and by L17 (i), so by L15 (ii) (equality case by substitutivity). For : , so by L17 (iii) with commutativity (adding on the left).
  3. 3
    is injective: two arguments in : gives (D014). Two in : gives by cancellation, so . Mixed, , : , so by irreflexivity (L15 (i), (ii)).
  4. 4
    is surjective onto : let , i.e. (D029). Compare with by L16. If : surjectivity of gives with . If : write for some (L17 (ii) in the strict case, with D027 in the equality case). From : by L17 (iii) with commutativity. Surjectivity of gives with , so .
  5. 5
    So is a bijection and (D033): finite, with by D035 and L23.
∎

Remarks

The map lists first and then shifted by : the arithmetic of L17 is exactly what makes "shifting by " injective and exhaustive. For overlapping sets the statement becomes inclusion-exclusion, , which needs subtraction and is not developed here. Iterated, this lemma counts any partition piece by piece: that is L27.
Wikipedia ↗Set.ncard_union_eq ↗

Used by

L27L34
Propose an edit1 published revision