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.

Further development can be found on the branch von_neumann_v2.

Definitions

• ZFSet.IsTransitive means that every element of a set is a subset.

TODO

• Define von Neumann ordinals.
• Define the basic arithmetic operations on ordinals from a purely set-theoretic perspective.
• Prove the equivalences between these definitions and those provided in SetTheory/Ordinal/Arithmetic.lean.

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.empty_isTransitive : ∅.IsTransitive

theorem ZFSet.IsTransitive.subset_of_mem {x : ZFSet} {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 : ZFSet} {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 : ZFSet} {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.