TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)‡ rests on unproved material (inherited)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Every natural number and $\omega$ are cardinals, every infinite cardinal is a limit ordinal, and on the natural numbers the cardinal operations are the published finite counting operations, with $\lvert A \rvert$ in the finite sense equal to $\lvert A \rvert$ in the cardinal sense

Statement

Work in ZF; no choice principle is used. Let $\mathbb{N} = \omega$ be the von Neumann naturals (The natural numbers $\mathbb{N}$ (von Neumann)), and let $+_{\mathbb{N}}$ , $\cdot_{\mathbb{N}}$ and $m^{n}$ be the natural-number operations (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ for the power). Then:

(a) Every natural number is a cardinal (Cardinal (initial ordinal) and cardinality), and $\omega$ is a cardinal.

(b) Every infinite cardinal is a limit ordinal (Successor and limit ordinals).

(c) One notation, one meaning. If $A$ is finite (Finite, countably infinite, countable, uncountable) then $A$ is well-orderable and the natural number $\lvert A \rvert$ of The cardinality $\lvert A\rvert$ of a finite set is the cardinal $\lvert A \rvert$ of A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used.

(d) One arithmetic. For $m, n \in \omega$ , read as cardinals,

$m \oplus n = m +_{\mathbb{N}} n, \qquad m \otimes n = m \cdot_{\mathbb{N}} n, \qquad m^{n} \text{ as a cardinal } = m^{n} \text{ as a natural number},$

the natural-number power being that of Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ and the cardinal exponential being defined in ZF here because the function set it counts is finite. Moreover $m \oplus n$ and $m \otimes n$ are also the ordinal sum and product of $m$ and $n$ (On $\omega$ the ordinal $+$ and $\cdot$ are the Peano operations: $\omega$ is closed under ordinal $+$ , $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product). No agreement is claimed between the cardinal power and the ordinal power; On $\omega$ the ordinal $+$ and $\cdot$ are the Peano operations: $\omega$ is closed under ordinal $+$ , $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product itself claims none for exponentiation, and none is needed below.

Facts & Assumptions

Given: The von Neumann naturals $\mathbb{N} = \omega$ , the finite counting operations of The cardinality $\lvert A\rvert$ of a finite set, and the cardinal operations of Cardinal sum $\kappa \oplus \lambda$ , product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$ , and why they are written apart from the ordinal operations, in ZF.

[L1]

If $n \approx m$ with $n, m \in \mathbb{N}$ then $n = m$ (claim 3 of The pigeonhole principle on $\mathbb{N}$ ); and $\mathbb{N} \not\approx n$ for every $n \in \mathbb{N}$ (claim 4).

[L2]

$\mathbb{N}$ is a transitive set and $m \in n$ if and only if $m < n$ , so $n = \{m \in \mathbb{N} : m < n\}$ (On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ ).

[L3]

Every natural number is an ordinal, and $\omega$ is an ordinal ( $\omega$ is the least limit ordinal claim (ii), Ordinal (von Neumann)).

[L4]

Every element of an ordinal is an ordinal, $\alpha \notin \alpha$ , $\alpha \subseteq \beta$ iff $\alpha \in \beta$ or $\alpha = \beta$ , and ordinals satisfy trichotomy (Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals).

[L5]

For a well-orderable $X$ , $\lvert X \rvert$ is the least ordinal equinumerous with $X$ , and equinumerous sets receive the same one (A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used).

[L6]

For finite $A$ there is exactly one $n \in \mathbb{N}$ with $A \approx n$ , written $\lvert A \rvert$ ; $\lvert n \rvert = n$ ; and $\lvert B \rvert = \lvert A \rvert$ when $A \approx B$ (The cardinality $\lvert A\rvert$ of a finite set, Finite, countably infinite, countable, uncountable).

[L7]

For finite disjoint $A, B$ : $A \cup B$ is finite with $\lvert A \cup B\rvert = \lvert A\rvert +_{\mathbb{N}} \lvert B\rvert$ (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition, claim 1). For finite $A, B$ : $A \times B$ is finite with $\lvert A \times B\rvert = \lvert A\rvert \cdot_{\mathbb{N}} \lvert B\rvert$ (The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$ , and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$ , claim 1). For finite $A, B$ : the set of functions $B \to A$ is finite with cardinality $\lvert A\rvert^{\lvert B\rvert}$ (The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$ , Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ ).

[L8]

$\omega$ is inductive, so it is closed under $\sigma(n) = n \cup \{n\}$ ; $\sigma$ is injective and never $0$ ; and every nonzero natural number is a successor (The natural numbers $\mathbb{N}$ (von Neumann), The von Neumann naturals form a Peano system, Every nonzero natural number is a successor).

[L9]

$\kappa \oplus \lambda = \lvert \kappa \sqcup \lambda\rvert$ , $\kappa \otimes \lambda = \lvert \kappa \times \lambda\rvert$ , $\kappa^{\lambda} = \lvert {}^{\lambda}\kappa\rvert$ (Cardinal sum $\kappa \oplus \lambda$ , product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$ , and why they are written apart from the ordinal operations); a bijection witnesses $\approx$ and compositions of bijections are bijections (Equinumerous sets, $A \approx B$ and $A \preceq B$ , Injection, surjection, bijection).

[L10]

