Alphabeta Math
LemmaStatement: 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.

Every subset of an at most countable set is at most countable

Statement

Let A be at most countable (Finite, countably infinite, countable, uncountable) and let B⊆A. Then B is at most countable.

The proof establishes the sharper statement about subsets of N from which this follows: a subset S⊆N is finite if it is bounded above, and countably infinite if it is not.

No choice principle is used. This is the point of the lemma rather than a footnote to it. The enumeration of an unbounded S⊆N is built by always taking the least element of S above the previous one, and the least element of a nonempty set of naturals is canonical (The well-ordering principle): it is determined by S, not selected from it. Replacing "least" by "some" would turn the construction into an appeal to dependent choice.

Facts & Assumptions

Given: An at most countable set A and a subset B⊆A. Throughout, a natural number is the von Neumann natural, so that 0=∅ and σ(n)=n∪{n} (The natural numbers N (von Neumann)); that n={ m∈N:m<n }, and in particular that every element of a natural number is a natural number, is On N the order is membership: m<n  ⟺  m∈n, proved earlier on this page from the additive order of Order on the natural numbers.

[L1]

A is finite when A≈n for some n∈N, countably infinite when A≈N, and at most countable when one of the two holds (Finite, countably infinite, countable, uncountable).

[L2]

≈ is symmetric and transitive, an injection is a bijection onto its image, and the restriction of a bijection to a subset is a bijection onto the image of that subset (Equinumerous sets, A≈B and A⪯B, Injection, surjection, bijection).

[L3]

Well-ordering: every nonempty subset of N has a least element (The well-ordering principle).

[L4]

Strong induction: if for every n the truth of P(m) for all m<n implies P(n), then P(n) holds for every n (Strong (complete) induction).

[L5]

Recursion: for any set X, any x0∈X and any F:X→X there is a function h:N→X with h(0)=x0 and h(σ(n))=F(h(n)) (The recursion theorem).

[L6]

Order facts in N: m∈n  ⟺  m<n, m≤n  ⟺  m⊆n, n<σ(n), and m<σ(n)  ⟺  m≤n (On N the order is membership: m<n  ⟺  m∈n); exactly one of m<n, m=n, n<m holds, so < is irreflexive and any two naturals are comparable (Trichotomy of the order on N); ≤ is reflexive, antisymmetric, transitive and total (≤ is a linear order on N), whence < is transitive, because m<n<p gives m≤p while m=p would force m=n by antisymmetry; m<n  ⟺  σ(m)≤n (Discreteness: σ(n) is the immediate successor).

[L7]

Every nonzero natural is a successor (Every nonzero natural number is a successor).

[L8]

Membership is irreflexive on N: k∉k for every k∈N, and every natural number is a transitive set (Every natural number is a transitive set and is not a member of itself).

Proof

technique · cases
1.1

Since A is at most countable there is a bijection φ:A→N0 where N0=n for some n∈N or N0=N; in either case N0⊆N, and restricting φ to B gives a bijection of B onto S:=φ[B]⊆N, so B≈S. It therefore suffices to prove that every subset of N is at most countable, since then S≈n′ or S≈N and transitivity carries the conclusion back to B.

givenL1L2L6suffices: every subset of N is at most countable
1.2

Every subset of a natural number is finite: by strong induction on n, assume every subset of every m<n is finite. If n=0 then a subset T⊆0=∅ is empty and T≈0. Otherwise n=σ(m) by [L7], with m<n; given T⊆σ(m)=m∪{m}, the set T∖{m} is a subset of m, so the hypothesis at m gives a bijection u:T∖{m}→k for some k∈N. If m∉T then T=T∖{m}≈k. If m∈T, extend u by u(m):=k; since k∉k by irreflexivity of membership, the value k is not already taken and the extension is a bijection T→k∪{k}=σ(k). In both cases T is finite, so the claim holds for n and hence for all n.

