---
title: "有界部分集合が制御された段階に現れる"
module: L.GCH.BoundedSubset
lang: ja
site: "Bedrock"
description: "有界部分集合が現れる段階を制御する"
stage: "GCH の証明"
reading_order: 119
canonical: https://bedrock.institute/ja/L.GCH.BoundedSubset.html
html: L.GCH.BoundedSubset.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/BoundedSubset.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Numerals, L.Stage, L.Cardinal, L.GCH.Assembly, L.InjectionComposition, L.GCH.SkolemHull, L.GCH.CardinalSquareLaw, L.GCH.AdequateStages, L.GCH.StageCountingTools, L.GCH.StageInjection, L.GCH.OmegaRecursion, L.GCH.HullCounting]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.BoundedSubset.md, https://bedrock.institute/zh/L.GCH.BoundedSubset.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 有界部分集合が制御された段階に現れる

有界部分集合定理では、台となる集合が順序数であり `ω` に属さない内部基数 `κ` と、周囲の各要素が `κ` に属する任意の構成可能集合 `y` を考えます。命題的切り詰めのもとで、`y ∈ Lset β` を満たし、符号化された単射 `β ↪ κ` が存在するような構成可能順序数 `β` が得られます。`y` を定義する論理式は仮定せず、最小の段階も選ばず、`y` ごとに `β` を一様に選ぶこともありません。

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

この証明で用いる古典性は、ここで明示された排中律の実例だけです。この仮定は、本章で利用する段階、包、符号化された写像の先行する構成を支えますが、最後の切り詰められた存在を、選択された証人の族へ変えるものではありません。

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

宇宙レベル `ℓ` と、レベル `ℓ-suc ℓ` における排中律を固定します。以下のすべての構成は、最後の有界部分集合定理も含め、この一つの古典的仮定だけに依存し、選択原理には依存しません。

```agda
module L.GCH.BoundedSubset {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

議論を通して、二つの種類の対象を区別しなければなりません。`κ`、`α₀`、`lam`、そして後の `β` は周囲の累積階層の集合を表し、そのうちいくつかは順序数であることが示されます。一方、`Lset κ`、`Lset α₀`、`Lset lam`、`Lset β` は、それぞれに対応する構成可能段階です。段階の添字に属することと、その添字が定める段階に属することは別の主張です。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( #∈ω )
```

最初の課題は、`κ` と `y` を一つの十分高い構成可能段階へ入れることです。`y` はすでに構成可能な集合として与えられているので、それが現れる段階を直接得られます。`y` を定義する論理式も、有限個の定義パラメータの列も、この構成には入りません。

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Numerals {ℓ} using ( pairʟ )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )
```

中心となる方針は、`Lset κ` に一点 `y` を加え、この推移的な出発集合から初等 Skolem 包を生成し、凝縮を適用することです。出発集合を `κ` で数えれば、包全体も `κ` で数えられます。その後、凝縮によって崩壊した包がある段階 `Lset β` と同一視されます。

```agda
open import L.GCH.Assembly {ℓ} lem using ( InternalBoundedSubset )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.GCH.SkolemHull {ℓ} lem
  using ( module UnionKit; module HullStage; module HullElemDown )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; ω⊆; Goal; module Step )
```

この方針には、二種類の制御が必要です。十分な閉性をもつ順序数 `lam` は、包と凝縮の議論を行う周囲の段階を与えます。符号化された単射は大きさを制御し、まず `X ↪ κ`、次に `M ↪ κ`、最後に `β ↪ κ` を与えます。

```agda
open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate )
open import L.GCH.StageCountingTools {ℓ} lem using ( move )
open import L.GCH.StageInjection {ℓ} lem using ( stage-counted; module Site )
open import L.GCH.OmegaRecursion {ℓ} lem using ( pairʟ-in )
open import L.GCH.HullCounting {ℓ} lem
```

大きさの評価は、二つの基本的な部分から始まります。段階 `Lset κ` は `κ` へ符号化でき、単元集合も `κ` へ符号化できます。有限のタグが二つの像を区別し、無限の内部基数 `κ` に対する平方法則が、得られた積を再び `κ` へ収めます。

```agda
  using ( ord⊆Lset; module Union2; tag-union; module Point; module Count )
