Definable subsets of a set

For a set A, the operator Def A collects exactly the subsets of A defined by a first-order formula over the restricted structure on A, with finitely many parameters from A. Its membership theorem exposes the formula, environment, and satisfaction relation used by later constructibility arguments.

Two design points carry the chapter. The formulas take A's small member type ⟪ A ⟫ as their constant domain, so "parameters from A" is enforced by the type. And satisfaction is the inner semantics, on the restricted structure 𝒮ᵥ ↾ (∈ A): quantifiers range over members of A only, which is what "definable in (A, ∈)" means in the textbook, and which lets the essential smallness of the previous chapters apply here: every formula evaluates small, so Def A is a set, with no resizing needed at all.

The question of this chapter: for a set A, which subsets of A can be singled out by a first-order formula interpreted inside (A, ∈)? The answer will be collected into a single operator Def A, itself a set of the ambient hierarchy. Everything takes place at one fixed universe level ℓ, so that Def A is small enough to exist as a set at the same level as A.

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

open import Base.Prelude

module L.Definability {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; Transitive )

The formulas come from an inductive object language: Formula K n has constants indexed by a type K and n slots indexing free variables, with atoms built from a structure's membership and equality relations. Choosing K = ⟪ A ⟫, the small member type of A, makes "parameters from A" true by construction: every constant names a member of A. The bounded fragment Δ₀ will matter later, when the inner and outer readings of satisfaction are compared; constant mapping and relabelling are the operations that move a formula between constant domains and transport satisfaction along such a move.

open import FOL.Syntax using ( Formula; var; con; _∈̇_; ⊤̇ )
open import FOL.LevyHierarchy using ( Δ₀ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import FOL.Manipulation.Relabelling using ( mapΔ₀; ⊨-map )
import FOL.Absoluteness

"Definable in (A, ∈)" means quantifiers may only range over members of A. So satisfaction must be taken in the structure restricted to the class x ↦ x ∈ˢ A, not in the ambient hierarchy. The chapter works over the ambient structure 𝒮ᵥ carried by the level-ℓ hierarchy, with carrier S and membership ∈ₛ; the restriction to A and the smallness of the restricted world come from the smallness chapter: given a class, a small type with an equivalence to the restricted carrier, and a constant interpretation, it rebuilds the restricted structure and proves every formula evaluates to a small proposition there. The restriction class here is simply membership in A.

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Smallness {ℓ} using ( module InnerSmall )

open import Cubical.Foundations.Equiv
  using ( _≃_; equivFun; invEq; invEquiv; compEquiv; propBiimpl→Equiv )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )

Essential smallness is what lets satisfaction become an index for a set. Since each formula evaluates to a small proposition inside (A, ∈), the members of A satisfying a formula can be indexed by a small type, and the hierarchy constructor sett turns a small index type and an indexing map into a set. Both the subset defined by one formula and Def itself will be built this way. Membership in a sett is then only a truncated existence statement, and propositions-valued targets force truncation to be eliminated into propositions rather than yielding chosen witnesses. The shape of the constructions produces the chapter's path-based specifications.

open import Cubical.Data.Sigma using ( Σ-cong-equiv-snd )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )

Finally, the vocabulary of truth values. The connectives and quantifiers act directly on propositions in hProp (ℓ-suc ℓ), so satisfaction takes values in hProp (ℓ-suc ℓ), with ⟨ p ⟩ projecting the underlying proposition of an hProp. Equality of such propositions is a path, so specifications about membership will be stated as paths of propositions and proved by chains of them. With this setup, the next section fixes one set A and defines its definable subsets.

open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber; presentation
        ; isEmb⟪_⟫↪; _⊆_; extensionality )

open ZFStructure 𝒮ᵥ

The operator

Everything below is relative to one set A, so the section works in a module DefOf A. The restriction class is membership in A, and the essential smallness witness e is the library's presentation: the small member type ⟪ A ⟫ is the restricted carrier, up to equivalence (with the small membership converted pointwise to the large one). The constant interpretation ι sends a constant, an index in ⟪ A ⟫, to the corresponding member of the restricted carrier; its first component is the member itself, definitionally.

