---
title: "Ordinals below a successor cardinal inject into its base"
module: L.GCH.BelowSuccessorCardinal
lang: en
site: "Bedrock"
description: "Ordinals below a successor cardinal inject into its base"
stage: "Proving GCH"
reading_order: 108
canonical: https://bedrock.institute/en/L.GCH.BelowSuccessorCardinal.html
html: L.GCH.BelowSuccessorCardinal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/BelowSuccessorCardinal.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.InjectionComposition]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.BelowSuccessorCardinal.md, https://bedrock.institute/ja/L.GCH.BelowSuccessorCardinal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Ordinals below a successor cardinal inject into its base

A successor cardinal is the first cardinal strictly beyond its base. Suppose `δ` is the successor cardinal of `κ` inside `L`. This chapter proves that every ordinal `α ∈ δ` admits an internal injection into `κ`. The proof combines well-founded induction with ordinal trichotomy. Excluded middle has two precise roles: it supplies the trichotomy of ordinals, and in the case `κ ∈ α` it turns the failure of cardinality into the mere existence of a smaller target.

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

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

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

Fix one universe level and an instance of excluded middle at the level of the propositions used by the hierarchy. The classical hypothesis is explicit and precisely leveled. It is used first through ordinal trichotomy and later through a direct decision of `Ex`; the remaining ingredients are structural facts about `V`, `L`, ordinals and internal injections.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
```

The argument moves between two structures. The ambient hierarchy supplies well-founded membership and its irreflexivity. The constructible universe supplies the ordinal and cardinal predicates. Ordinal trichotomy compares the current ordinal with `κ`, while inclusion coding and transitivity compose the resulting internal injections.

```agda
open import L.Cardinal {ℓ} lem using ( InjL; SuccCardL; IsCardinalL )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )

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

The exceptional branch produces only a truncated witness. Accordingly, the proof uses sums and the empty type to analyze a decision, propositional truncation to state mere existence, and well-founded induction to descend through membership. These logical forms match the conclusion `InjL`, which is itself propositionally truncated.

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
import Cubical.Induction.WellFounded as WF

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

Write `SV.S` for the carrier of the ambient hierarchy. Membership induction takes place on this type: an element is a set of `V`, without yet carrying evidence that it belongs to `L`.

```agda
module SV = hPropStructure 𝒮ᵥ using ( S )
```

Write `SL.S` for the carrier of the constructible universe. Its elements are pairs consisting of an ambient set and a certificate of constructibility. The predicates `SuccCardL`, `IsCardinalL` and `InjL` concern elements of this carrier.

```agda
module SL = hPropStructure 𝒮ʟ using ( S )
```

Assume that `δ` is the successor cardinal of `κ`, and let `α` be an ordinal belonging to `δ`. The goal `InjL α κ` says merely that an internal injection from `α` to `κ` exists. This is the precise form of the familiar statement that every ordinal below the successor of `κ` has cardinality at most `κ`.

```agda
below-succ-injects :
    (κ δ : SL.S) → SuccCardL δ κ
  → (α : SL.S) → IsOrd (fst α) → ⟨ fst α ∈ˢ fst δ ⟩
  → InjL α κ
```

Well-founded induction is performed on the underlying set of `α`. The predicate `P a` restores exactly the data needed to regard an ambient set `a` as the ordinal under consideration: a constructibility certificate, ordinalhood, and membership in `δ`. Under those assumptions it asks for an internal injection from `(a , la)` to `κ`.

```agda
below-succ-injects κ δ (ordδ , _ , κ∈δ , least) α =
  WF.WFI.induction regularityV {P = P} step (fst α) (snd α)
  where
  P : SV.S → Type (ℓ-suc ℓ)
  P a = (la : ⟨ isL a ⟩) → IsOrd a → ⟨ a ∈ˢ fst δ ⟩ → InjL (a , la) κ
```

Because `κ ∈ δ` and `δ` is an ordinal, `κ` is itself an ordinal. The induction step may therefore apply ordinal trichotomy to `a` and the underlying set of `κ`. Its induction hypothesis is available at every member of `a`, which is exactly what the third trichotomy branch will require.

```agda
  ordκ : IsOrd (fst κ)
  ordκ = mem-ord {A = fst δ} ordδ (fst κ) κ∈δ

  step : (a : SV.S) → (∀ a' → ⟨ a' ∈ˢ a ⟩ → P a') → P a
  step a ih la orda a∈δ = go (ord-tri a orda (fst κ) ordκ)
    where
```

