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.

The Schröder-Bernstein theorem

Statement

Let $A$ and $B$ be sets with $A ⪯ B$ and $B ⪯ A$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ). Then $A \approx B$ .

Equivalently: if there is an injection $A \to B$ and an injection $B \to A$ , then there is a bijection $A \to B$ (Injection, surjection, bijection).

The proof uses no choice principle. The bijection is written down explicitly from the two given injections, and the only "selections" it makes are of the unique preimage of a point under an injection, which is determined, not chosen. The single infinite construction is an application of the recursion theorem (The recursion theorem), whose data are a set, a starting point and one function.

Facts & Assumptions

Given: Sets $A$ and $B$ together with injections $f : A \to B$ and $g : B \to A$ . For $S \subseteq A$ write $f [S]$ for its image, and similarly for $g$ .

[L1]

Injection, surjection, bijection, image and preimage, and the fact that an injective $g$ has, for each $x \in g [B]$ , exactly one $b \in B$ with $g (b) = x$ (Injection, surjection, bijection).

[L2]

$A \approx B$ means precisely that some bijection $A \to B$ exists (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[L3]

Recursion theorem: for any set $X$ , any $x_{0} \in X$ and any $F : X \to X$ there is a (unique) function $h : N \to X$ with $h (0) = x_{0}$ and $h (σ (n)) = F (h (n))$ for all $n \in N$ (The recursion theorem, The natural numbers $N$ (von Neumann)).

[L4]

Every nonzero natural number is a successor: $n \neq 0$ implies $n = σ (m)$ for some $m \in N$ (Every nonzero natural number is a successor).

Proof

technique · direct

1.1

Apply [L3] with $X = P (A)$ (a set by the Power Set axiom), with $x_{0} = A ∖ g [B]$ , and with $F : P (A) \to P (A)$ defined by $F (S) = g [f [S]]$ : this yields a function $n \mapsto C_{n}$ from $N$ to $P (A)$ with $C_{0} = A ∖ g [B]$ and $C_{σ (n)} = g [f [C_{n}]]$ for every $n$ .

L3givenconstruct

2.1

Put $C = ⋃_{n \in N} C_{n}$ , a subset of $A$ (a set by Replacement and Union applied to the function of step 1.1); thus $x \in C$ if and only if $x \in C_{n}$ for some $n \in N$ , and $C_{σ (n)} \subseteq C$ for every $n$ .

step 1.1construct

3.1

Let $x \in A ∖ C$ . Then $x \notin C_{0} = A ∖ g [B]$ , so $x \in g [B]$ , and since $g$ is injective there is exactly one $b \in B$ with $g (b) = x$ ; write $b = g^{- 1} (x)$ , a value determined by $x$ alone.

step 2.1L1given

4.1

Define $h : A \to B$ by $h (x) = f (x)$ for $x \in C$ and $h (x) = g^{- 1} (x)$ for $x \in A ∖ C$ ; the two clauses have disjoint domains whose union is $A$ , and each assigns exactly one value, by step 3.1 for the second, so $h$ is a well-defined function.

step 3.1construct

5.1

If $x, y \in C$ and $h (x) = h (y)$ then $f (x) = f (y)$ , so $x = y$ because $f$ is injective; if $x, y \in A ∖ C$ and $h (x) = h (y) = b$ then $x = g (b) = y$ by step 3.1.

step 4.1givenL1

5.2

The remaining case cannot occur: if $x \in C$ and $y \in A ∖ C$ had $h (x) = h (y)$ , then $x \in C_{n}$ for some $n$ , and $h (y) = g^{- 1} (y)$ gives $y = g (h (y)) = g (f (x)) \in g [f [C_{n}]] = C_{σ (n)} \subseteq C$ , contradicting $y \notin C$ ; hence $h$ is injective.

step 1.1step 2.1step 4.1

5.3

$h$ is surjective: let $b \in B$ and consider $g (b) \in A$ . If $g (b) \notin C$ then $h (g (b)) = g^{- 1} (g (b)) = b$ . If $g (b) \in C$ then $g (b) \in C_{n}$ for some $n$ ; here $n \neq 0$ , since $g (b) \in g [B]$ while $C_{0} = A ∖ g [B]$ , so $n = σ (m)$ by [L4] and $g (b) \in C_{σ (m)} = g [f [C_{m}]]$ , that is, $g (b) = g (f (x))$ for some $x \in C_{m} \subseteq C$ ; injectivity of $g$ gives $b = f (x) = h (x)$ . Either way $b$ is a value of $h$ .

step 1.1step 2.1step 4.1L1L4given

6.1

Thus $h : A \to B$ is injective and surjective, hence a bijection, and therefore $A \approx B$ .

step 5.1step 5.2step 5.3L1L2∎

Remarks

The set $C$ is exactly the set of points of $A$ reachable from the "unmatched" part $A ∖ g [B]$ by applying $g \circ f$ finitely often. On $C$ the bijection follows $f$ forwards; off $C$ it runs $g$ backwards. Both halves are forced: a point outside $g [B]$ cannot be an image of $g$ , and once one point is handled by $f$ its $g \circ f$ image must be handled by $f$ too.
Why the choice-freeness is worth stating. Many textbook proofs phrase the construction as "follow the chain of preimages backwards until it stops", which sounds like an infinite sequence of selections. It is not: the preimage under an injection is unique when it exists, and the recursion above is a single application of The recursion theorem to one explicitly given function $S \mapsto g [f [S]]$ . The theorem is a theorem of ZF.
With this theorem, $⪯$ behaves like an order on equinumerosity classes: $A ⪯ B$ and $B ⪯ A$ give $A \approx B$ . Comparability, that $A ⪯ B$ or $B ⪯ A$ holds for any two sets, is a different matter entirely: over ZF it is equivalent to the Axiom of Choice (The Axiom of Choice), a classical result quoted here and proved nowhere on this page, the harder half of it going back to Hartogs. Nothing on this page uses comparability.

Depends on

Used by

Dependency tree · two levels

13 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

J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
J. Lebl, Basic Analysis: Introduction to Real Analysis, basic set theory (standard reference, not scraped)
Schröder-Bernstein theorem (Wikipedia) (standard reference, not scraped)
Countable set (Wikipedia) (standard reference, not scraped)