The class M assigns to each set x the proposition x ∈ˢ A, so the restricted carrier Σ[ x ∈ S ] (x ∈ᶜ M) is, elementwise, a member of A together with the proof that it is one. The equivalence e exhibits this carrier as essentially small. Its first factor is the inverse of presentation A, which identifies a member of A merely lying in the fiber of the indexing map with an index in ⟪ A ⟫; its second factor converts, for each v, the small membership statement v ∈ₛ A into the large one v ∈ˢ A and back. These are propositions, so the pointwise conversion is legitimate.

module DefOf (A : S) where

  M : S → hProp (ℓ-suc ℓ)
  M x = x ∈ˢ A

  e : ⟪ A ⟫ ≃ (Σ[ x ∈ S ] (x ∈ᶜ M))
  e = compEquiv (invEquiv (presentation A))

The constant interpretation ι is then just the equivalence e read as a function. Because the domain type of formulas will be ⟪ A ⟫ itself, a constant of the language is an index for a member of A, and ι decodes it into the restricted carrier. The first projection of ι m is definitionally the underlying set ⟪ A ⟫↪ m, a fact the membership proofs will use without ceremony.

        (Σ-cong-equiv-snd (λ v →
          propBiimpl→Equiv (snd (v ∈ₛ A)) (snd (v ∈ˢ A))
            (∈∈ₛ {a = v} {b = A} .snd) (∈∈ₛ {a = v} {b = A} .fst)))

  ι : ⟪ A ⟫ → Σ[ x ∈ S ] (x ∈ᶜ M)
  ι = equivFun e

Opening InnerSmall at this data rebuilds the world: the structure 𝒮M restricted to membership in A, its satisfaction relation ⊨ᵐ, and the theorem ⊨ᵐ-small that every formula over ⟪ A ⟫ evaluates to a small proposition. Making the opening public means later chapters read inner satisfaction under exactly these names. From here on, "satisfies" always means this inner relation, with quantifiers confined to members of A.

  open InnerSmall M ⟪ A ⟫ e {K = ⟪ A ⟫} ι public

With the inner satisfaction ⊨ᵐ and its smallness in scope, the operator can be defined directly. smallSat φ m is the truth value of φ at the member m, living one universe down; defSet φ is the subset φ defines out of A, a sett over the members φ selects; and Def A is the collection of all of them, indexed by the formulas themselves. A formula is a piece of inductive data in Type ℓ, hence a legitimate small index: this is precisely syntax as index set.

The compression smallSat packages the two-step evaluation: ⊨ᵐ-small φ (ι m ∷ []) is a pair whose first component is a small proposition equivalent to the inner satisfaction statement, and whose second component is that equivalence. The environment ι m ∷ [] has a single entry because φ has one free-variable slot, filled by the member m through ι. Independently of this, any constants occurring in φ are interpreted through the constant interpretation ι, so they may name arbitrary members of A: parameters enter through constants, and the variable entry only fixes where the single free slot is evaluated. The underlying proposition ⟨ smallSat φ m ⟩ says that φ holds at m inside (A, ∈), in the small form suitable for indexing a sett.

  smallSat : Formula ⟪ A ⟫  → ⟪ A ⟫ → hProp ℓ
  smallSat φ m = ⊨ᵐ-small φ (ι m ∷ []) .fst

  defSet : Formula ⟪ A ⟫  → S
  defSet φ = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))

  Def : S

The definable subset defSet φ is presented by the index type Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩: an index is a member m together with a proof that φ holds at it, and the indexing map sends such a pair to the set ⟪ A ⟫↪ m. Note the truncation discipline: the proof component is a proof, not chosen data, and membership in defSet φ only asks for a proof to merely exist. Finally Def applies the same construction one level up, with the formulas themselves as the index family: each formula merely hits some defSet φ. Because formulas live in Type ℓ, the index type is small and the result is again a set of the hierarchy.

  Def = sett (Formula ⟪ A ⟫ ) defSet