```

以下では、いくつかの等しさを、所属を両方向に比較して証明します。合併への所属から得られる場合分けは命題的に切り詰められていますが、行き先となる所属の主張はいずれも命題です。したがって、どちらかの分岐を選んで保持することなく、その場合分けを局所的に利用できます。

```agda
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
```

有限 von Neumann 数項は合併の符号化に使うタグを与え、順序数の後続に関する閉性は包に必要な環境の一部をなします。整礎性は平方法則を支えます。命題的切り詰めは、特定のグラフを公開せずに、符号化された単射の存在を記録します。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet; ⁅_⁆s )
open InfinitySet {ℓ} using ( #_; ω; sucV )
import Cubical.Induction.WellFounded as WF
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

`InjL` によって単射を主張する場合、そのグラフが存在するのは命題的切り詰めの内側だけです。証明は命題の内部でそのような存在を合成できますが、切り詰めの外で計算データとして使える特定の単射を得ることはありません。

```agda
open PT using ( ∣_∣₁ )
```

部分集合の仮定は、意図的に周囲の所属を用いて述べられます。したがって、任意の周囲の集合 `z` について、`y` への所属から `κ` への所属を導けます。`z` 自身の構成可能性の証明が、初めから添えられている必要はありません。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

これに対して、`κ` と `y` は構成可能な台 `S` の要素であり、周囲の集合と、それが `L` に属する証拠とを組にしています。最後の証人も同じ形でまとめられるので、定理が与えるのは任意の周囲の順序数ではなく、構成可能な順序数です。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

## 基数の構成可能な部分集合を有界化する

台となる集合が順序数であり、内部の基数であり、`ω` の要素ではない構成可能集合 `κ` を固定します。さらに任意の構成可能集合 `y` を固定し、`y` の周囲の各要素が `κ` に属すると点ごとに仮定します。仮定はこれですべてです。とくに、`y` が論理式や有限個のパラメータで定義されるとは仮定しません。

```agda
module At (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ)
          (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
          (y : S) (y⊆κ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩) where
```

`κ` が順序数であることと `κ ∉ ω` から、`ω ⊆ κ` が従います。有限 von Neumann 数項 `# k` はどれも `ω` に属するので、すべての `k` について `# k ∈ κ` です。これらの要素を、合併の符号化における有限のタグとして使います。

```agda
  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)
```

順序数 `κ` と、それを添字とする構成可能段階は別の集合です。そこで `Lset κ` を内部集合 `Lκ` としてまとめます。この段階が出発集合の主要部分となり、`κ` 自身は、その出発集合を符号化して入れる基数として残ります。

```agda
  Lκ : S
  Lκ = LsetS (fst κ) oκ
```

`κ` と `y` を一つの共通の段階へ入れるため、まず `L` の内部で両者の無順序対を作ります。この対を含む推移的な段階は、その二つの要素も含むので、一度の出現段階の構成で両方を扱えます。

```agda
  private
    P₀ : S
    P₀ = pairʟ κ y
```

この無順序対が現れる、順序数である段階の添字 `α₀` を取ります。これは構成可能性から得られる扱いやすい添字にすぎず、`α₀` がこの対の現れる最小の段階だとは主張していません。

```agda
    α₀ : V ℓ
    α₀ = stage (fst P₀) (snd P₀)
```

選んだ段階の添字 `α₀` は順序数です。次にこれより真に上にある、十分性を強めた順序数を取るため、また後で順序数の推移性によって `κ` を `α₀` の下から `lam` へ運ぶために、この事実が必要です。

```agda
    oα₀ : IsOrd α₀
    oα₀ = stage-ord (fst P₀) (snd P₀)
```

基数 `κ` は `Lset α₀` に属します。`κ` は無順序対の要素であり、その対は `Lset α₀` に属し、この段階は推移的だからです。ここで得たのは段階への所属であって、後で使う順序数への所属 `κ ∈ α₀` ではありません。

```agda
    κ∈Lα₀ : ⟨ fst κ ∈ˢ Lset α₀ ⟩
    κ∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst κ}
      (pairʟ-in κ y κ (inl refl)) (stage-mem (fst P₀) (snd P₀))
```

同じ推移性の議論により、無順序対のもう一つの要素を通して `y` も `Lset α₀` に入ります。`κ` と違い、`y` は順序数とは仮定されていません。したがって後では、この事実を段階の単調性によって `Lset lam` へ運び、`y ∈ α₀` へ変換することはしません。

```agda
    y∈Lα₀ : ⟨ fst y ∈ˢ Lset α₀ ⟩
    y∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst y}
      (pairʟ-in κ y y (inr refl)) (stage-mem (fst P₀) (snd P₀))
```

ここで `α₀ ∈ lam` を満たす、十分性を強めた順序数 `lam` を明示的に取ります。この真の拡張が、後の包と凝縮の議論に必要な閉性を与えます。`lam` 自身は明示的なデータですが、その強められた十分性が保証する局所的な十分な添字は、命題的切り詰めの内側にとどまります。

```agda
    sa = superadequate-above α₀ oα₀
```

この高い順序数を、コードでは `lam`、本文では `λ` と書きます。その具体的な構成は以後使わず、順序数性、後続に関する閉性、強められた十分性、および `α₀` より上にあるという事実だけを使います。

```agda
  opaque
    lam : V ℓ
    lam = sa .fst
```

最初に保つ事実は、`lam` が順序数であることです。したがって `lam` は推移的であり、`lam` より下の順序数の所属をさらに上へ運べます。

```agda
    ordλ : IsOrd lam
    ordλ = sa .snd .fst
```

次に保つのは、順序数の後続に関する閉性です。`d ∈ lam` ならば `sucV d ∈ lam` でもあります。この閉性は、有限 Skolem 構成が `lam` を添字とする段階の内部にとどまるための構造的仮定の一つです。

```agda
    succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
    succλ = sa .snd .snd .snd .fst .snd .fst
```

強められた十分性とは、各 `d ∈ lam` に対して、`d ∈ γ ∈ lam` を満たす十分な順序数 `γ` が単に存在することです。これは `lam` より下に局所的な十分な余地を与えますが、最小の `γ` も、そのような `γ` の族も選びません。

```agda
    sup : Superadequate lam
    sup = sa .snd .snd .snd .snd
```

基数 `κ` は順序数の添字 `lam` に属します。`κ` と `α₀` はともに順序数なので、まず `κ ∈ Lset α₀` から `κ ∈ α₀` が得られます。さらに `α₀ ∈ lam` と順序数 `lam` の推移性から、`κ ∈ lam` が従います。この結論は添字 `lam` への所属であり、段階 `Lset lam` への所属ではありません。

```agda
    κ∈λ : ⟨ fst κ ∈ˢ lam ⟩
    κ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ (fst κ) oκ κ∈Lα₀) (sa .snd .snd .fst)
```

一方、`y` について必要なのは、段階 `Lset lam` への所属です。`α₀ ∈ lam` から、段階の単調性により `Lset α₀ ⊆ Lset lam` が得られます。これを先の `y ∈ Lset α₀` に適用すると、`y ∈ Lset lam` となります。`y` が順序数であるという仮定は必要ありません。

```agda
    y∈Lλ : ⟨ fst y ∈ˢ Lset lam ⟩
    y∈Lλ = Lset-mono {α = lam} {β = α₀} (sa .snd .snd .fst) y∈Lα₀
```

`y` の周囲の各要素は `Lset κ` に属します。部分集合の仮定により `z ∈ y` から `z ∈ κ` が得られます。`κ` は順序数なので、このような `z` も順序数であり、自身の後続段階に属し、累積性によって `z ∈ Lset κ` となります。したがって `y ⊆ κ` から、出発集合を推移的にするために必要な段階への包含が得られます。

```agda
  y⊆Lκ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ Lset (fst κ) ⟩
  y⊆Lκ z hz = ord⊆Lset (fst κ) oκ z (y⊆κ z hz)
```

`Lset lam` の内部で、出発集合 `X = Lset κ ∪ {y}` を作ります。これは `y` を含み、しかも推移的です。`Lset κ` に由来する要素は、その推移的な段階にとどまります。また `y` の要素は、仮定により `κ` に属し、したがって `Lset κ` に属します。この推移性こそが、後で崩壊に `y` を固定させます。

```agda
  module UK = UnionKit (fst κ) lam (fst y) oκ ordλ κ∈λ y⊆Lκ y∈Lλ κ∉ω
    using ( X; X⊆Lλ; ∅∈λ; Lα∈X; x∈X; X-mem; sgl≡; Xtr )
```

以下では、この `Lset κ` の推移的な拡張を `X` と書きます。覚えておくべき二つの性質は互いに補い合います。`y ∈ X` によって、位置を定めたい集合が包に入り、推移性によって、崩壊がその集合を変えません。

```agda
  X : V ℓ
  X = UK.X
```

数え上げのため、タグ `0 ∈ κ` を用いて、単元集合 `{y}` とその `κ` への符号化された単射を内部で構成し、それを `Lκ` と内部で合併します。こうして同じ集合 `Lset κ ∪ {y}` の符号化された提示が得られ、その二つの部分には、タグ付き合併の議論に必要な単射がすでに備わっています。

```agda
  module Pt = Point κ (num∈κ 0) y using ( Y; Y-out; Y-in; injL )
  module U = Union2 Lκ Pt.Y using ( D; out; in₁; in₂ )
```

この内部で構成した合併を `Xʟ` と書きます。これは `X` と同じ数学的な合併を表しますが、その構成には、`κ` への符号化された単射を示すために必要な内部データが伴っています。

```agda
  Xʟ : S
  Xʟ = U.D
```

`Xʟ` と `X` を同一視するため、両者の要素を二方向に比較します。順方向では、内部で符号化された合併への所属から、命題的切り詰めのもとで、`Lset κ` の要素である場合と、符号化された単元集合の要素である場合に分かれます。どちらからも `X` への所属が従います。`X` への所属は命題なので、この除去は正当です。

```agda
  Xʟ-eq : fst Xʟ ≡ X
  Xʟ-eq = extensionalV {a = fst Xʟ} {b = X} (λ z → ⇔toPath (fwd z) (bwd z))
    where
    fwd : (z : V ℓ) → ⟨ z ∈ˢ fst Xʟ ⟩ → ⟨ z ∈ˢ X ⟩
    fwd z h = PT.rec (snd (z ∈ˢ X)) go (U.out zS h)
```

段階の側の場合、左の包含によって、その要素は `X` に入ります。`z` を一時的に構成可能集合としてまとめられるのは、`L` の推移性によります。`z` は構成可能集合 `Xʟ` の要素なので、`z` 自身も構成可能です。

```agda
      where
      zS : S
      zS = z , isL-trans {x = fst Xʟ} {y = z} h (snd Xʟ)
      go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ fst Pt.Y ⟩ → ⟨ z ∈ˢ X ⟩
      go (inl hz) = UK.Lα∈X z hz
```

単元集合の側では、符号化された要素は、すでに `X` に属すると分かっている `y` に等しくなります。逆方向では、`X` への所属が、やはり命題的切り詰めのもとで `Lset κ` の側と単元集合の側に分かれます。行き先である `Xʟ` への所属は命題なので、この二度目の除去も正当です。

```agda
      go (inr hz) = subst (λ w → ⟨ w ∈ˢ X ⟩) (sym (Pt.Y-out zS hz)) UK.x∈X
    bwd : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩
    bwd z h = PT.rec (snd (z ∈ˢ fst Xʟ)) go (UK.X-mem z h)
      where
      go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ ⁅ fst y ⁆s ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩
```

逆方向の二つの場合は、`Xʟ` の二つの成分へそれぞれ入ります。`Lset κ` の要素は、その段階から構成可能性を受け継いで左側に入り、`{y}` の要素は、まず `y` と同一視されてから、符号化された単元集合の側に入ります。こうして外延性により `fst Xʟ ≡ X` が得られ、切り詰められた場合分けはどちらも保持されません。

```agda
      go (inl hz) = U.in₁ (z , isL-trans {x = Lset (fst κ)} {y = z} hz (snd Lκ)) hz
      go (inr hz) = subst (λ w → ⟨ w ∈ˢ fst Xʟ ⟩) (sym (UK.sgl≡ z hz)) (U.in₂ y Pt.Y-in)
```

始集合は構成可能です。内部の写しが構成可能で、二つの写しの底の集合が等しいからです。

```agda
  X-isL : ⟨ isL X ⟩
  X-isL = subst (λ w → ⟨ isL w ⟩) Xʟ-eq (snd Xʟ)
```

`X` とこの構成可能性の証明を組にして、`XS : S` とします。台となる周囲の集合は依然としてちょうど `X` であり、この包装は `InjL` が要求する内部の定義域を与えるだけです。

```agda
  XS : S
  XS = X , X-isL
```

無限基数の平方法則により、符号化された単射 `κ × κ ↪ κ` の存在が命題的切り詰めのもとで得られます。その仮定は冒頭で固定した事実、すなわち `κ` が順序数であり内部の基数であり、`ω` の要素ではないことに一致します。全単射も、特定の単射のグラフも得られません。

```agda
  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω
```

二つの成分の単射をタグ付き合併の構成に入れると、符号化された単射 `Xʟ ↪ κ × κ` が得られます。タグ `#0` と `#1` が、段階の側と単元集合の側を区別します。これを平方法則の単射と合成して `Xʟ ↪ κ` を得た後、`fst Xʟ ≡ X` に沿って定義域を構成可能な包装 `XS` へ移します。こうして必要な符号化された単射 `X ↪ κ` が、引き続き命題的切り詰めのもとで得られます。

```agda
  base : InjL XS κ
  base = move Xʟ XS κ κ Xʟ-eq refl
    (injl-trans Xʟ (prodL κ) κ
      (tag-union κ (num∈κ 0) (num∈κ 1) Lκ Pt.Y (stage-counted κ Lκ oκ κ∉ω refl) Pt.injL)
      pairκ)
```

`M` を、`Lset lam` の内部で `X` が生成する Skolem 包とします。この包に対する Tarski-Vaught の定理により、`M` は凝縮に必要な意味で初等的です。推移的集合 `X` 全体が出発集合なので、これは `y` を含み、後でその崩壊が `y` を固定する、同じ一つの包です。

```agda
  elem = HullElemDown.elem lam ordλ X UK.X⊆Lλ UK.∅∈λ
```

包の数え上げ定理は、`X ↪ κ` を Skolem 閉包の有限段階へ順に伝え、さらにそれらの合併へ伝えます。その結果、符号化された単射 `M ↪ κ` の存在が命題的切り詰めのもとで得られます。したがって、この包は凝縮を適用するのに必要な初等性をもち、その大きさも引き続き `κ` によって制御されます。

```agda
  hull↪κ = Count.hull↪κ lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL κ oκ cκ κ∉ω base
```

凝縮は明示的な順序数 `β` を与え、`M` の崩壊像を `Lset β` と同一視します。さらに `Lset β` と `M` を構成可能集合としてまとめ、逆崩壊から得られる符号化された単射 `Lset β ↪ M` の存在を命題的切り詰めのもとで与えます。ここで `β` は段階の添字であり、`Lset β` がそれによって添字づけられる段階です。

```agda
  module St = Site lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL
    using ( β; oβ; ext; Lβ; βL; hullL; Lβ↪M )
```

ここからは、一つの包の構成について三つの側面を使います。包 `M`、包含 `X ⊆ M`、そして像を `πX` とする崩壊写像 `π` です。対応する不動点定理は、`M` の推移的部分集合に適用できます。これらの事実から、まず崩壊が `y` を変えないことを示し、次に同じ `y` を凝縮によって同一視された段階へ入れます。

```agda
  module HS = HullStage lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ
    using ( πX; π; fixes; πX-intro )
```

集合 `y` は Skolem 包 `M` に属します。`y` は始点集合 `X` に入っており、`X` の各要素は `X` から生成された包に属するからです。

```agda
  y∈M : ⟨ fst y ∈ˢ HS.M ⟩
  y∈M = HSH.X⊆M (fst y) UK.x∈X
```

崩壊は `y` を固定します。始点の集合 `X` が推移的で包の中にあるため、崩壊の写像は `X` のすべての要素の上で恒等であり、`y` もその一つです。

```agda
  πy : HSC.π (fst y) ≡ fst y
  πy = HSC.fixes X
    (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
    UK.Xtr (fst y) UK.x∈X
```

`y` は包に属するので、崩壊像は `π(y)` を含みます。凝縮によってこの像は構成可能段階 `Lset β` と同一視され、不動点の等式 `π(y) = y` から `y ∈ Lset β` が従います。ここで崩壊は `y` を別の集合に置き換えたのではなく、もとの `y` を制御された構成可能段階の中に位置づけています。

```agda
  y∈Lβ : ⟨ fst y ∈ˢ Lset St.β ⟩
  y∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πy
    (subst (λ w → ⟨ HSC.π (fst y) ∈ˢ w ⟩) St.ext (HSC.πX-intro (fst y) y∈M))
```

順序数 `β` は、三つの符号化された単射の鎖によって `κ` へ単射します。順序数の所属による `β` から `Lset β` への包含、制限された逆崩壊による `Lset β` から包 `M` への単射、そして包の計数による `M` から `κ` への単射です。この鎖が与えるのは符号化された単射であり、裸の順序数の比較ではありません。

```agda
  β↪κ : InjL St.βL κ
  β↪κ = injl-trans St.βL St.Lβ κ
    (inclusion-coded St.βL St.Lβ (λ z hz → ord⊆Lset St.β St.oβ z hz))
    (injl-trans St.Lβ St.hullL κ St.Lβ↪M hull↪κ)
```

局所的な証人は、構成可能順序数 `β`、その順序数性、`y` が段階 `Lset β` に属するという事実、そして符号化された単射 `β ↪ κ` をまとめます。ここで返されるのは段階の添字 `β` であり、`Lset β` は `y` が位置づけられた構成可能段階です。この二つは区別されます。

```agda
  result : Σ[ b ∈ S ] (IsOrd (fst b) × ⟨ fst y ∈ˢ Lset (fst b) ⟩ × InjL b κ)
  result = St.βL , St.oβ , y∈Lβ , β↪κ
```

最後に、`∣_∣₁` は局所的な証人全体を命題的切り詰めのもとに置きます。したがって、最後の定理が保つのは、ある構成可能順序数 `β` が `y ∈ Lset β` を満たし、符号化された単射 `β ↪ κ` が存在するということだけです。最小または標準的な `β` も、`y` ごとの証人の一様な選択も与えません。

```agda
internal-bounded-subset : InternalBoundedSubset
internal-bounded-subset κ oκ cκ κ∉ω y y⊆κ =
  ∣ At.result κ oκ cκ κ∉ω y y⊆κ ∣₁
```