On $\omega$ the ordinal sum and product are the Peano ones (On $\omega$ the ordinal $+$ and $\cdot$ are the Peano operations: $\omega$ is closed under ordinal $+$ , $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product, claim (b)).

Proof

technique · direct

1.1

Let $n \in \mathbb{N}$ and suppose $\alpha \in n$ with $\alpha \approx n$ ; then $\alpha \in \mathbb{N}$ by [L2], so $\alpha = n$ by [L1], giving $n \in n$ , which [L4] forbids; so $n$ is a cardinal.

L1L2L3L4

1.2

Suppose $\alpha \in \omega$ with $\alpha \approx \omega$ ; then $\alpha \in \mathbb{N}$ and $\mathbb{N} \approx \alpha$ , which [L1] forbids; so $\omega$ is a cardinal, and claim (a) holds.

L1L3L4

1.3

Let $\kappa$ be an infinite cardinal, so $\omega \subseteq \kappa$ ; then $\kappa \ne 0$ , and if $\kappa = \beta \cup \{\beta\}$ for an ordinal $\beta$ then $\beta \in \omega$ is impossible, since $\kappa = \sigma(\beta) \in \omega$ by [L8] would give $\kappa \in \kappa$ against [L4], so $\omega \subseteq \beta$ by [L4]; the map sending $\beta$ to $0$ , each $j \in \omega$ to $\sigma(j)$ , and each $\xi \in \beta$ with $\omega \subseteq \xi$ to itself is then a bijection $\kappa \to \beta$ , its three pieces having the pairwise disjoint images $\{0\}$ , $\omega \setminus \{0\}$ and $\{\xi \in \beta : \omega \subseteq \xi\}$ by [L8]; so $\beta \approx \kappa$ with $\beta \in \kappa$ , contradicting that $\kappa$ is a cardinal, and $\kappa$ is therefore a limit ordinal, which is claim (b).

L4L8L9

1.4

For $m, n \in \mathbb{N}$ the sets $\{0\} \times m$ and $\{1\} \times n$ are finite and disjoint with $\lvert \{0\} \times m\rvert = m$ and $\lvert \{1\} \times n\rvert = n$ by [L6], so [L7] gives that $m \sqcup n$ , $m \times n$ and ${}^{n}m$ are all finite, with finite cardinalities $m +_{\mathbb{N}} n$ , $m \cdot_{\mathbb{N}} n$ and $m^{n}$ respectively.

L6L7L9

2.1

Claim (c): let $A$ be finite and $n = \lvert A \rvert$ in the sense of [L6], so $A \approx n$ and $A$ is well-orderable; if $\beta \approx A$ with $\beta \in n$ then $\beta \in \mathbb{N}$ by [L2] and $\beta \approx n$ by [L9], so $\beta = n$ by [L1], contradicting [L4]; hence $n$ is the least ordinal equinumerous with $A$ and equals the cardinal $\lvert A \rvert$ of [L5].

step 1.1L1L2L4L5L6L9

3.1

Claim (d): each of $m \sqcup n$ , $m \times n$ and ${}^{n}m$ is finite by step 1.4, hence well-orderable, so its cardinal cardinality is defined in ZF and equals its finite cardinality by step 2.1; reading this through [L9] gives $m \oplus n = m +_{\mathbb{N}} n$ , $m \otimes n = m \cdot_{\mathbb{N}} n$ and $m^{n}$ (cardinal) $= m^{n}$ (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ ), and [L10] identifies the first two with the ordinal sum and product.

step 1.4step 2.1L9L10

4.1

Claims (a), (b), (c) and (d) all hold, in ZF.

step 1.2step 1.3step 2.1step 3.1∎

Remarks

Why this theorem is not optional. Two published items already write $\lvert A \rvert$ : The cardinality $\lvert A\rvert$ of a finite set, where the value is a natural number and the definition applies to finite sets only, and Cardinal (initial ordinal) and cardinality, where the value is an initial ordinal. On a finite set both apply. Without claim (c) the same symbol would carry two meanings and every finite computation on this page would be ambiguous; with it there is one meaning, and a natural number may be read as a cardinal without comment.

The same holds for $+$ on $\omega$ , twice over. Claim (d) closes the second half of a dictionary whose first half is On $\omega$ the ordinal $+$ and $\cdot$ are the Peano operations: $\omega$ is closed under ordinal $+$ , $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product: the Peano sum, the ordinal sum and the cardinal sum of two natural numbers are one natural number. The three operations diverge immediately above $\omega$ , and that divergence is the reason Cardinal sum $\kappa \oplus \lambda$ , product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$ , and why they are written apart from the ordinal operations writes $\oplus$ and $\otimes$ rather than $+$ and $\cdot$ .

What claim (b) is for. It is used wherever an argument needs to take suprema below an infinite cardinal, or to know that $\max(\xi,\eta) + 1$ stays below $\kappa$ when $\xi, \eta < \kappa$ . The proof is the shift bijection that Cardinal (initial ordinal) and cardinality already describes for $\omega^{+}$ , carried out at an arbitrary infinite cardinal: prepending or removing one point does not change the size of an infinite well-ordered set, so a successor ordinal above $\omega$ is never an initial ordinal.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 117 results over 33 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

K. Kearnes, Cardinal Arithmetic (Fall 2025 course handout) (standard reference, not scraped)
Cardinal number (Wikipedia) (standard reference, not scraped)
Finite set (Wikipedia) (standard reference, not scraped)