Membership, specified

Both Def and each defSet φ are setts, so their membership is definitionally "merely hit by the index family". For Def this needs no proof at all: a member of Def is merely a defSet φ. For the definable subsets there are two specifications: their members stay inside A, and a member ⟪ A ⟫↪ m belongs to defSet φ exactly when the inner world satisfies φ at m; this is literally what "definable subset" means (the compression smallSat was only an encoding, and the equivalence preserves it).

The first specification says each defSet φ is contained in A. A member of defSet φ merely comes from an index (m , _) with some proof, together with a path q identifying the indexed set with y. Since membership in A is a proposition, truncation can be eliminated into it: the proof transports the known fact ⟪ A ⟫↪ m ∈ˢ A along q to obtain y ∈ˢ A. The known fact itself is exactly the small membership ⟪ A ⟫↪ m ∈ₛ A, converted through ∈∈ₛ.

  defSet⊆A : (φ : Formula ⟪ A ⟫ ) (y : S) → ⟨ y ∈ˢ defSet φ ⟩ → ⟨ y ∈ˢ A ⟩
  defSet⊆A φ y = PT.rec (snd (y ∈ˢ A)) λ { ((m , _) , q) →
    subst (λ v → ⟨ v ∈ˢ A ⟩) q
          (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) }

  private

The second specification is the heart of the chapter, and it is stated as a path of propositions, not a pair of implications: membership of ⟪ A ⟫↪ m in defSet φ equals the inner satisfaction statement (ι m ∷ []) ⊨ᵐ φ. The auxiliary decode re-expands smallSat into the full pair, so the equivalence in its second component is available to both directions. Note also the private injectivity lemma: ⟪ A ⟫↪ is an embedding of ⟪ A ⟫ into the carrier, so paths between its values come from paths between indices; this will recover m' ≡ m from a path of sets.

    ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
    ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

  defSet-mem : (φ : Formula ⟪ A ⟫ ) (m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet φ) ≡ ((ι m ∷ []) ⊨ᵐ φ)
  defSet-mem φ m = ⇔toPath fwd bwd

