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.
Transitivity, growth, ordinals and rank in L
Statement
In ZF every is transitive, and implies . Moreover
For , iff . Thus is transitive and contains all ordinals.
Facts & Assumptions
Given: ZF. Checked transitivity via parameter-defined members, successor power-set bounds, bounded ordinalhood on arbitrary transitive levels, and both least-rank implications.
The constructible hierarchy and constructible rank: The hierarchy uses Def at successors, union at limits, and rank is the first successor membership stage minus one.
Ordinals and omega in transitive models: Ordinalhood has the bounded absolute characterization proved there, valid over any nonempty transitive membership domain.
Transitivity and growth of hierarchy stages: The cumulative hierarchy grows by power sets and unions and has the stated ordinal intersections.
Proof
If is transitive, every is the subset of defined by , so . Each is a subset of ; hence implies . This proves transitivity of Def(A), including by its special clause. Set transfinite induction along each ordinal interval now proves transitivity of the levels and nesting: successors use this observation; limits are increasing unions.
Induct simultaneously against the cumulative hierarchy. At zero the inclusion is equality. If , every member of is a subset of , hence is in . At limits take unions. Thus ; in particular any ordinal in is less than .
Induction proves that every ordinal below belongs to . Zero is immediate. Given , for the bounded ordinalhood formula over the transitive nonempty defines precisely the subset , so . For , . Old ordinals remain by nesting, and limit stages take unions. This proves the ordinal intersection identity and .
The formula defines the whole set over itself when nonempty, and Def(empty) contains empty. Hence . For , its first membership stage is . If , leastness gives and so . Conversely that inequality and nesting place in . Transitivity of the class union follows from transitivity of each level; step 3.1 puts every ordinal in that union.
Depends on
Used by
Dependency tree · two levels
10 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
- Geschke Lemmas 5.1,5.3,5.5,5.6(a) pp14–15; Marks Lemma 20.3 pp86–87 (standard reference, not scraped)