Von Neumann ordinals

This file works towards the development of von Neumann ordinals, i.e. transitive sets, well-ordered under ∈.

Definitions

• ZFSet.IsTransitive means that every element of a set is a subset.
• ZFSet.IsOrdinal means that the set is transitive and well-ordered under ∈. We show multiple equivalences to this definition.
• Ordinal.toZFSet converts Lean's type-theoretic ordinals into ZFC ordinals. We prove that these two notions are order-isomorphic.

Transitive sets

def ZFSet.IsTransitive (x : ZFSet.{u_1}) : Prop

A transitive set is one where every element is a subset.

This is equivalent to being an infinite-open interval in the transitive closure of membership.

@[simp]

theorem ZFSet.isTransitive_empty : ∅.IsTransitive

theorem ZFSet.IsTransitive.subset_of_mem {x y : ZFSet.{u}} (h : x.IsTransitive) : y ∈ x → y ⊆ x

theorem ZFSet.isTransitive_iff_mem_trans {z : ZFSet.{u}} : z.IsTransitive ↔ ∀ {x y : ZFSet.{u}}, x ∈ y → y ∈ z → x ∈ z

theorem ZFSet.IsTransitive.mem_trans {z : ZFSet.{u}} : z.IsTransitive → ∀ {x y : ZFSet.{u}}, x ∈ y → y ∈ z → x ∈ z

Alias of the forward direction of ZFSet.isTransitive_iff_mem_trans.

theorem ZFSet.IsTransitive.inter {x y : ZFSet.{u}} (hx : x.IsTransitive) (hy : y.IsTransitive) : (x ∩ y).IsTransitive

theorem ZFSet.IsTransitive.sUnion {x : ZFSet.{u}} (h : x.IsTransitive) : x.sUnion.IsTransitive

The union of a transitive set is transitive.

theorem ZFSet.IsTransitive.sUnion' {x : ZFSet.{u}} (H : ∀ y ∈ x, y.IsTransitive) : x.sUnion.IsTransitive

The union of transitive sets is transitive.

theorem ZFSet.IsTransitive.iUnion {α : Type u_1} [Small.{u, u_1} α] {f : α → ZFSet.{u}} (hf : ∀ (i : α), (f i).IsTransitive) : (iUnion fun (i : α) => f i).IsTransitive

theorem ZFSet.IsTransitive.union {x y : ZFSet.{u}} (hx : x.IsTransitive) (hy : y.IsTransitive) : (x ∪ y).IsTransitive

theorem ZFSet.IsTransitive.powerset {x : ZFSet.{u}} (h : x.IsTransitive) : x.powerset.IsTransitive

theorem ZFSet.isTransitive_iff_sUnion_subset {x : ZFSet.{u}} : x.IsTransitive ↔ x.sUnion ⊆ x

theorem ZFSet.IsTransitive.sUnion_subset {x : ZFSet.{u}} : x.IsTransitive → x.sUnion ⊆ x

Alias of the forward direction of ZFSet.isTransitive_iff_sUnion_subset.

theorem ZFSet.isTransitive_iff_subset_powerset {x : ZFSet.{u}} : x.IsTransitive ↔ x ⊆ x.powerset

theorem ZFSet.IsTransitive.subset_powerset {x : ZFSet.{u}} : x.IsTransitive → x ⊆ x.powerset

Alias of the forward direction of ZFSet.isTransitive_iff_subset_powerset.

Ordinals

structure ZFSet.IsOrdinal (x : ZFSet.{u_1}) : Prop

A set x is a von Neumann ordinal when it's a transitive set, that's transitive under ∈. We prove that this further implies that x is well-ordered under ∈ in isOrdinal_iff_isWellOrder.

The transitivity condition a ∈ b → b ∈ c → a ∈ c can be written without assuming a ∈ x and b ∈ x. The lemma isOrdinal_iff_isTrans shows this condition is equivalent to the usual one.

• isTransitive : x.IsTransitive

  An ordinal is a transitive set.

• mem_trans' {y z w : ZFSet.{u_1}} : y ∈ z → z ∈ w → w ∈ x → y ∈ w

  The membership operation within an ordinal is transitive.

theorem ZFSet.IsOrdinal.subset_of_mem {x y : ZFSet.{u}} (h : x.IsOrdinal) : y ∈ x → y ⊆ x