The forward direction unpacks what membership merely gives: an index (m' , h), where h proves smallSat φ m', and a path q with ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m. Injectivity turns q into m' ≡ m, and transporting h along it yields a proof of smallSat φ m. The second component of decode, the equivalence between the small proposition and inner satisfaction, then converts this proof into the target statement. Every ingredient is used: truncation gives the index, embedding gives the path between indices, transport moves the proof, equivalence decodes it.

    where
    decode = ⊨ᵐ-small φ (ι m ∷ [])
    fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩ → ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩
    fwd = PT.rec (snd ((ι m ∷ []) ⊨ᵐ φ)) λ { ((m' , h) , q) →
      invEq (decode .snd) (subst (λ k → ⟨ smallSat φ k ⟩) (⟪⟫↪-inj q) h) }

The reverse direction is short because the equivalence also runs that way: given hφ : (ι m ∷ []) ⊨ᵐ φ, apply the equivalence to get a proof of smallSat φ m, and take the index (m , proof) with the trivial path refl. The result is truncated with ∣_∣₁, which is all that membership demands. Together the two directions give the promised exact correspondence between inner satisfaction and membership in the definable subset.

    bwd : ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩
    bwd hφ = ∣ (m , equivFun (decode .snd) hφ) , refl ∣₁

Def refines, never shrinks

Two facts locate Def A before any transitivity assumption is made. The always-true formula defines all of A, so A itself is an element of Def A; and every element of Def A is a subset of A. This does not yet assert A ⊆ Def A. That stronger inclusion is proved in the next section from transitivity, by defining each member of A separately.

The private helper A-mem converts a large membership proof into its fiber form: a member y of A merely comes from some index m with ⟪ A ⟫↪ m ≡ y, and since ∈-asFiber returns the fiber as data (the truncation lives inside the membership proof it consumes), the pair can be taken apart with let. Equality of the two sets is then proved by extensionality, so it suffices to establish inclusion in both directions.

  private
    A-mem : (y : S) → ⟨ y ∈ˢ A ⟩ → Σ[ m ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ m ≡ y)
    A-mem y y∈ = ∈-asFiber {a = y} {b = A} y∈

  defSet⊤≡A : defSet ⊤̇ ≡ A
  defSet⊤≡A = extensionality (defSet ⊤̇) A (sub₁ , sub₂)

The easy direction reuses the containment just proved. A set-theoretic member y of defSet ⊤̇ gives, via the definition of sett membership, a truncated index; defSet⊆A then places y inside A, and the conversion ∈∈ₛ repackages the statement in the form the inclusion ⊆ expects. Nothing here uses what ⊤̇ means: this half holds for every defSet φ.

    where
    sub₁ : ⟨ defSet ⊤̇ ⊆ A ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = A} .fst
      (defSet⊆A ⊤̇ y (∈∈ₛ {a = y} {b = defSet ⊤̇} .snd y∈ₛ))
    sub₂ : ⟨ A ⊆ defSet ⊤̇ ⟩

The converse uses what "true" means: since ⊤̇ holds at every member, defSet-mem ⊤̇ m identifies ⟪ A ⟫↪ m ∈ˢ defSet ⊤̇ with a proposition that any inhabitant proves, here supplied as the identity function. So each member y of A, being merely ⟪ A ⟫↪ m, is transported along the fiber path into defSet ⊤̇. Note the use of sym (defSet-mem ⊤̇ m) inside subst ⟨_⟩: the theorem is a path of propositions, so it transports proofs in whichever direction the goal needs.

    sub₂ y y∈ₛ =
      let (m , q) = A-mem y (∈∈ₛ {a = y} {b = A} .snd y∈ₛ)
      in subst (λ v → ⟨ v ∈ₛ defSet ⊤̇ ⟩) q
           (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet ⊤̇} .fst
             (subst ⟨_⟩ (sym (defSet-mem ⊤̇ m)) (λ z → z)))

The dual containment Def∋⊆A says every element of Def A is a subset of A. Its hypothesis is itself a truncation: x merely is some defSet φ. The target is a proposition, being built from propositions by products, so PT.rec may eliminate the truncation; the case then transports y ∈ˢ x backwards along the path identifying x with defSet φ and applies the containment of defSet φ. Combined with defSet⊤≡A, which yields A ∈ Def, the picture is complete: Def contains A as an element and contains only subsets of A.

  Def∋⊆A : (x : S) → ⟨ x ∈ˢ Def ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩
  Def∋⊆A x = PT.rec (isPropΠ λ y → isPropΠ λ _ → snd (y ∈ˢ A))
    (λ { (φ , q) y y∈x → defSet⊆A φ y (subst (λ s → ⟨ y ∈ˢ s ⟩) (sym q) y∈x) })

Under transitivity, A ⊆ Def A

When A is transitive, each member a of A is itself definable, by the same two-symbol construction that built intersection in the model chapter: the atomic formula "the variable is a member of a". Separation's implicit "∈ A" clause is what transitivity discharges: members of a are already members of A, so the atom carves out exactly a. Hence A ⊆ Def A: no element is omitted. Combined with the previous section, iterating Def can only accumulate, which is exactly what the constructible tower requires.

The submodule takes transitivity of A as an explicit hypothesis. The atomic formula atom mₐ is var zero ∈̇ con mₐ: one free-variable slot, and a single constant naming the element mₐ. This is where the design choice of using ⟪ A ⟫ as the constant domain pays off again: every member of A is available as a constant, with ι decoding it into the restricted carrier.

  module Refine (Atrans : Transitive 𝒮ᵥ M) where

    atom : ⟪ A ⟫ → Formula ⟪ A ⟫ 
    atom mₐ = var zero ∈̇ con mₐ

    atom-mem : (mₐ m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet (atom mₐ)) ≡ (⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ)

The specialization of the membership theorem to this atom is immediate, because the environment is fixed to the single parameter m and the inner truth of var zero ∈̇ con mₐ is, by the semantics of atoms, precisely membership ⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ inside the restricted world. Since restricted membership is defined by the ambient membership of the underlying sets, the atom really selects the elements of ⟪ A ⟫↪ mₐ; the remaining work is only to show the presented set defSet (atom mₐ) equals that element.

    atom-mem mₐ m = defSet-mem (atom mₐ) m

    defSet-atom≡ : (mₐ : ⟪ A ⟫) → defSet (atom mₐ) ≡ ⟪ A ⟫↪ mₐ
    defSet-atom≡ mₐ = extensionality (defSet (atom mₐ)) (⟪ A ⟫↪ mₐ) (sub₁ , sub₂)
      where
      sub₁ : ⟨ defSet (atom mₐ) ⊆ ⟪ A ⟫↪ mₐ ⟩

The forward inclusion eliminates the truncated index of y ∈ˢ defSet (atom mₐ): an index is a pair (m , h) of a member and a proof that the atom holds at it, plus the path q from the indexing map. By atom-mem, the proof h becomes membership ⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ in the ambient sense, and ∈∈ₛ converts it to a set-theoretic member of ⟪ A ⟫↪ mₐ; transporting along q finishes. This mirrors the proof of defSet⊆A with the atom's meaning in place of the trivial containment in A.

      sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ⟪ A ⟫↪ mₐ))
        (λ { ((m , h) , q) →
          subst (λ v → ⟨ v ∈ₛ ⟪ A ⟫↪ mₐ ⟩) q
            (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = ⟪ A ⟫↪ mₐ} .fst
              (subst ⟨_⟩ (atom-mem mₐ m) ∣ (m , h) , refl ∣₁)) })

