The first infinite ordinal in models of ZF

This module develops the theory of ω and the natural numbers inside a von Neumann model of ZF, providing the infinitary tools needed for the Kunen inconsistency argument.

def Set.toZFSet {A : ZFSet.{u_1}} (B : Set ↥A) : ZFSet.{u_1}

The toZFSet declaration.

Equations

• B.toZFSet = ZFSet.sep (fun (x : ZFSet.{?u.1}) => ∃ (hx : x ∈ A), ⟨x, hx⟩ ∈ B) A

@[simp]

theorem Set.mem_toZFSet {A : ZFSet.{u_1}} (B : Set ↥A) (x : ZFSet.{u_1}) : x ∈ B.toZFSet ↔ ∃ (hx : x ∈ A), ⟨x, hx⟩ ∈ B

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

The IsWellFoundedRevMem declaration.

Equations

• SetTheory.IsWellFoundedRevMem x = ∀ S ∈ 𝓟 x, S ≠ ∅ → ∃ y ∈ S, ∀ z ∈ S, y ∉ z

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

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

theorem SetTheory.IsWellFoundedRevMem.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) : IsWellFoundedRevMem (j x₁) ↔ IsWellFoundedRevMem x₁

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

The MemOmega declaration.

Equations

• SetTheory.MemOmega x = (SetTheory.IsOrdinal x ∧ SetTheory.IsWellFoundedRevMem x)

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

theorem SetTheory.MemOmega.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) : MemOmega (j x₁) ↔ MemOmega x₁

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

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

theorem SetTheory.forall_set {x : ZFSet.{u_1}} {p : Set ↥x → Prop} : (∀ (y : Set ↥x), p y) ↔ ∀ y ⊆ x, p {z : ↥x | ↑z ∈ y}

theorem SetTheory.IsWellFoundedRevMem.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : IsWellFoundedRevMem x ↔ IsWellFounded ↥⇓x fun (a b : ↥⇓x) => b ∈ a

noncomputable def SetTheory.ωₛ : ZFSet.{u_1}

The ωₛ declaration.

Equations

• SetTheory.ωₛ = Ordinal.omega0.toZFSet

@[implicit_reducible]

noncomputable instance SetTheory.instNatCastM {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : NatCast M

Equations

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

@[implicit_reducible]

noncomputable instance SetTheory.instOfNatM {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {n : ℕ} : OfNat M n

Equations

• SetTheory.instOfNatM = { ofNat := ↑n }

theorem SetTheory.NatCast.natCast.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {n : ℕ} : ⇓↑n = (↑n).toZFSet

theorem SetTheory.ofNat_eq_natCast {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (n : ℕ) : OfNat.ofNat n = ↑n

theorem SetTheory.natCast_zero {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : 0 = ∅

theorem SetTheory.natCast_succ {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {n : ℕ} : ↑(n + 1) = succ ↑n

theorem SetTheory.toZFSet_nat_mem_ωₛ {n : ℕ} : (↑n).toZFSet ∈ ωₛ

theorem SetTheory.eq_natCast_of_mem_ωₛ {α : ZFSet.{u_1}} (hα : α ∈ ωₛ) : ∃ (n : ℕ), α = (↑n).toZFSet

theorem SetTheory.nwf_rev_of_ωₛ_le {α : ZFSet.{0}} (hα : ωₛ ≤ α) : ¬IsWellFounded ↥α fun (x y : ↥α) => y ∈ x

theorem SetTheory.wf_rev_of_lt_ωₛ {α : ZFSet.{0}} (hα : α ∈ ωₛ) : IsWellFounded ↥α fun (x y : ↥α) => y ∈ x

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

theorem SetTheory.MemOmega.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (n : M) : MemOmega n ↔ ⇓n ∈ ωₛ

theorem SetTheory.eq_natCast_of_memOmega {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α : M} (hα : MemOmega α) : ∃ (n : ℕ), α = ↑n

theorem SetTheory.memOmega_natCast {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {n : ℕ} : MemOmega ↑n

theorem SetTheory.ωₘ.eu {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] : IsSet {n : M₀ | MemOmega n}

noncomputable def SetTheory.ωₘ {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumannWithOmega M] : M

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

Equations

• SetTheory.ωₘ = Exists.choose ⋯

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

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

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

theorem SetTheory.ωₘ.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumannWithOmega M] (y : M) : y ∈ ωₘ ↔ MemOmega y

theorem SetTheory.ωₘ.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumannWithOmega M] (v : M) : ωₘ = v ↔ ∀ (y : M), y ∈ v ↔ MemOmega y

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

@[simp]

theorem SetTheory.natCast_mem_ωₘ {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] {n : ℕ} : ↑n ∈ ωₘ

theorem SetTheory.ωₘ.toV {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] : ωₘ = ↓ωₘ

theorem SetTheory.ωₘ.toZFSet {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] : ⇓ωₘ = ωₛ

@[simp]

theorem SetTheory.isOrdinal_ωₘ {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] : IsOrdinal ωₘ

noncomputable def SetTheory.omegaEquiv {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] : ↥ωₘ ≃ ℕ

The omegaEquiv declaration.

Equations

• SetTheory.omegaEquiv = (Equiv.ofBijective (fun (n : ℕ) => ⟨↑n, ⋯⟩) ⋯).symm

@[implicit_reducible]

noncomputable instance SetTheory.instOfNatOrdinals {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {n : ℕ} : OfNat (Ordinals M) n

Equations

• SetTheory.instOfNatOrdinals = { ofNat := ⟨↑n, ⋯⟩ }