---
title: "Locating ordinals in the constructible hierarchy"
module: L.Ordinal.Stages
lang: en
site: "Bedrock"
description: "Locating ordinals in the constructible hierarchy"
stage: "Constructible stages and the axioms"
reading_order: 29
canonical: https://bedrock.institute/en/L.Ordinal.Stages.html
html: L.Ordinal.Stages.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Ordinal/Stages.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping, V.Hierarchy, V.Model, L.Definability, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Rank]
routes: [constructible-axioms]
translations: [https://bedrock.institute/zh/L.Ordinal.Stages.md, https://bedrock.institute/ja/L.Ordinal.Stages.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Locating ordinals in the constructible hierarchy

An ordinal's position in the constructible hierarchy is controlled by membership: it appears by its successor stage and cannot appear before its own rank. This chapter proves both directions and gives a bounded formula for recognizing ordinals inside a stage.

One question about the tower is still open, and it is the one the axiom of infinity turns on: given a stage, exactly which ordinals have appeared by then? The answer is as clean as it could be. The ordinals in `Lset α` are precisely the members of `α`, so the tower's index and its ordinal content agree, level for level, and an ordinal first appears at the stage after itself.

Both directions require real work. One direction says an ordinal cannot appear early: if it is in `Lset α` then it is a member of `α`. That is the harder one, and it goes through rank, which is why the rank construction is needed here. A set in `Lset α` is a definable subset of some earlier stage, its members therefore have rank below that stage by induction, and so its own rank is bounded; being an ordinal, it is its own rank.

The other direction says an ordinal cannot appear late: every member of `α` is already in `Lset α`. That one is a straight induction, given that an ordinal appears at the stage after itself, which is the theorem being proved. The circularity is only apparent: the induction hypothesis supplies the statement for the members, and the members are the only thing needed.

With both halves the ordinals of a stage are carved out of it by a single formula, "is an ordinal", which is Δ₀ because transitivity can be said with bounded quantifiers alone. So `α` is a definable subset of `Lset α`, and the definable-power-set clause for the successor stage then applies.

The chapter works inside a fixed universe level ℓ, and everything that follows speaks about sets, membership, and stages of L at that level. We assume excluded middle at level ℓ-suc ℓ. Its sole mathematical use is ordinal trichotomy: for two ordinals, one of membership in either direction or equality is returned. Every later conclusion inherits this classicality through the two comparison lemmas built in the next section.

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Ordinal.Stages {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

Two kinds of vocabulary meet here. From the ambient hierarchy V come the basic moves: membership ∈ˢ on the set S, the von Neumann successor `sucV`, induction and irreflexivity along membership. From the constructible side come the stages `Lset α` themselves, the definable-subset layer `𝒟ₒ`, and the two directions `Lset-in` and `Lset-out` relating membership in a stage to membership in its definable power set. The chapter's statement lives entirely in this intersection: it asks where an ordinal sits among the `Lset α`.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-∧; δ-∀∈ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-irrefl )
```

Ordinals enter as the predicate `IsOrd`: a set is an ordinal exactly when it is transitive and all of its members are transitive. This is the von Neumann reading, where the ordinal α is the set of all smaller ordinals, so asking whether an ordinal has appeared at a stage is literally a membership question. Also from earlier chapters come `mem-ord` and `suc-ord`, the closure facts that a member of an ordinal is an ordinal and that the successor of an ordinal is an ordinal; they keep every stage index in the argument an honest ordinal.

```agda
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}
  using ( IsOrd; isTransV; Lset; Lset-layer; layer-trans
        ; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv; Lset-mono; Lset-in; Lset-out )
```

The decision procedure behind everything is `ord-tri`: given two ordinals, each certified to be one, it returns which of the three cases holds, a ∈ b, a = b, or b ∈ a. It uses the stated excluded-middle assumption. The comparison returns a sum of three cases; impossible branches land in the empty type. Separately, propositional truncation ∣_∣₁ records that the earlier stage witnessing a stage decomposition merely exists.

```agda
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Rank {ℓ} using ( rank; rank-upper; rank-ord; rank-fix )

open import Cubical.Data.Sum as Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
```

The rank construction supplies three properties. For a set x, `rank x` is an ordinal collecting how deep x sits in the cumulative hierarchy; `rank-ord` certifies it is an ordinal, `rank-fix` identifies the rank of an ordinal with the ordinal itself, and `rank-upper` bounds the rank of a set from bounds on the ranks of its members. These are the facts needed for the harder direction.

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; extensionality; _⊆_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
```

To connect ambient membership with formulas over a stage, a set A has a chosen presentation ⟪ A ⟫, and `∈-asFiber` passes from membership in A to an index naming that member. Mutual inclusion gives equality through `extensionality`. Formula satisfaction is interpreted directly in `hProp`: each formula denotes an hProp. These identifications let the argument pass between sets, their indices and bounded formulas.

```agda
  using ( module InfinitySet )
open InfinitySet using ( sucV )

open hPropStructure 𝒮ᵥ
```

## Comparison, twice

Trichotomy leaves exactly three mathematical possibilities. If a belongs to b, it belongs to the successor of b; if a = b, then a belongs to that successor as its new top element. The only remaining possibility, b ∈ a, will be ruled out by the inclusion a ⊆ b.

Suppose a ⊆ b for sets a and b, and compare them by trichotomy. If a is a member of b, the first helper applies `∈sucV-inl`: a member of b is automatically a member of `sucV b`, since the successor is b together with its singleton. If a equals b, the second helper transports the fact `self∈sucV b`, that b belongs to its own successor, along the path a ≡ b. Two of the three cases are already closed.

```agda
private
  ∈-case : (a b : S) → ⟨ a ∈ˢ b ⟩ → ⟨ a ∈ˢ sucV b ⟩
  ∈-case a b a∈b = ∈sucV-inl a∈b

  ≡-case : (a b : S) → a ≡ b → ⟨ a ∈ˢ sucV b ⟩
  ≡-case a b a≡b = subst (λ w → ⟨ w ∈ˢ sucV b ⟩) (sym a≡b) (self∈sucV b)
```

The remaining case is b ∈ a, which inclusion rules out: b ∈ a and a ⊆ b would give b ∈ b, contradicting `∈-irrefl`. From this contradiction the desired conclusion a ∈ sucV b follows. Hence for ordinals a and b, inclusion a ⊆ b forces a ∈ sucV b.

```agda
  wit-case : (a b : S) → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩)
           → ⟨ b ∈ˢ a ⟩ → ⟨ a ∈ˢ sucV b ⟩
  wit-case a b a⊆b b∈a = Empty.rec (∈-irrefl b (a⊆b b b∈a))

⊆→∈suc : (a b : S) → IsOrd a → IsOrd b
       → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩) → ⟨ a ∈ˢ sucV b ⟩
```

This is the first use of the classical comparison. Everything done after the trichotomy result is returned is constructive; the second successor comparison below uses the same principle once more.

```agda
⊆→∈suc a b orda ordb a⊆b = Sum.rec
  (∈-case a b)
  (Sum.rec (≡-case a b) (wit-case a b a⊆b))
  (ord-tri a orda b ordb)
```

Now suppose β ∈ α. Trichotomy compares sucV β with α, so either the successor still lies inside α, it equals α, or α lies inside sucV β. The type `Out β α` records the first two alternatives; the third will contradict β ∈ α.

The impossible case is discharged inside `overshoot`, whose premises are exactly the two facts that cannot hold at once: α belongs to `sucV β` while β belongs to the ordinal α. Unfolding a member of `sucV β` with `∈sucV-elim` gives two subcases: α ∈ β, or α = β. The elimination principle demands that the target be a proposition, and the empty type `⊥*` is one, so both branches may end in a contradiction.

```agda
private
  Out : S → S → Type (ℓ-suc ℓ)
  Out β α = ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)

  overshoot : (β α : S) → IsOrd α → ⟨ β ∈ˢ α ⟩ → ⟨ α ∈ˢ sucV β ⟩ → Out β α
  overshoot β α ordα β∈α α∈sβ = Empty.rec*
```

In the first subcase we have the membership chain α ∈ β ∈ α. Transitivity of α, its first component `ordα .fst`, composes the chain to α ∈ α. In the second, α = β transports β ∈ α along the reversed path and again yields α ∈ α. Both contradict `∈-irrefl`, so the impossible third alternative entails the required conclusion `Out β α`.

```agda
    (∈sucV-elim {A = β} {x = α} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.isProp⊥* α∈sβ
      (λ α∈β → lift (∈-irrefl α (ordα .fst α∈β β∈α)))
      (λ α≡β → lift (∈-irrefl α (subst (λ w → ⟨ w ∈ˢ α ⟩) (sym α≡β) β∈α))))

suc∈or≡ : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
        → ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)
```

The lemma proper now runs the trichotomy between `sucV β` and α, both certified ordinals, `sucV β` via `suc-ord`. The first two cases already have the required shape, membership or equality, and are returned directly.

```agda
suc∈or≡ β α ordβ ordα β∈α = go (ord-tri (sucV β) (suc-ord ordβ) α ordα)
  where
  go : (⟨ sucV β ∈ˢ α ⟩ ⊎ ((sucV β ≡ α) ⊎ ⟨ α ∈ˢ sucV β ⟩)) → Out β α
  go (inl s∈α)        = inl s∈α
  go (inr (inl s≡α))  = inr s≡α
```

The third case, α ∈ sucV β, is precisely the premise of `overshoot`, and feeding it the standing hypothesis β ∈ α closes the analysis. The conclusion `suc∈or≡` is the sharp form of "no overshoot": below α, the successor stages of members of α are never strictly beyond α.

```agda
  go (inr (inr α∈sβ)) = overshoot β α ordα β∈α α∈sβ
```

And the cumulation lemma it is used for: an ordinal that has appeared at its own successor stage has appeared at every later stage, where later means the index is above it.

This is the bridge between the pointwise statement "β appears at sucV β" and the stage-level statement "every member of α is in Lset α". Given β ∈ α, the successor sucV β sits inside α or coincides with it, and either way membership in the smaller stage transports into membership in `Lset α`.

The membership branch uses monotonicity of stages: `Lset-mono` says that if γ ∈ δ then `Lset γ` is included in `Lset δ`, so a member of the earlier stage is a member of the later one. Here γ = sucV β and δ = α, exactly the first case of `suc∈or≡`.

```agda
private
  cumul-∈ : (β α : S) → ⟨ sucV β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset (sucV β) ⟩
          → ⟨ β ∈ˢ Lset α ⟩
  cumul-∈ β α s∈α = Lset-mono {α = α} {β = sucV β} s∈α {x = β}

  cumul-≡ : (β α : S) → sucV β ≡ α → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩
```

The equality branch is the degenerate one: when sucV β is not strictly below but equal to α, membership in `Lset (sucV β)` is already membership in `Lset α`, and the transport along the path makes this literally so. The statement of `Lset-cumul` takes the two ordinal certificates and the appearance hypothesis, and dispatches on `suc∈or≡`.

```agda
  cumul-≡ β α s≡α = subst (λ w → ⟨ β ∈ˢ Lset w ⟩) s≡α

Lset-cumul : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
           → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩
Lset-cumul β α ordβ ordα β∈α β∈Lsβ =
  Sum.rec (λ s∈α → cumul-∈ β α s∈α β∈Lsβ)
```

Note the shape of the result: it does not say that β ∈ Lset α for all β ∈ α outright, since that appearance at the successor stage is still a hypothesis. The final theorem will supply that hypothesis by induction, and this lemma is exactly the step that turns it into stage content.

```agda
          (λ s≡α → cumul-≡ β α s≡α β∈Lsβ)
          (suc∈or≡ β α ordβ ordα β∈α)
```

## Nothing appears before its rank

If a set belongs to `Lset α`, its rank is bounded by `α`. Applied to an ordinal, whose rank agrees with itself, this shows that the ordinal cannot occur at an earlier stage.

The harder half. By induction on the stage index: a set in `Lset α` lies in the definable subsets of `Lset β` for some `β` in `α`, so it is a subset of `Lset β`; each of its members therefore has rank in `β` by the inductive hypothesis; so its own rank, which is the union of the successors of those ranks, is included in `β`; comparison puts it inside the successor of `β`, and that is inside `α`.

One notational point about the induction: membership in a truncated existential is itself truncated, and the induction is stated over the truncated form β ∈ᵗ α rather than over explicit members. The goal, a membership statement, is a proposition, so eliminating that truncation with `PT.rec` is legitimate.

The statement quantifies over all ordinals α at once, and ∈-induction is applied to the whole predicate as a function of α, with the ordinal certificate carried along as an argument. The induction is on membership in α, so the inductive hypothesis at α speaks about members β of α, not about earlier stages by any list order.

```agda
rank-Lset : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩
rank-Lset = ∈-induction
  {P = λ α → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩} step
  where
  step : (α : S)
```

The key step exposes what x ∈ Lset α means: by `Lset-out`, x merely belongs to a definable-subset layer over some β ∈ α. The layer membership is again truncated, but the conclusion rank x ∈ α is a proposition, so `PT.rec` may eliminate the truncation and work with the fiber β, β∈α, x∈𝒟ₒLβ as if it were given.

```agda
       → (∀ β → β ∈ᵗ α → IsOrd β → (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ rank x ∈ˢ β ⟩)
       → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩
  step α IH ordα x x∈Lα = PT.rec (snd (rank x ∈ˢ α)) fromStage (Lset-out α x x∈Lα)
    where
    fromStage : Σ[ β ∈ S ] (⟨ β ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩) → ⟨ rank x ∈ˢ α ⟩
```

Inside the fiber, everything needed to run the induction hypothesis is recovered. The member β of the ordinal α is itself an ordinal by `mem-ord`, which is what lets the inductive hypothesis fire at β.

```agda
    fromStage (β , β∈α , x∈𝒟ₒLβ) = rankx∈α
      where
      ordβ : IsOrd β
      ordβ = mem-ord {A = α} ordα β β∈α
      x⊆Lβ : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ Lset β ⟩
```

Definability of x over `Lset β` means x is a subset of it: `𝒟ₒ-inv` unpacks the certificate and `DefOf.Def∋⊆A` turns it into the inclusion x ⊆ Lset β. Composing with the inductive hypothesis, every member y of x has rank in β. Then `rank-upper`, given exactly such bounds on member ranks, includes `rank x` itself into β.

```agda
      x⊆Lβ = DefOf.Def∋⊆A (Lset β) x (𝒟ₒ-inv (Lset β) x x∈𝒟ₒLβ)
      ry∈β : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ rank y ∈ˢ β ⟩
      ry∈β y y∈x = IH β β∈α ordβ y (x⊆Lβ y y∈x)

      rankx⊆β : (z : S) → ⟨ z ∈ˢ rank x ⟩ → ⟨ z ∈ˢ β ⟩
      rankx⊆β = rank-upper x β ordβ ry∈β
```

What remains is to lift rank x ∈ sucV β into rank x ∈ α. Both rank x and β are ordinals, the former by `rank-ord`, and `⊆→∈suc` from the first section applies to their inclusion, placing rank x in the successor of β. The elimination `∈sucV-elim` then compares with the known β ∈ α: if rank x is a member of β, transitivity of α lifts the membership one step; if rank x equals β, the path transports β ∈ α directly. Either way the rank lands in α, completing the induction.

```agda
      rankx∈α : ⟨ rank x ∈ˢ α ⟩
      rankx∈α = ∈sucV-elim {A = β} {x = rank x} (snd (rank x ∈ˢ α))
        (⊆→∈suc (rank x) β (rank-ord x) ordβ rankx⊆β)
        (λ rx∈β → ordα .fst rx∈β β∈α)
        (λ rx≡β → subst (λ w → ⟨ w ∈ˢ α ⟩) (sym rx≡β) β∈α)
```

For an ordinal the conclusion simplifies, because rank fixes it: an ordinal in `Lset α` is a member of `α`. This is the lower bound of the chapter's characterization in its usable form.

The step is a transport: `rank-fix x ordx` gives the path rank x ≡ x, and substituting along it converts the rank bound rank x ∈ α into the membership x ∈ α. Note the direction, which the induction above guarantees: appearance in a stage forces membership in the index, not the converse.

```agda
ord∈Lset→∈ : (α : S) → IsOrd α → (x : S) → IsOrd x → ⟨ x ∈ˢ Lset α ⟩
           → ⟨ x ∈ˢ α ⟩
ord∈Lset→∈ α ordα x ordx x∈Lα =
  subst (λ w → ⟨ w ∈ˢ α ⟩) (rank-fix x ordx) (rank-Lset α ordα x x∈Lα)
```

## Being an ordinal, said with bounded quantifiers

Being a transitive set all of whose members are transitive can be expressed with bounded quantifiers. The formula therefore recognizes ordinals absolutely between a transitive stage and the ambient universe.

The predicate is two clauses, and both are already bounded: a set is transitive when every member of every member of it is a member of it, and its members are transitive when the same holds one level down. No unbounded quantifier appears, so the formula is Δ₀, and no constant appears either, which spares the whole relabelling apparatus.

The indices are de Bruijn: each bounded quantifier binds a fresh variable `0` and pushes the earlier ones outward, so after two binders the candidate ordinal is at index 2.

The first clause says transitivity. Its bounded quantifier ∀̇∈ ranges over members of the value bound one step out; reading the de Bruijn indices, after one binder the members live at index 0 and the candidate at index 1, and inside the second binder the atomic formula demands y ∈ x with y at 0 and x pushed to 2. The formula is polymorphic in the alphabet K of constants but uses none, so the same syntax serves every interpretation.

```agda
φ-ord : ∀ {ℓk} {K : Type ℓk} → Formula K 1
φ-ord =
  (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
  ∧̇
  (∀̇∈ (var zero)
```

The second clause stacks one more quantifier: a member x of the candidate, a member y of x, and a member z of y must land back in the candidate, which says each member of the candidate is transitive. Three binders later, the innermost variable is at 0 and the candidate at 3. The certificate `φ-ord-Δ₀` is built from the same three primitive certificates, δ-∈ for atomic membership, δ-∀∈ for bounded quantifiers, and δ-∧ for the conjunction, mirroring the formula's construction step by step.

```agda
    (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))

φ-ord-Δ₀ : ∀ {ℓk} {K : Type ℓk} → Δ₀ (φ-ord {K = K})
φ-ord-Δ₀ = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
```

## The ordinals of a stage

Separation by the bounded ordinal formula collects exactly the ordinals belonging to a stage. Its membership specification is available both internally and in the ambient universe.

Fix a stage. Using bounded absoluteness for the transitive stage, satisfaction of the formula in the ambient hierarchy unfolds to exactly the two clauses of the ordinal predicate, so the two are interchangeable by reshuffling arguments. Then the definable subset it carves is `α` itself: a member of it is an ordinal of the stage, hence a member of `α` by the rank half; and a member of `α` is an ordinal that has already appeared, by cumulation, so it satisfies the formula.

Cumulation needs, for each member of `α`, that it appears at its own successor stage. That is the theorem itself, so it enters here as a hypothesis, and the induction below is what supplies it.

Fix the ordinal α with its certificate. The stage A = `Lset α` is a layer, and `layer-trans` upgrades that to transitivity of A as a set, the only hypothesis under which the Δ₀ formula will be absolute between A's internal satisfaction and the ambient universe. The definability machinery of the chapter on L.Definability is opened relative to A, so `defSet φ` below always means the subset φ defines out of A.

```agda
module OrdAt (α : S) (ordα : IsOrd α) where
  private
    A = Lset α
    Atrans = layer-trans (Lset-layer α)
    module DefA = DefOf A
```

Members of A present themselves through the fiber ⟪ A ⟫: an index m names the element ⟪ A ⟫↪ m of A. The formula φ is our φ-ord instantiated at the carrier ⟪ A ⟫, so it has one free-variable slot, occupied by the environment ⟪ A ⟫↪ m ∷ []. Because φ has no constants, `mapFo DefA.ι φ` merely relabels through the constant interpretation ι, which for this formula changes nothing syntactically. The satisfaction sign ⊨ᵛ here is the ambient one, from the absoluteness refinement.

```agda
    module RefA = DefA.Refine Atrans
    open RefA.Abs using ( _⊨ᵛ_ )

    φ : Formula ⟪ A ⟫ 1
    φ = φ-ord {K = ⟪ A ⟫}

  ⊨ᵛ→ord : (m : ⟪ A ⟫) → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
```

The first direction reads satisfaction into the ordinal predicate. The satisfaction of a conjunction is a pair, and its first component is exactly the first bounded clause applied to x = B, the presented element: every y ∈ x with x ∈ B lands back in B. That is the transitivity condition for B, so the pair's first projection is a certificate that B is transitive.

```agda
         → IsOrd (⟪ A ⟫↪ m)
  ⊨ᵛ→ord m sat = transB , memTransB
    where
    B = ⟪ A ⟫↪ m
    transB : isTransV B
```

The second component is the second clause, with the quantifiers nested one deeper: for x ∈ B, y ∈ x and z ∈ y, the element z lands in B. That says precisely that every member x of B is itself transitive, so together with the first projection the satisfaction data is exactly an IsOrd certificate for B.

```agda
    transB {x} {y} y∈x x∈B = sat .fst x x∈B y y∈x
    memTransB : (x : S) → ⟨ x ∈ˢ B ⟩ → isTransV x
    memTransB x x∈B {y} {z} z∈y y∈x = sat .snd x x∈B y y∈x z z∈y

  ord→⊨ᵛ : (m : ⟪ A ⟫) → IsOrd (⟪ A ⟫↪ m)
         → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
```

The converse direction assembles a satisfaction from an ordinal certificate. Its first component must accept x ∈ B and y ∈ x and return y ∈ B, and transitivity of B, the first component of the IsOrd pair, does exactly that with the arguments in the right order.

```agda
  ord→⊨ᵛ m ord = c1 , c2
    where
    B = ⟪ A ⟫↪ m
    c1 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ B ⟩
    c1 x x∈B y y∈x = ord .fst y∈x x∈B
```

The second component must chain three memberships back into B, and the second clause of the IsOrd pair is exactly that chain. So satisfaction of φ and the ordinal predicate are interchangeable in both directions; the two formulations express the same mathematical condition. With this equivalence established, the main statement takes shape: the definable subset selected by φ equals α, proved by `extensionality` from two inclusions, and stated under the explicit hypothesis α⊆A that every member of α has already appeared in A.

```agda
    c2 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩
       → (z : S) → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩
    c2 x x∈B y y∈x z z∈y = ord .snd x x∈B z∈y y∈x

  defSet-φ-ord : ((β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ A ⟩) → DefA.defSet φ ≡ α
  defSet-φ-ord α⊆A = extensionality (DefA.defSet φ) α (sub₁ , sub₂)
```

The inclusion from the definable subset to α is where the rank half of the chapter earns its keep. Membership in a definable subset unfolds by `∈∈ₛ` into a presentation-level fact, so sub₁ takes y with a proof that y belongs to `defSet φ` and must produce y ∈ α.

```agda
    where
    sub₁ : ⟨ DefA.defSet φ ⊆ α ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = α} .fst
      (y∈α (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ))
      where
```

Three conversions stack here. Membership of y in the definable subset yields membership in A by `defSet⊆A`, since the subset is contained in the stage. The chosen presentation turns this membership proof, via `∈-asFiber`, into an index m and a path q identifying y with the element named by m.

```agda
      y∈α : ⟨ y ∈ˢ DefA.defSet φ ⟩ → ⟨ y ∈ˢ α ⟩
      y∈α y∈def = ord∈Lset→∈ α ordα y ordy y∈A
        where
        y∈A = DefA.defSet⊆A φ y y∈def
        fib = ∈-asFiber {a = y} {b = A} y∈A
```

The path q transports membership from y to the presented element ⟪ A ⟫↪ m. Because φ is Δ₀ and A is transitive, `abs-defSet` identifies the hProp of membership in `defSet φ` with the hProp of ambient satisfaction of `mapFo ι φ` at the one-element environment. Substitution along these paths yields the required inhabitant sat; path transport itself imposes no propositionality condition.

```agda
        m = fib .fst
        q = fib .snd
        sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
        sat = subst ⟨_⟩ (RefA.abs-defSet φ φ-ord-Δ₀ m)
                (subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) (sym q) y∈def)
```

From sat, the implication `⊨ᵛ→ord` returns an IsOrd certificate for the presented element, and transporting along q turns it into one for y itself. Then `ord∈Lset→∈`, the rank half, places y inside α. So an arbitrary member of the definable subset is an ordinal of the stage, and the stage index contains it.

```agda
        ordy : IsOrd y
        ordy = subst IsOrd q (⊨ᵛ→ord m sat)

    sub₂ : ⟨ α ⊆ DefA.defSet φ ⟩
    sub₂ y y∈ₛ = ∈∈ₛ {a = y} {b = DefA.defSet φ} .fst
      (y∈def (∈∈ₛ {a = y} {b = α} .snd y∈ₛ))
```

The reverse inclusion runs the same circuit backward. A member y of α arrives with its ordinal certificate already in hand, from `mem-ord`. The hypothesis α⊆A presents y inside the stage via a fiber m, q, and `ord→⊨ᵛ` gives ambient satisfaction of φ at that environment.

```agda
      where
      y∈def : ⟨ y ∈ˢ α ⟩ → ⟨ y ∈ˢ DefA.defSet φ ⟩
      y∈def y∈α = subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) q
        (subst ⟨_⟩ (sym (RefA.abs-defSet φ φ-ord-Δ₀ m)) sat)
        where
```

Absoluteness now converts in the other direction: ambient satisfaction of the Δ₀ formula is membership of ⟪ A ⟫↪ m in `defSet φ`, and transporting along q lands the membership on y itself, inside the definable subset. No choice is made anywhere: each fiber m, q is used locally, on the very y that produced it.

```agda
        ordy = mem-ord {A = α} ordα y y∈α
        y∈A = α⊆A y y∈α
        fib = ∈-asFiber {a = y} {b = A} y∈A
        m = fib .fst
        q = fib .snd
```

The two inclusions close, and `defSet-φ-ord` states the conclusion: the subset the bounded formula carves out of `Lset α` is exactly α. Everything so far is conditional on α⊆A; the next section removes the condition, and with it the chapter's main theorem falls into place.

```agda
        sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
        sat = ord→⊨ᵛ m (subst IsOrd (sym q) ordy)
```

## An ordinal appears at its successor

Every ordinal is a definable subset of itself, selected by the bounded ordinal formula. Hence `α` belongs to the definable power set of `Lset α`, which is the successor stage.

The remaining gap is the inclusion `α ⊆ Lset α`, which the previous section had to assume. It is filled by induction on membership: the induction hypothesis states the theorem for each member `β` of `α`, so `β` appears in `Lset (sucV β)`, and cumulation from the first section raises it into `Lset α`. Once every member has accumulated, `α` is carved out of `Lset α` by the formula, and one branch of the union in the definition of the next stage contains it. The circularity is only apparent, because the induction hypothesis concerns the members, not `α` itself.

Two small facts are packaged before the induction. The first is a one-way bridge from definable power set to stage: a certificate that `α` lies in `𝒟ₒ (Lset α)`, meaning `α` is a definable subset of `Lset α`, is exactly the data `Lset-in` needs, once combined with `self∈sucV α`, which says `α` belongs to its own successor. The second line begins the theorem itself, and the induction principle for membership is applied directly: the statement being proved by induction is the theorem, relativized to each ordinal.

```agda
private
  𝒟ₒ→Lset-suc : (α : S) → ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩ → ⟨ α ∈ˢ Lset (sucV α) ⟩
  𝒟ₒ→Lset-suc α α∈𝒟ₒ = Lset-in (sucV α) α α (self∈sucV α) α∈𝒟ₒ

ord∈Lset-suc : (α : S) → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩
ord∈Lset-suc = ∈-induction
```

The induction step receives, for every member `β` of `α`, the theorem's conclusion at `β`, and must produce it at `α`. Since the previous section already reduced the goal to the single hypothesis `α ⊆ Lset α`, all the step does is assemble that inclusion and hand the result to the bridge lemma. Nothing about `α` beyond its ordinalhood and the induction hypothesis is used.

```agda
  {P = λ α → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩} step
  where
  step : (α : S) → (∀ β → β ∈ᵗ α → IsOrd β → ⟨ β ∈ˢ Lset (sucV β) ⟩)
       → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩
  step α IH ordα = 𝒟ₒ→Lset-suc α α∈𝒟ₒ
```

The inclusion is built member-by-member. For each `β` in `α`, being a member of the ordinal `α` makes `β` an ordinal in its own right, and the induction hypothesis places it in `Lset (sucV β)`; the cumulation lemma of the first section, whose second comparison was designed for exactly this shape, then lifts it to `Lset α`. This is where the earlier comparison lemmas pay off: a single case split on whether `sucV β` lies in `α` or equals it covers every member at once.

```agda
    where
    α⊆A : (β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset α ⟩
    α⊆A β β∈α = Lset-cumul β α ordβ ordα β∈α (IH β β∈α ordβ)
      where
      ordβ = mem-ord {A = α} ordα β β∈α
```

With `α ⊆ Lset α` in hand, the previous section's conclusion applies verbatim: the definable subset of `Lset α` selected by `φ-ord` is `α` itself. The certificate is supplied merely, by truncation, since a member of `𝒟ₒ` needs only some defining formula and proof of agreement, and the pair of `φ-ord` with the extensionality argument from `OrdAt` is exactly such a witness. The bridge lemma then moves `α` into `Lset (sucV α)`, completing the induction and the theorem.

```agda
    α∈𝒟ₒ : ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩
    α∈𝒟ₒ = 𝒟ₒ-intro (Lset α) α
      ∣ φ-ord {K = ⟪ Lset α ⟫} , OrdAt.defSet-φ-ord α ordα α⊆A ∣₁
```

## Recap

Ordinals now have exact stage bounds: `α` appears in `Lset (sucV α)`, and appearance in `Lset β` forces `α ∈ β`. The bounded ordinal formula makes these facts available to later internal arguments.

`ord∈Lset-suc` says an ordinal appears at the stage after itself, and `ord∈Lset→∈` says it appears no earlier. Together the ordinals of `Lset α` are exactly the members of `α`. The chapter is classical, through the two comparisons of its first section, and everything else it uses was constructive. The module `L.Stage` applies this result to `ω`, completing the proof of the axiom of infinity.