The reverse inclusion is where transitivity enters. Given y ∈ˢ ⟪ A ⟫↪ mₐ, unfold it to the ambient membership y∈a; transitivity of A states that a member of a member of A is again a member of A, applied here with the witness mₐ-as that ⟪ A ⟫↪ mₐ ∈ˢ A. So y ∈ˢ A, and the fiber decomposition hands over an index m with ⟪ A ⟫↪ m ≡ y, ready to be presented as an inhabitant of defSet (atom mₐ).

        (∈∈ₛ {a = y} {b = defSet (atom mₐ)} .snd y∈ₛ)
      sub₂ : ⟨ ⟪ A ⟫↪ mₐ ⊆ defSet (atom mₐ) ⟩
      sub₂ y y∈ₛ =
        let y∈a     = ∈∈ₛ {a = y} {b = ⟪ A ⟫↪ mₐ} .snd y∈ₛ
            y∈A     = Atrans {x = ⟪ A ⟫↪ mₐ} {y = y} y∈a mₐ-as

To conclude, the index m just obtained must actually satisfy the atom at itself. Transporting y∈a backwards along the fiber path puts membership inside ⟪ A ⟫↪ mₐ, and atom-mem, read in the reverse direction via sym, converts that into a proof of smallSat (atom mₐ) m. The final transport along q lands in defSet (atom mₐ). Both inclusions together give the equality of sets. Note how every transport here moves a proof along a path of sets or of propositions, never building new data.

            (m , q) = ∈-asFiber {a = y} {b = A} y∈A
        in subst (λ v → ⟨ v ∈ₛ defSet (atom mₐ) ⟩) q
             (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet (atom mₐ)} .fst
               (subst ⟨_⟩ (sym (atom-mem mₐ m))
                 (subst (λ v → ⟨ v ∈ˢ ⟪ A ⟫↪ mₐ ⟩) (sym q) y∈a)))

