Ordinals in models of ZF

This module develops the theory of ordinals inside a von Neumann model of ZF, including their order structure and the correspondence with Mathlib's Ordinal type.

def SetTheory.IsOrdinal {M : Type 1} [ZFStructure M] (x : M) : Prop

The IsOrdinal declaration.

Equations

• SetTheory.IsOrdinal x = (SetTheory.IsTransitive x ∧ ∀ y ∈ x, SetTheory.IsTransitive y)

theorem SetTheory.IsOrdinal.elementarity {M : Type 1} [sM : ZFStructure M] {N : Type 1} [sN : ZFStructure N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsOrdinal (j x₁) ↔ IsOrdinal x₁

theorem SetTheory.IsOrdinal.to_realize {M : Type 1} [sM : ZFStructure M] (x₁ : M) : IsOrdinal x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

theorem SetTheory.IsOrdinal.realize_iff {M : Type 1} [sM : ZFStructure M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsOrdinal (v✝ 0)

def SetTheory.IsStrongLimit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (κ : M) : Prop

The IsStrongLimit declaration.

Equations

• SetTheory.IsStrongLimit κ = (SetTheory.IsOrdinal κ ∧ ∀ α ∈ κ, SetTheory.cardLT (𝓟 α) κ)

theorem SetTheory.IsStrongLimit.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsStrongLimit (j x₁) ↔ IsStrongLimit x₁

theorem SetTheory.IsStrongLimit.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsStrongLimit (v✝ 0)

theorem SetTheory.IsStrongLimit.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsStrongLimit x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

def SetTheory.IsOrdinalValuedFunc {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (f : M) : Prop

The IsOrdinalValuedFunc declaration.

Equations

• SetTheory.IsOrdinalValuedFunc f = (SetTheory.IsFunc f ∧ ∀ x ∈ SetTheory.Ran f, SetTheory.IsOrdinal x)

theorem SetTheory.IsOrdinalValuedFunc.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsOrdinalValuedFunc (v✝ 0)

theorem SetTheory.IsOrdinalValuedFunc.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsOrdinalValuedFunc (j x₁) ↔ IsOrdinalValuedFunc x₁

theorem SetTheory.IsOrdinalValuedFunc.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsOrdinalValuedFunc x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

theorem SetTheory.IsOrdinal.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (α : M) : IsOrdinal ↓α ↔ IsOrdinal α

theorem SetTheory.IsOrdinal.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (α : M) : IsOrdinal α ↔ (⇓α).IsOrdinal

@[simp]

theorem SetTheory.isOrdinal_empty {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : IsOrdinal ∅

theorem ZFSet.IsOrdinal.mem_iff_lt {x y : ZFSet.{u_1}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ↔ x < y

theorem SetTheory.IsOrdinal.mem_iff_lt {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} (hx : IsOrdinal x) (hy : IsOrdinal y) : x ∈ y ↔ x < y

@[reducible, inline]

abbrev SetTheory.Ordinals (M : Type 1) [ZFStructure M] : Type 1

The Ordinals declaration.

Equations

• SetTheory.Ordinals M = { x : M // SetTheory.IsOrdinal x }

noncomputable def SetTheory.rank {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : M

The rank declaration.

Equations

• One or more equations did not get rendered due to their size.

theorem SetTheory.toZFSet_rank {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : ⇓(rank x) = (⇓x).rank.toZFSet

theorem SetTheory.rank_mem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} (mem : x ∈ y) : rank x < rank y

theorem SetTheory.rank_mono {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} (sub : x ⊆ y) : rank x ≤ rank y

theorem SetTheory.rank_ordinal {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α : M} (hα : IsOrdinal α) : rank α = α

@[simp]

theorem SetTheory.isOrdinal_rank {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α : M} : IsOrdinal (rank α)

theorem SetTheory.IsOrdinal.mem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α β : M} (hx : IsOrdinal α) (hy : β ∈ α) : IsOrdinal β

theorem SetTheory.IsOrdinal.lt_of_mem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α β : M} (hx : IsOrdinal α) (hy : β ∈ α) : β < α

theorem SetTheory.IsOrdinal.not_le_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α β : M} (hα : IsOrdinal α) (hβ : IsOrdinal β) : ¬α ≤ β ↔ β < α

theorem SetTheory.rank_enoughTransitive {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : rank ↑(enoughTransitive x) = rank x

theorem SetTheory.rank_trcl {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : rank (trcl x) = rank x

theorem SetTheory.rank_singleton {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : rank {x} = succ (rank x)

noncomputable def SetTheory.rankFunc {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : ↥(trcl {x}) → ↥(succ (rank x))

The rankFunc declaration.

Equations

• SetTheory.rankFunc x ⟨y, hy⟩ = ⟨SetTheory.rank y, ⋯⟩

def SetTheory.IsRankFunction {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x f : M) : Prop

The IsRankFunction declaration.

Equations

• SetTheory.IsRankFunction x f = (SetTheory.IsOrdinalValuedFunc f ∧ SetTheory.IsTransitive (SetTheory.Dom f) ∧ x ∈ SetTheory.Dom f ∧ SetTheory.PreserveMem f)

theorem SetTheory.IsRankFunction.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsRankFunction (j x₁) (j x₂) ↔ IsRankFunction x₁ x₂

theorem SetTheory.IsRankFunction.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : IsRankFunction x₁ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.IsRankFunction.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsRankFunction (v✝ 0) (v✝ 1)

theorem SetTheory.isRankFunction_rankFunc {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : IsRankFunction x (funcToSet (rankFunc x))

theorem SetTheory.rankAux.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : ∃! α : M, IsGLB {α : M | ∃ (f : M), IsRankFunction x f ∧ apply f x = α} α

theorem SetTheory.rankAux.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ rankAux (v✝ 0) = v✝ 1

theorem SetTheory.rankAux.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsGLB {α : M | ∃ (f : M), IsRankFunction x₁ f ∧ apply f x₁ = α} (rankAux x₁)

theorem SetTheory.rankAux.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : rankAux x₁ = v ↔ IsGLB {α : M | ∃ (f : M), IsRankFunction x₁ f ∧ apply f x₁ = α} v

theorem SetTheory.rankAux.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : rankAux (j x₁) = j (rankAux x₁)

theorem SetTheory.rankAux.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : rankAux x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

instance SetTheory.rankAux.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => rankAux (v 0)

noncomputable def SetTheory.rankAux {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.rankAux x₁ = Exists.choose ⋯

theorem SetTheory.rank_induction {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {p : M → Prop} (x : M) (h : ∀ (x : M), (∀ (y : M), rank y < rank x → p y) → p x) : p x

theorem SetTheory.rankAux_eq_rank {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : rankAux x = rank x

@[implicit_reducible]

noncomputable instance SetTheory.instLinearOrderOrdinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : LinearOrder (Ordinals M)

Equations

• One or more equations did not get rendered due to their size.

instance SetTheory.instWellFoundedLTOrdinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : WellFoundedLT (Ordinals M)

@[implicit_reducible]

noncomputable instance SetTheory.instOrderBotOrdinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : OrderBot (Ordinals M)

Equations

• SetTheory.instOrderBotOrdinals = { bot := ⟨∅, ⋯⟩, bot_le := ⋯ }

@[implicit_reducible]

noncomputable instance SetTheory.instConditionallyCompleteLinearOrderBotOrdinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : ConditionallyCompleteLinearOrderBot (Ordinals M)

Equations

• SetTheory.instConditionallyCompleteLinearOrderBotOrdinals = WellFoundedLT.conditionallyCompleteLinearOrderBot (SetTheory.Ordinals M)

theorem SetTheory.sSup_empty_ordinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : sSup ∅ = ⊥

@[simp]

theorem SetTheory.sInf_empty_ordinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : sInf ∅ = ⊥

noncomputable def SetTheory.toOrdinal {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : Ordinals M ↪o Ordinal.{0}

The toOrdinal declaration.

Equations

• SetTheory.toOrdinal = { toFun := fun (α : SetTheory.Ordinals M) => (⇓↑α).rank, inj' := ⋯, map_rel_iff' := ⋯ }

def SetTheory.maxOrdinal (M : Type 1) [ZFStructure M] [hM : IsVonNeumann M] : WithTop Ordinal.{0}

The maxOrdinal declaration.

Equations

• One or more equations did not get rendered due to their size.

theorem SetTheory.maxOrdinal_vonNeumann {μ : Ordinal.{0}} [Fact (Order.IsSuccLimit μ)] : maxOrdinal ↥(ZFSet.vonNeumann μ) = ↑μ

theorem SetTheory.maxOrdinal_V : maxOrdinal V = ⊤

theorem SetTheory.toZFSet_toOrdinal {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α : Ordinals M} : (toOrdinal α).toZFSet = ⇓↑α

theorem SetTheory.exists_toOrdinal_eq {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α : Ordinal.{0}} (hα : ↑α < maxOrdinal M) : ∃ (β : Ordinals M), toOrdinal β = α

theorem SetTheory.toOrdinal_lt {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α : Ordinals M} : ↑(toOrdinal α) < maxOrdinal M

instance SetTheory.comOrdinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : ContinuousOrderMapBounded Subtype.val

instance SetTheory.comToOrdinal {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : ContinuousOrderMap ⇑toOrdinal