TheoremStatement: AI-adaptedProof: AI-adaptedprecheck pass

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.1L3givenconstruct

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$ .

2.1step 1.1construct

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$ .

3.1step 2.1L1given

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.

4.1step 3.1construct

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.

5.1step 4.1givenL1

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.

5.2step 1.1step 2.1step 4.1

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.

5.3step 1.1step 2.1step 4.1L1L4given

$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$ .

6.1step 5.1step 5.2step 5.3L1L2∎

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

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, as proved later in Comparability of arbitrary sets, that any two sets admit an injection one way or the other, is equivalent to the Axiom of Choice ↗ using Hartogs' theorem. This is an orientation reference, not an assumption of the present theorem. Nothing on this page uses comparability.

The Schröder-Bernstein theorem

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources