Lemma·L23
Uniqueness of cardinality
A set matches at most one natural number.
For every set
and all
:
with
from D033.
In words
For a set A and natural numbers m and n: if the set is equinumerous with m and also equinumerous with n, then m and n are the same number.
Never needed: F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Let and be bijections. Then is a bijection by L03, and is a bijection by L02 (iv).
- 2
- 3Both cases are absurd (falsum), so (F04, excluded middle).
∎
Remarks
This is what makes counting meaningful: however a finite set is enumerated, the same number comes out. Nothing analogous is being claimed for infinite sets here; that theory needs ordinals and choice. The lemma licenses the notation
of D035.