TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Countable unions of at most countable sets, assuming ${A C}_{ω}$

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $(A_{n})_{n \in N}$ be a family of at most countable sets (Finite, countably infinite, countable, uncountable) indexed by $N$ . Then

$U = ⋃_{n \in N} A_{n}$

is at most countable.

The hypothesis ${A C}_{ω}$ is not decoration and it is not removable. It is spent at exactly one step, step 3.1 below, where one surjection $N \to A_{n}$ is selected for every $n$ at once. Each $A_{n}$ has such surjections, in general many of them, and the countability assumption provides no rule for singling one out. Without some choice principle the theorem is not available at all: ZF alone does not prove it, conditionally on the consistency of ZF, as recorded among this page's false statements and discussed in the remarks below, where that item is named and linked. The consistency hypothesis is not a formality and cannot be dropped: the separation rests on an external independence result that this library quotes rather than proves, and it cannot be stated without it.

Facts & Assumptions

Given: A family $(A_{n})_{n \in N}$ of at most countable sets, its union $U = ⋃_{n \in N} A_{n}$ , and the Axiom of Countable Choice as an explicit hypothesis.

[L1]

Finite, countably infinite, at most countable; $\emptyset$ is finite (Finite, countably infinite, countable, uncountable).

[L2]

A nonempty set $X$ is at most countable if and only if there is a surjection $N \to X$ (A nonempty set is at most countable iff it is a surjective image of $N$ ).

[L3]

${A C}_{ω}$ : for every family $(X_{n})_{n \in N}$ of nonempty sets there is $f$ with $f (n) \in X_{n}$ for all $n$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L4]

There is a bijection $β : N \to N \times N$ ( $N \times N \approx N$ , Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[L5]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L6]

A composition of surjections is a surjection (Injection, surjection, bijection).

Proof

technique · direct

1.1

If $U = \emptyset$ then $U$ is finite, hence at most countable.

givenL1

1.2

Assume instead $U \neq \emptyset$ ; then $J : = {n \in N : A_{n} \neq \emptyset}$ is nonempty, so it has a least element $n_{0}$ by [L5].

givenL5

1.3

Fix the bijection $β : N \to N \times N$ of [L4].

2.1

For $n \in J$ let $S_{n}$ be the set of all surjections $N \to A_{n}$ , which is nonempty by [L2] since $A_{n}$ is nonempty and at most countable; for $n \notin J$ put $S_{n} : = S_{n_{0}}$ , also nonempty. This makes $(S_{n})_{n \in N}$ a family of nonempty sets indexed by $N$ , defined with no choices.

step 1.2givenL2construct

3.1

This is the step that uses choice. Apply ${A C}_{ω}$ [L3] to the family $(S_{n})_{n \in N}$ of step 2.1: it delivers a function $n \mapsto s_{n}$ with $s_{n} \in S_{n}$ for every $n$ , that is, one surjection $s_{n} : N \to A_{n}$ selected simultaneously for every $n \in J$ . Nothing in the hypotheses names a particular surjection onto $A_{n}$ , so this selection cannot be replaced by a definition; it is exactly here, and nowhere else in the proof, that the theorem leaves ZF.

step 2.1L3choose

4.1

Define $t : N \times N \to U$ by $t (n, k) = s_{n} (k)$ ; the value lies in $A_{n} \subseteq U$ for $n \in J$ and in $A_{n_{0}} \subseteq U$ otherwise, so $t$ is well defined. It is surjective: any $x \in U$ lies in some $A_{n}$ , which is then nonempty, so $n \in J$ and $x = s_{n} (k)$ for some $k$ because $s_{n}$ is onto $A_{n}$ .

step 3.1given

5.1

Hence $t \circ β : N \to U$ is a surjection by [L6], and $U \neq \emptyset$ , so $U$ is at most countable by [L2].

step 1.3step 4.1L2L6

6.1

In both cases $U$ is at most countable, which is the assertion.

step 1.1step 5.1L1∎

Remarks

An at most countable index set is no more general. If $I$ is at most countable and $(A_{i})_{i \in I}$ are at most countable, then either $I$ is empty, and the union is $\emptyset$ , or a surjection $r : N \to I$ exists (A nonempty set is at most countable iff it is a surjective image of $N$ ) and $⋃_{i \in I} A_{i} = ⋃_{n \in N} A_{r (n)}$ , which the theorem covers. That reindexing uses no choice.
The two-set union needs no choice at all, and neither does any union of finitely many sets: with $A$ and $B$ both at most countable and nonempty, fix surjections $f, g : N \to A, B$ (two choices made one after the other, which is ordinary existential instantiation, not a choice principle) and put $u (0, k) = f (k)$ and $u (n, k) = g (k)$ for $n \neq 0$ , a surjection $N \times N \to A \cup B$ . This is the form used in The irrationals are uncountable, and keeping it separate from the countable case is the whole point of flagging step 3.1.
The proof isolates its exact use of ${A C}_{ω}$ at step 3.1. It does not infer from that proof cost that the hypothesis is necessary; proving such a lower bound belongs to the later symmetric-model development.

Depends on

Used by

…and 51 more results.

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

D. H. Fremlin, Measure Theory, Chapter 56 (standard reference, not scraped)
Axiom of countable choice (Wikipedia) (standard reference, not scraped)
Countable set (Wikipedia) (standard reference, not scraped)

Countable unions of at most countable sets, assuming ACωACω​