With the equality in hand, membership in Def is one truncation away. Given a ∈ˢ A, the fiber decomposition of that membership provides an index mₐ with ⟪ A ⟫↪ mₐ ≡ a; since the fiber is data here, the pair can be opened with let and mₐ named.

        where
        mₐ-as : ⟨ ⟪ A ⟫↪ mₐ ∈ˢ A ⟩
        mₐ-as = ∈∈ₛ {a = ⟪ A ⟫↪ mₐ} {b = A} .snd (∈ₛ⟪ A ⟫↪ mₐ)

    A⊆Def : (a : S) → ⟨ a ∈ˢ A ⟩ → ⟨ a ∈ˢ Def ⟩
    A⊆Def a a∈ =

The element defSet (atom mₐ) of Def equals ⟪ A ⟫↪ mₐ, and composing that equality with the fiber path q gives defSet (atom mₐ) ≡ a. Wrapping the pair of a formula and this equality in the truncation ∣_∣₁ produces exactly what membership in Def demands: a formula whose defined subset is a, merely. Thus every element of A survives into Def, and with the previous section the operator only refines.

      let (mₐ , q) = ∈-asFiber {a = a} {b = A} a∈
      in ∣ atom mₐ , defSet-atom≡ mₐ ∙ q ∣₁

Definability read from outside

One consequence deserves its own name, because the constructible-stage proofs lean on it repeatedly. Membership in defSet φ is a statement of the inner world (A, ∈), and the arguments to come are conducted in the ambient hierarchy. For a Δ₀ formula the two readings agree, which is the absoluteness theorem; what remains is bookkeeping, since absoluteness is stated over the members of the class while defSet is stated over the small index type. Relabelling closes that gap, and the whole proof is a three-step path: the specification of defSet, then the relabelling of the formula, then absoluteness.

A must be transitive for this, which is why the lemma lives in this submodule; every stage of the tower is.

The absoluteness module is instantiated at the ambient structure, the class M, and the transitivity hypothesis, yielding the restricted structure Abs.𝒮M, the outer satisfaction Abs.⊨ᵛ, and the Δ₀ absoluteness Abs.abs₀. The statement takes a witness d certifying that φ is Δ₀, and asserts a path of propositions: membership of ⟪ A ⟫↪ m in defSet φ equals the satisfaction of mapFo ι φ in the ambient structure at the environment ⟪ A ⟫↪ m ∷ []. The formula on the right has its constants mapped through ι, so it is a formula over the ambient carrier naming members of A.

    module Abs = FOL.Absoluteness.Single 𝒮ᵥ M Atrans

    abs-defSet : (φ : Formula ⟪ A ⟫ ) → Δ₀ φ → (m : ⟪ A ⟫)
               → (⟪ A ⟫↪ m ∈ˢ defSet φ)
                 ≡ ((⟪ A ⟫↪ m ∷ []) Abs.⊨ᵛ (mapFo ι φ))
    abs-defSet φ d m =

The proof concatenates three paths. First, defSet-mem reads membership in the definable subset as inner satisfaction of φ at ι m. Second, ⊨-map (in the symmetric direction, hence sym) says that relabelling the constants through ι does not change the truth value, because ι is precisely the constant interpretation of the inner world; what remains is inner satisfaction of the relabelled formula mapFo ι φ. Third, abs₀ transports inner satisfaction of that Δ₀ formula to outer satisfaction in the ambient structure, this being the only step that uses transitivity. The result lets later chapters treat membership in a definable subset as an ambient, not merely inner, statement.

        defSet-mem φ m
      ∙ sym (⊨-map Abs.𝒮M ι id φ (ι m ∷ []))
      ∙ Abs.abs₀ (mapΔ₀ ι d) (ι m ∷ [])

Recap

Def A is the set of subsets of A definable in the inner world (A, ∈) with parameters from A: syntax as index set, inner satisfaction for meaning, and essential smallness supplying the required universe level. The specification defSet-mem states directly what "definable" means, and the operator only refines: A ⊆ Def A under transitivity (A⊆Def), and members of Def A are subsets of A (Def∋⊆A). The next chapter iterates this step into a universe.