theorem ZFSet.IsOrdinal.mem_trans {x y z : ZFSet.{u}} (h : z.IsOrdinal) : x ∈ y → y ∈ z → x ∈ z

theorem ZFSet.IsOrdinal.isTrans {x : ZFSet.{u}} (h : x.IsOrdinal) : IsTrans { x_1 : ZFSet.{u} // x_1 ∈ x } (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

theorem ZFSet.isOrdinal_iff_isTrans {x : ZFSet.{u}} : x.IsOrdinal ↔ x.IsTransitive ∧ IsTrans { x_1 : ZFSet.{u} // x_1 ∈ x } (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

The simplified form of transitivity used within IsOrdinal yields an equivalent definition to the standard one.

theorem ZFSet.IsOrdinal.mem {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y ∈ x) : y.IsOrdinal

theorem ZFSet.isOrdinal_iff_forall_mem_isTransitive {x : ZFSet.{u}} : x.IsOrdinal ↔ x.IsTransitive ∧ ∀ y ∈ x, y.IsTransitive

An ordinal is a transitive set of transitive sets.

theorem ZFSet.isOrdinal_iff_forall_mem_isOrdinal {x : ZFSet.{u}} : x.IsOrdinal ↔ x.IsTransitive ∧ ∀ y ∈ x, y.IsOrdinal

An ordinal is a transitive set of ordinals.

theorem ZFSet.IsOrdinal.subset_iff_eq_or_mem {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ⊆ y ↔ x = y ∨ x ∈ y

theorem ZFSet.IsOrdinal.eq_or_mem_of_subset {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ⊆ y → x = y ∨ x ∈ y

Alias of the forward direction of ZFSet.IsOrdinal.subset_iff_eq_or_mem.

theorem ZFSet.IsOrdinal.mem_of_subset_of_mem {x y z : ZFSet.{u}} (h : x.IsOrdinal) (hz : z.IsOrdinal) (hx : x ⊆ y) (hy : y ∈ z) : x ∈ z

theorem ZFSet.IsOrdinal.notMem_iff_subset {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∉ y ↔ y ⊆ x

theorem ZFSet.IsOrdinal.not_subset_iff_mem {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : ¬x ⊆ y ↔ y ∈ x

theorem ZFSet.IsOrdinal.mem_or_subset {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ∨ y ⊆ x

theorem ZFSet.IsOrdinal.subset_total {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ⊆ y ∨ y ⊆ x

theorem ZFSet.IsOrdinal.mem_trichotomous {x y : ZFSet.{u}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ∨ x = y ∨ y ∈ x

theorem ZFSet.IsOrdinal.trichotomous {x : ZFSet.{u}} (h : x.IsOrdinal) : Std.Trichotomous (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

@[deprecated ZFSet.IsOrdinal.trichotomous (since := "2026-01-24")]

theorem ZFSet.IsOrdinal.isTrichotomous {x : ZFSet.{u}} (h : x.IsOrdinal) : Std.Trichotomous (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

Alias of ZFSet.IsOrdinal.trichotomous.

theorem ZFSet.isOrdinal_iff_trichotomous {x : ZFSet.{u}} : x.IsOrdinal ↔ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

An ordinal is a transitive set, trichotomous under membership.

@[deprecated ZFSet.isOrdinal_iff_trichotomous (since := "2026-01-24")]

theorem ZFSet.isOrdinal_iff_isTrichotomous {x : ZFSet.{u}} : x.IsOrdinal ↔ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

Alias of ZFSet.isOrdinal_iff_trichotomous.

---

An ordinal is a transitive set, trichotomous under membership.

theorem ZFSet.IsOrdinal.isWellOrder {x : ZFSet.{u}} (h : x.IsOrdinal) : IsWellOrder { x_1 : ZFSet.{u} // x_1 ∈ x } (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

theorem ZFSet.isOrdinal_iff_isWellOrder {x : ZFSet.{u}} : x.IsOrdinal ↔ x.IsTransitive ∧ IsWellOrder { x_1 : ZFSet.{u} // x_1 ∈ x } (Subrel (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) fun (x_1 : ZFSet.{u}) => x_1 ∈ x)

An ordinal is a transitive set, well-ordered under membership.

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

theorem ZFSet.IsOrdinal.rank_le_iff_subset {x y : ZFSet.{u_1}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x.rank ≤ y.rank ↔ x ⊆ y

theorem ZFSet.IsOrdinal.rank_inj {x y : ZFSet.{u_1}} (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x.rank = y.rank ↔ x = y

@[simp]

theorem ZFSet.isOrdinal_empty : ∅.IsOrdinal

theorem ZFSet.isOrdinal_succ {x : ZFSet.{u_1}} (h : x.IsOrdinal) : (insert x x).IsOrdinal

Type-theoretic ordinals to von Neumann ordinals

@[irreducible]

noncomputable def Ordinal.toPSet (o : Ordinal.{u}) : PSet.{u}

The von Neumann ordinal corresponding to a given Ordinal, as a PSet.

The elements of o.toPSet are all a.toPSet with a < o.

@[simp]

theorem Ordinal.type_toPSet (o : Ordinal.{u_1}) : o.toPSet.Type = o.ToType

theorem Ordinal.mem_toPSet_iff {o : Ordinal.{u_1}} {x : PSet.{u_1}} : x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet

@[simp, irreducible]

theorem Ordinal.rank_toPSet (o : Ordinal.{u_1}) : o.toPSet.rank = o

noncomputable def Ordinal.toZFSet (o : Ordinal.{u}) : ZFSet.{u}

The von Neumann ordinal corresponding to a given Ordinal, as a ZFSet.

The elements of o.toZFSet are all a.toZFSet with a < o.

@[simp]

theorem Ordinal.mk_toPSet (o : Ordinal.{u_1}) : ZFSet.mk o.toPSet = o.toZFSet

theorem Ordinal.mem_toZFSet_iff {o : Ordinal.{u_1}} {x : ZFSet.{u_1}} : x ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = x

@[simp]

theorem Ordinal.rank_toZFSet (o : Ordinal.{u_1}) : o.toZFSet.rank = o

@[simp]

theorem Ordinal.coe_toZFSet {o : Ordinal.{u_1}} : ↑o.toZFSet = toZFSet '' Set.Iio o

theorem Ordinal.toZFSet_monotone : Monotone toZFSet

@[simp]

theorem Ordinal.toZFSet_mem_toZFSet_iff {a b : Ordinal.{u_1}} : a.toZFSet ∈ b.toZFSet ↔ a < b

@[simp]

theorem Ordinal.toZFSet_subset_toZFSet_iff {a b : Ordinal.{u_1}} : a.toZFSet ⊆ b.toZFSet ↔ a ≤ b

theorem Ordinal.toZFSet_strictMono : StrictMono toZFSet

theorem Ordinal.toZFSet_injective : Function.Injective toZFSet

@[simp]

theorem Ordinal.toZFSet_zero : toZFSet 0 = ∅

@[simp]

theorem Ordinal.toZFSet_succ (o : Ordinal.{u_1}) : (Order.succ o).toZFSet = insert o.toZFSet o.toZFSet

@[simp]

theorem Ordinal.card_toZFSet (o : Ordinal.{u_1}) : o.toZFSet.card = o.card

theorem ZFSet.isOrdinal_toZFSet (o : Ordinal.{u_1}) : o.toZFSet.IsOrdinal

theorem ZFSet.IsOrdinal.toZFSet_rank_eq {x : ZFSet.{u_1}} (hx : x.IsOrdinal) : x.rank.toZFSet = x

theorem ZFSet.isOrdinal_iff_mem_range_toZFSet {x : ZFSet.{u}} : x.IsOrdinal ↔ x ∈ Set.range Ordinal.toZFSet

noncomputable def Ordinal.toZFSetIso : Ordinal.{u_1} ≃o { x : ZFSet.{u_1} // x.IsOrdinal }

Ordinal is order-equivalent to the type of von Neumann ordinals.

@[simp]

theorem Ordinal.toZFSetIso_apply (o : Ordinal.{u_1}) : toZFSetIso o = ⟨o.toZFSet, ⋯⟩

@[simp]

theorem Ordinal.toZFSetIso_symm_apply (x : { x : ZFSet.{u_1} // x.IsOrdinal }) : (RelIso.symm toZFSetIso) x = (↑x).rank