Skip to content
Axiomatic Wiki
Theorem·T20

The naturals form an infinite set

No natural number counts the naturals: omega is not equinumerous with any numeral.

The set of naturals is infinite (D034): with from D033.
In words
No natural number counts the naturals: omega cannot be put in bijection with any finite numeral.
Rests onF02F03F04F06F08F09F11F14A01A06A08
Never needed: F05 · F10 · F12 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Suppose for contradiction (F04) that for some , via a bijection (D033).
  2. 2
    The numeral is a subset of : gives (L06), and (D006) with and , so .
  3. 3
    The restriction is a function whose values are values of , hence injective (if then , so ).
  4. 4
    But (L15 (vi)), so T12 forbids any injection . This contradiction (F03) shows no such exists: is not finite, that is, infinite.
∎

Remarks

The first infinite set in the library, and the witness that the axiom of infinity delivers something genuinely new. It is countable (the identity injects into itself), so is the prototype of a countably infinite set; every countably infinite set is equinumerous with it by Cantor-Schröder-Bernstein. That not every infinite set is countable is T21.
Wikipedia ↗Set.infinite_coe_iff ↗
Propose an edit1 published revision