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.
Minimum-rank selection and Collection
Statement
In ZF every nonempty definable class has a least member-rank , and is a nonempty set. Replacement yields the Collection schema: if , a set exists with . Conversely, Separation and Collection yield Replacement for functional formulas.
Facts & Assumptions
Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.
In ZF, for every set and ordinal , Thus is the least with , and iff . (Rank characterizes hierarchy membership)
Proof
Instantiate one and minimize the ranks attained in among ordinals at most . Separation on and ordinal well-ordering yield a least such , which is globally least. All members of rank lie in , so Separation inside that stage forms the asserted nonempty set.
Given the Collection premise, for each the class of witnesses has a unique least rank by step 1.1. Replacement collects these ordinals; set . The stage contains at least one witness for each , because the witnesses of its minimum rank lie in . Thus suffices. For , take .
Conversely assume Separation and Collection, and let be functional on the set . Collection supplies a set containing a witness for each . Separation gives . Uniqueness ensures every value of occurs in this set and that every member is such a value, which is the Replacement conclusion. This direction does not use rank or a prior application of Replacement.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
3 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
- Marks, Set Theory, Berkeley edition — section 7 Scott trick and Exercise 7.8 p.35. (standard reference, not scraped)