L1L2L4L6L7L8
1.3

Case S bounded: assume there is b0∈N with s≤b0 for every s∈S. Then s<σ(b0) for every s∈S by [L6], that is, S⊆σ(b0).

assume-case boundedL6
1.4

Case S unbounded: assume that for every b∈N there is s∈S with b<s. Then S≠∅, and for each s∈S the set { t∈S:s<t } is nonempty, so [L3] makes ν(s):=min⁡{ t∈S:s<t } a well-defined element of S with s<ν(s); this defines a function ν:S→S with no arbitrary choices.

assume-case unboundedL3construct
2.1

In the bounded case S is a subset of the natural number σ(b0), hence finite by step 1.2, hence at most countable.

step 1.2step 1.3L1
2.2

In the unbounded case apply [L5] with X=S, x0=min⁡S (available by [L3] since S≠∅) and F=ν: there is e:N→S with e(0)=min⁡S and e(σ(n))=ν(e(n))=min⁡{ t∈S:e(n)<t } for every n.

step 1.4L3L5construct
3.1

For every n, e(n)<e(σ(n)) by the defining property of ν; consequently m<n implies e(m)<e(n), by strong induction on n (for n=σ(j) and m<n one has m≤j by [L6], so either m=j, giving e(m)<e(σ(j)) directly, or m<j, giving e(m)<e(j)<e(σ(j)) by the hypothesis at j and transitivity). Hence e is injective: if m≠n then m<n or n<m by comparability, and irreflexivity forbids e(m)=e(n).

step 2.2L4L6L7
3.2

For every k, k≤e(k): again by strong induction, at k=0 this is immediate, and for k=σ(j) the hypothesis at j gives j≤e(j)<e(σ(j)), so j<e(k) and therefore σ(j)≤e(k) by [L6], that is k≤e(k).

step 2.2L4L6L7
4.1

e is surjective onto S: let t∈S. The set K={ k∈N:t≤e(k) } contains t by step 3.2, so k∗:=min⁡K exists by [L3]. If k∗=0 then e(0)=min⁡S≤t because t∈S, and t≤e(0), so e(0)=t. Otherwise k∗=σ(j) by [L7], and j∉K by minimality, so e(j)<t; then t belongs to { u∈S:e(j)<u }, whence e(k∗)=min⁡{ u∈S:e(j)<u }≤t, and with t≤e(k∗) this gives e(k∗)=t. In both cases t is a value of e.

step 2.2step 3.2L3L6L7
5.1

In the unbounded case e:N→S is therefore a bijection, so S≈N and S is countably infinite, hence at most countable.

step 3.1step 4.1L1L2
6.1

Every S⊆N is either bounded above or not, so steps 2.1 and 5.1 cover all cases and every subset of N is at most countable; by the reduction of step 1.1 the subset B of the at most countable set A is at most countable.

step 1.1step 2.1step 5.1cases-exhaustiveL1L2∎

Remarks

  • A subset of a countably infinite set may perfectly well be finite: {0,1} and ∅ are subsets of N. This is exactly why the conclusion is "at most countable" and not "countably infinite", and it is why the library's convention that "countable" means "at most countable" (Finite, countably infinite, countable, uncountable) keeps the statement free of case distinctions.

  • The dichotomy proved here, bounded subsets of N are finite and unbounded ones are copies of N, is the only structural fact about N the rest of the page needs. The enumeration e built in the unbounded case is the increasing one, and it is unique with that property.

  • The bounded case rests on the von Neumann encoding: "bounded by b0" is literally "a subset of the set σ(b0)", which is what makes the induction of step 1.2 an induction on a natural number rather than on an informal count. That translation is not a convention but a theorem, On N the order is membership: m<n  ⟺  m∈n, since the library's order on N is defined additively (Order on the natural numbers) and not by membership.

Depends on

Used by

…and 17 more results.

Dependency tree · two levels

31 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