Von Neumann ordinals

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

We currently only have an initial development of transitive sets and ordinals. Further development can be found on the Mathlib 3 branch von_neumann_v2.

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 ∈.

TODO

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

def ZFSet.IsTransitive (x : ZFSet) : Prop

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

Equations

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

@[simp]

theorem ZFSet.isTransitive_empty : ∅.IsTransitive

@[deprecated ZFSet.isTransitive_empty]

theorem ZFSet.empty_isTransitive : ∅.IsTransitive

Alias of ZFSet.isTransitive_empty.

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

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

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

Alias of the forward direction of ZFSet.isTransitive_iff_mem_trans.

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

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

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

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

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

theorem ZFSet.isTransitive_iff_sUnion_subset {x : ZFSet} : x.IsTransitive ↔ ⋃₀ x ⊆ x

theorem ZFSet.IsTransitive.sUnion_subset {x : ZFSet} : x.IsTransitive → ⋃₀ x ⊆ x

Alias of the forward direction of ZFSet.isTransitive_iff_sUnion_subset.

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

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

Alias of the forward direction of ZFSet.isTransitive_iff_subset_powerset.

structure ZFSet.IsOrdinal (x : ZFSet) : Prop

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

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}, 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} (h : x.IsOrdinal) : y ∈ x → y ⊆ x

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

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

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

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