---
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, FOL.Syntax, FOL.Semantics, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.DefinableInjection, 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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# Ordinals below a successor cardinal inject into its base

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

Fix a universe level `ℓ` and assume `lem : LEM (ℓ-suc ℓ)`. This hypothesis supplies a decision for each proposition at that level; it remains an explicit parameter of the constructions below.

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∃̇_ )
import FOL.Semantics
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 )
open import L.Cardinal {ℓ} lem using ( InjL; SuccCardL; IsCardinalL )
open import L.DefinableInjection {ℓ} lem using ( injLAt; module InjLAt )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

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.

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 to decide the formula presenting `Ex`; the remaining ingredients are structural facts about `V`, `L`, ordinals and internal injections.

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.

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.Induction.WellFounded as WF

open hPropView 𝒮ᵥ 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 = hPropView 𝒮ᵥ 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 = hPropView 𝒮ʟ using ( S )
module Sem = FOL.Semantics 𝒮ʟ
module At = Sem.At SL.S id
```

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 α' → ⊥₀
    not-card κ∈a c = ∈-irrefl a (least α' orda c κ∈a α' a∈δ)

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

    exFo : Formula SL.S 1
    exFo = ∃̇ ((var zero ∈̇ var (suc zero))
             ∧̇ injLAt (suc zero) zero)

    exFill : Ex → ⟨ (α' ∷ []) At.⊨ exFo ⟩
    exFill = map₁ (λ { (γ , γ∈a , inj) → γ , γ∈a
      , InjLAt.fill (suc zero) zero (γ ∷ α' ∷ []) inj })

    exRead : ⟨ (α' ∷ []) At.⊨ exFo ⟩ → Ex
    exRead = map₁ (λ { (γ , γ∈a , sat) → γ , γ∈a
      , InjLAt.read (suc zero) zero (γ ∷ α' ∷ []) sat })

    exDecision : Dec Ex
    exDecision = mapDec exRead (λ ns e → ns (exFill e))
      (FOL.Semantics.decideSatisfaction 𝒮ʟ id lem (α' ∷ []) exFo)
```

The formula `exFo` binds the possible `γ`, conjoins `γ ∈ α'` with the formula `injLAt α' γ`, and therefore presents exactly `Ex`. The maps `exFill` and `exRead` prove the two directions under propositional truncation. Excluded middle is then applied through `decideSatisfaction` to this formula. If satisfaction holds, the required mere witness is present; if it is refuted, every proposed member and injection yields a contradiction, precisely the condition saying that `α'` is a cardinal.

```agda
    some-γ : ⟨ κ .fst ∈ˢ a ⟩ → Ex
    some-γ κ∈a = decide exDecision
      where
      decide : Dec Ex → 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 (yes e) = e
      decide (no ¬e) =
        ⊥₀-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)) = 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.