Pair the ambient set `a` with its certificate `la` to obtain the corresponding element `α'` of `L`. This keeps the well-founded induction on the simple carrier `SV.S`, while cardinality statements are made in their proper domain `SL.S`.

```agda
    α' : SL.S
    α' = a , la
```

Consider the branch `κ ∈ a`. If `α'` were an `L`-cardinal, the leastness clause of `SuccCardL δ κ` would place `δ` inside `α'`. Since `a ∈ δ`, this would give `a ∈ a`, contradicting the irreflexivity of membership. Thus `α'` cannot be a cardinal in this branch.

The type `Ex` states the relevant negation of cardinality positively: merely, there is some `γ ∈ α'` into which `α'` internally injects.

```agda
    not-card : ⟨ fst κ ∈ˢ a ⟩ → IsCardinalL α' → Empty.⊥
    not-card κ∈a c = ∈-irrefl a (least α' orda c κ∈a α' a∈δ)

    Ex : Type (ℓ-suc ℓ)
    Ex = ∥ Σ[ γ ∈ SL.S ] (⟨ fst γ ∈ˢ a ⟩ × InjL α' γ) ∥₁
```

Apply excluded middle to the proposition `Ex`. If it holds, the required mere witness is already present. If it is refuted, then every proposed member `γ` and injection from `α'` to `γ` yields a contradiction; this is precisely the condition saying that the ordinal `α'` is a cardinal.

```agda
    some-γ : ⟨ fst κ ∈ˢ a ⟩ → Ex
    some-γ κ∈a = decide (lem (Ex , squash₁))
      where
      decide : Ex ⊎ (Ex → Empty.⊥) → Ex
```

The refutation branch is impossible by `not-card`, so both outcomes produce `Ex`. At this step excluded middle provides the case distinction; it does not remove the truncation or choose a particular `γ`.

```agda
      decide (inl e)  = e
      decide (inr ¬e) =
        Empty.rec (not-card κ∈a (λ γ γ∈a inj → ¬e ∣ γ , γ∈a , inj ∣₁))
```

A witness of the untruncated content of `Ex` consists of `γ ∈ a` and an internal injection from `α'` to `γ`. Since members of an ordinal are ordinals and `δ` is transitive, `γ` again satisfies the induction predicate. The induction hypothesis supplies an injection from `γ` to `κ`, and transitivity of internal injection composes the two.

```agda
    from-γ : Σ[ γ ∈ SL.S ] (⟨ fst γ ∈ˢ a ⟩ × InjL α' γ) → InjL α' κ
    from-γ (γ , γ∈a , α↪γ) =
      injl-trans α' γ κ α↪γ
```

To invoke the induction hypothesis at `γ`, the proof supplies all three components of `P`: constructibility is the second component of `γ`; ordinalhood follows from `γ ∈ a` and the ordinalhood of `a`; membership in `δ` follows from `γ ∈ a ∈ δ` and the transitivity of the ordinal `δ`.

```agda
        (ih (fst γ) γ∈a (snd γ)
            (mem-ord {A = a} orda (fst γ) γ∈a)
            (ordδ .fst γ∈a a∈δ))
```

The first trichotomy branch has `a ∈ κ`. Because an ordinal is transitive, every member of `a` is then a member of `κ`; this inclusion is coded as an internal injection from `α'` to `κ`.

```agda
    go : Tri a (fst κ) → InjL α' κ
    go (inl a∈κ)       =
      inclusion-coded α' κ (λ z z∈a → ordκ .fst z∈a a∈κ)
```

In the equality branch, transport along `a ≡ fst κ` turns the same inclusion into the required injection. In the remaining branch `κ ∈ a`, the truncated witness supplied above is eliminated into `InjL α' κ`; this elimination is valid because `InjL` is itself a proposition.

```agda
    go (inr (inl e))   =
      inclusion-coded α' κ (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) e z∈a)
    go (inr (inr κ∈a)) = PT.rec squash₁ from-γ (some-γ κ∈a)
```

The three branches exhaust ordinal trichotomy. Hence every ordinal below the successor cardinal `δ` internally injects into its base `κ`. Well-founded membership permits the descent to `γ`. Excluded middle is used in two places: `ord-tri` obtains the trichotomy, and the branch above `κ` obtains the truncated smaller target.