feat(set_theory/zfc/ordinal): transitive sets (#15288)

We define transitive sets, as an initial development towards von Neumann ordinals.

src/set_theory/zfc.lean → src/set_theory/zfc/basic.lean

@@ -556,6 +556,9 @@ prefix `⋃₀ `:110 := Set.sUnion
 quotient.induction_on₂ x y (λ x y, iff.trans mem_sUnion
   ⟨λ ⟨z, h⟩, ⟨⟦z⟧, h⟩, λ ⟨z, h⟩, quotient.induction_on z (λ z h, ⟨z, h⟩) h⟩)
 
+theorem mem_sUnion_of_mem {x y z : Set} (hy : y ∈ z) (hz : z ∈ x) : y ∈ ⋃₀ x :=
+mem_sUnion.2 ⟨z, hz, hy⟩
+
 @[simp] theorem sUnion_singleton {x : Set.{u}} : ⋃₀ ({x} : Set) = x :=
 ext $ λ y, by simp_rw [mem_sUnion, exists_prop, mem_singleton, exists_eq_left]
 

src/set_theory/zfc/ordinal.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2022 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+
+import set_theory.zfc.basic
+
+/-!
+# 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
+
+- `Set.is_transitive` 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
+  `set_theory/ordinal/arithmetic.lean`.
+-/
+
+namespace Set
+
+/-- A transitive set is one where every element is a subset. -/
+def is_transitive (x : Set) : Prop := ∀ y ∈ x, y ⊆ x
+
+theorem is_transitive.subset_of_mem {x y : Set} (h : x.is_transitive) : y ∈ x → y ⊆ x := h y
+
+theorem is_transitive_iff_mem_trans {z : Set} :
+  z.is_transitive ↔ ∀ {x y : Set}, x ∈ y → y ∈ z → x ∈ z :=
+⟨λ h x y hx hy, h.subset_of_mem hy hx, λ H x hx y hy, H hy hx⟩
+
+alias is_transitive_iff_mem_trans ↔ is_transitive.mem_trans _
+
+theorem is_transitive.sUnion {x : Set} (h : x.is_transitive) : (⋃₀ x).is_transitive :=
+λ y hy z hz, begin
+  rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩,
+  exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)
+end
+
+theorem is_transitive_iff_sUnion_subset {x : Set} : x.is_transitive ↔ ⋃₀ x ⊆ x :=
+⟨λ h y hy, by { rcases mem_sUnion.1 hy with ⟨z, hz, hz'⟩, exact h.mem_trans hz' hz },
+  λ H y hy z hz, H $ mem_sUnion_of_mem hz hy⟩
+
+alias is_transitive_iff_sUnion_subset ↔ is_transitive.sUnion_subset _
+
+theorem is_transitive_iff_subset_powerset {x : Set} : x.is_transitive ↔ x ⊆ powerset x :=
+⟨λ h y hy, mem_powerset.2 $ h.subset_of_mem hy, λ H y hy z hz, mem_powerset.1 (H hy) hz⟩
+
+alias is_transitive_iff_subset_powerset ↔ is_transitive.subset_powerset _
+
+end Set