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.
Constructible subsets appear before successor cardinals
Statement
In ZF, if is an infinite cardinal and with , then . More generally, if and , then for some .
Here is the Hartogs successor cardinal, so no ambient Choice is assumed.
Facts & Assumptions
Given: Ambient ZF, an infinite cardinal , and a constructible set satisfying one of the displayed subset hypotheses.
Canonical L-hulls are elementary and small makes the canonical hull of an infinite well-orderable seed elementary and of the same cardinality as that seed, without invoking Choice.
Condensation for constructible levels identifies the collapse of an elementary substructure of a nonzero limit -level as an actual level .
What the collapse fixes says that the collapse fixes a transitive subset included in the hull, and determines images by images of their members.
Cardinality of infinite constructible levels gives and a well-order of .
For every set the Hartogs number is a cardinal, and for every cardinal it is the least cardinal strictly above ; this is a theorem of ZF identifies with the least ordinal not injectible into .
Transitivity, growth, ordinals and rank in L gives transitivity and nesting of the constructible levels.
Proof
Choose a nonzero limit large enough that and the relevant finite seed belong to ; this is possible because is constructible and the -levels are nested and exhaustive for . For the first clause set , and for the second set . Each seed is a subset of . In the first case because is infinite; in the second F4 gives the same conclusion. Both seeds are well-orderable.
Let . By F1, and is well-orderable with . Collapse to . By F2 there is an ordinal with . Since and the collapse bijects with , there is an injection ; F5 therefore gives .
In the first case, , so F3 fixes every ordinal below . Since and , the recursive collapse equation gives . Thus . In the second case, is transitive by F6, so F3 fixes it pointwise; again and imply , whence .
We have proved the general clause with . For the first clause, nesting gives , so . The case is included, and no selection from a family of sets occurred: the hull is canonical and the cardinal bound uses only the Hartogs successor.
Depends on
Canonical L-hulls are elementary and small
Condensation for constructible levels
What the collapse fixes
Cardinality of infinite constructible levels
For every set the Hartogs number is a cardinal, and for every cardinal it is the least cardinal strictly above ; this is a theorem of ZF
Transitivity, growth, ordinals and rank in L