CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

The irrationals are uncountable

Statement

Let $\mathbb{R}$ be a complete ordered field (Complete ordered field (least-upper-bound property)) and let $\iota : \mathbb{Q} \to \mathbb{R}$ be the canonical embedding (The unique embedding of ℚ into an ordered field); write $\mathbb{Q}_{\mathbb{R}} = \iota[\mathbb{Q}]$ for the copy of the rationals inside $\mathbb{R}$ , the set usually written $\mathbb{Q}$ once the identification is made. Then the set of irrationals

$\mathbb{R} \setminus \mathbb{Q}_{\mathbb{R}}$

is uncountable (Finite, countably infinite, countable, uncountable).

Only the union of two sets is used, and that needs no choice whatsoever. If the irrationals were at most countable, then $\mathbb{R}$ would be the union of the two at most countable sets $\mathbb{Q}_{\mathbb{R}}$ and $\mathbb{R} \setminus \mathbb{Q}_{\mathbb{R}}$ , and countability of a two-set union is proved by interleaving two given enumerations. The countable union theorem, which does spend $\mathrm{AC}_\omega$ , is not invoked here and is not needed; see the remarks below.

Facts & Assumptions

Given: A complete ordered field $\mathbb{R}$ , the canonical embedding $\iota : \mathbb{Q} \to \mathbb{R}$ , the subset $\mathbb{Q}_{\mathbb{R}} = \iota[\mathbb{Q}]$ and its complement $X = \mathbb{R} \setminus \mathbb{Q}_{\mathbb{R}}$ , so that $\mathbb{R} = \mathbb{Q}_{\mathbb{R}} \cup X$ .

[L1]

$\iota$ is injective (The unique embedding of ℚ into an ordered field), hence a bijection of $\mathbb{Q}$ onto $\mathbb{Q}_{\mathbb{R}}$ ; $\approx$ is transitive (Equinumerous sets, $A \approx B$ and $A \preceq B$ , Injection, surjection, bijection).

[L2]

$\mathbb{Q} \approx \mathbb{N}$ , so $\mathbb{Q}$ is at most countable ( $\mathbb{Q}$ is countably infinite).

[L3]

A nonempty set is at most countable if and only if some surjection $\mathbb{N} \to$ it exists (A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$ ); uncountable means not at most countable (Finite, countably infinite, countable, uncountable).

[L4]

There is a bijection $\beta : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ ( $\mathbb{N} \times \mathbb{N} \approx \mathbb{N}$ ).

[L5]

$\mathbb{R}$ is uncountable ( $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874)).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $X = \mathbb{R} \setminus \mathbb{Q}_{\mathbb{R}}$ is at most countable.

assume-contra

1.2

$\mathbb{Q}_{\mathbb{R}} \approx \mathbb{Q} \approx \mathbb{N}$ by [L1] and [L2], so $\mathbb{Q}_{\mathbb{R}}$ is at most countable, and it is nonempty since $\iota(0) \in \mathbb{Q}_{\mathbb{R}}$ .

L1L2

1.3

Fix the bijection $\beta : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ of [L4].

2.1

If $X = \varnothing$ then $\mathbb{R} = \mathbb{Q}_{\mathbb{R}}$ , which is at most countable by step 1.2.

step 1.2given

2.2

Otherwise $X \ne \varnothing$ , and since $X$ is at most countable by assumption and $\mathbb{Q}_{\mathbb{R}}$ is nonempty and at most countable by step 1.2, [L3] provides surjections $f : \mathbb{N} \to \mathbb{Q}_{\mathbb{R}}$ and $g : \mathbb{N} \to X$ .

step 1.1step 1.2L3

3.1

Define $u : \mathbb{N} \times \mathbb{N} \to \mathbb{R}$ by $u(0,k) = f(k)$ and $u(n,k) = g(k)$ for $n \ne 0$ . Every element of $\mathbb{R}$ lies in $\mathbb{Q}_{\mathbb{R}}$ or in $X$ , hence is $f(k)$ or $g(k)$ for some $k$ , so $u$ is surjective onto $\mathbb{R}$ . The two surjections were obtained one after the other, not selected simultaneously from an infinite family, so no choice principle is used.

step 2.2given

4.1

Hence $u \circ \beta : \mathbb{N} \to \mathbb{R}$ is a surjection and $\mathbb{R} \ne \varnothing$ , so $\mathbb{R}$ is at most countable by [L3].

step 1.3step 3.1L3

5.1

In either case $\mathbb{R}$ is at most countable, by step 2.1 in the first and step 4.1 in the second; this contradicts [L5]. Therefore $X = \mathbb{R} \setminus \mathbb{Q}_{\mathbb{R}}$ is uncountable.

step 2.1step 4.1L3L5discharge-contradiction∎

Remarks

The same argument shows that removing any at most countable set from $\mathbb{R}$ leaves an uncountable set. In particular the algebraic numbers, once they are available, can be removed to show transcendental numbers exist, which is how Cantor's 1874 paper presented the result: an existence proof for transcendentals with no example constructed.
The corollary is a statement about the set of irrationals only. It says nothing about any individual irrational, and it does not exhibit one; the library exhibits $\sqrt{2}$ separately ( $\sqrt{2}$ exists in every complete ordered field, and is irrational, FALSE: some rational number squares to 2).
Keeping the two-set union separate from the countable union is not pedantry. The countable case genuinely needs $\mathrm{AC}_\omega$ (Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$ ) and is unprovable in ZF conditionally on the consistency of ZF, which is the honest form of FALSE: countable unions of countable sets are countable is a theorem of ZF and rests on an external independence result quoted there rather than proved; whereas this corollary, like $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874) itself, is outright a theorem of ZF.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 86 results over 22 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

J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
J. Lebl, Basic Analysis I (standard reference, not scraped)
Irrational number (Wikipedia) (standard reference, not scraped)
Countable set (Wikipedia) (standard reference, not scraped)