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.

TODO

• Define the von Neumann hierarchy.
• Build correspondences between these set notions and those of the standard Ordinal type.

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.

Equations

• x.IsTransitive = ∀ y ∈ x, y ⊆ x

@[simp]

theorem ZFSet.isTransitive_empty : ∅.IsTransitive

@[deprecated ZFSet.isTransitive_empty (since := "2024-09-21")]

theorem ZFSet.empty_isTransitive : ∅.IsTransitive

Alias of ZFSet.isTransitive_empty.

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).IsTransitive

The union of a transitive set is transitive.

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

The union of transitive sets is transitive.

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 ⊆ x

theorem ZFSet.IsTransitive.sUnion_subset {x : ZFSet.{u}} : x.IsTransitive → ⋃₀ x ⊆ 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.not_mem_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.isTrichotomous {x : ZFSet.{u}} (h : x.IsOrdinal) : IsTrichotomous { 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_isTrichotomous {x : ZFSet.{u}} : x.IsOrdinal ↔ x.IsTransitive ∧ IsTrichotomous { 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, 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.

@[simp]

theorem ZFSet.isOrdinal_empty : ∅.IsOrdinal

theorem ZFSet.isOrdinal_not_mem_univ : IsOrdinal ∉ Class.univ

The Burali-Forti paradox: ordinals form a proper class.