A model of ZFC

In this file, we model Zermelo-Fraenkel set theory (+ choice) using Lean's underlying type theory, building on the pre-sets defined in Mathlib/SetTheory/ZFC/PSet.lean.

The theory of classes is developed in Mathlib/SetTheory/ZFC/Class.lean.

Main definitions

• ZFSet: ZFC set. Defined as PSet quotiented by PSet.Equiv, the extensional equivalence.
• ZFSet.choice: Axiom of choice. Proved from Lean's axiom of choice.
• ZFSet.omega: The von Neumann ordinal ω as a Set.
• Classical.allZFSetDefinable: All functions are classically definable.
• ZFSet.IsFunc : Predicate that a ZFC set is a subset of x × y that can be considered as a ZFC function x → y. That is, each member of x is related by the ZFC set to exactly one member of y.
• ZFSet.funs: ZFC set of ZFC functions x → y.
• ZFSet.Hereditarily p x: Predicate that every set in the transitive closure of x has property p.

Notes

To avoid confusion between the Lean Set and the ZFC Set, docstrings in this file refer to them respectively as "Set" and "ZFC set".

def ZFSet : Type (u + 1)

The ZFC universe of sets consists of the type of pre-sets, quotiented by extensional equivalence.

def ZFSet.mk : PSet.{u_1} → ZFSet.{u_1}

Turns a pre-set into a ZFC set.

@[simp]

theorem ZFSet.mk_eq (x : PSet.{u_1}) : ⟦x⟧ = mk x

@[simp]

theorem ZFSet.mk_out (x : ZFSet.{u_1}) : mk (Quotient.out x) = x

class ZFSet.Definable (n : ℕ) (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) : Type (u + 1)

A set function is "definable" if it is the image of some n-ary PSet function. This isn't exactly definability, but is useful as a sufficient condition for functions that have a computable image.

• out : (Fin n → PSet.{u}) → PSet.{u}

  Turns a definable function into an n-ary PSet function.

• mk_out (xs : Fin n → PSet.{u}) : ZFSet.mk (out f xs) = f fun (x : Fin n) => ZFSet.mk (xs x)

  A set function f is the image of Definable.out f.

@[reducible, inline]

abbrev ZFSet.Definable₁ (f : ZFSet.{u} → ZFSet.{u}) : Type (u + 1)

An abbrev of ZFSet.Definable for unary functions.

@[reducible, inline]

abbrev ZFSet.Definable₁.mk {f : ZFSet.{u} → ZFSet.{u}} (out : PSet.{u} → PSet.{u}) (mk_out : ∀ (x : PSet.{u}), ⟦out x⟧ = f ⟦x⟧) : Definable₁ f

A simpler constructor for ZFSet.Definable₁.

@[reducible, inline]

abbrev ZFSet.Definable₁.out (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] : PSet.{u} → PSet.{u}

Turns a unary definable function into a unary PSet function.

theorem ZFSet.Definable₁.mk_out {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x : PSet.{u}} : ZFSet.mk (out f x) = f (ZFSet.mk x)

@[reducible, inline]

abbrev ZFSet.Definable₂ (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) : Type (u + 1)

An abbrev of ZFSet.Definable for binary functions.

@[reducible, inline]

abbrev ZFSet.Definable₂.mk {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} (out : PSet.{u} → PSet.{u} → PSet.{u}) (mk_out : ∀ (x y : PSet.{u}), ⟦out x y⟧ = f ⟦x⟧ ⟦y⟧) : Definable₂ f

A simpler constructor for ZFSet.Definable₂.

@[reducible, inline]

abbrev ZFSet.Definable₂.out (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] : PSet.{u} → PSet.{u} → PSet.{u}

Turns a binary definable function into a binary PSet function.

theorem ZFSet.Definable₂.mk_out {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} [Definable₂ f] {x y : PSet.{u}} : ZFSet.mk (out f x y) = f (ZFSet.mk x) (ZFSet.mk y)

instance ZFSet.instDefinableOfDefinable₁ (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] (n : ℕ) (g : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) [Definable n g] : Definable n fun (s : Fin n → ZFSet.{u_1}) => f (g s)

instance ZFSet.instDefinableOfDefinable₂ (f : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}) [Definable₂ f] (n : ℕ) (g₁ g₂ : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) [Definable n g₁] [Definable n g₂] : Definable n fun (s : Fin n → ZFSet.{u_1}) => f (g₁ s) (g₂ s)

instance ZFSet.instDefinable (n : ℕ) (i : Fin n) : Definable n fun (s : Fin n → ZFSet.{u_1}) => s i

theorem ZFSet.Definable.out_equiv {n : ℕ} (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) [Definable n f] {xs ys : Fin n → PSet.{u}} (h : ∀ (i : Fin n), xs i ≈ ys i) : out f xs ≈ out f ys

theorem ZFSet.Definable₁.out_equiv (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] {x y : PSet.{u}} (h : x ≈ y) : out f x ≈ out f y

theorem ZFSet.Definable₂.out_equiv (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] {x₁ y₁ x₂ y₂ : PSet.{u}} (h₁ : x₁ ≈ y₁) (h₂ : x₂ ≈ y₂) : out f x₁ x₂ ≈ out f y₁ y₂

noncomputable def Classical.allZFSetDefinable {n : ℕ} (F : (Fin n → ZFSet.{u}) → ZFSet.{u}) : ZFSet.Definable n F

All functions are classically definable.

theorem ZFSet.eq {x y : PSet.{u_1}} : mk x = mk y ↔ x.Equiv y

theorem ZFSet.sound {x y : PSet.{u_1}} (h : x.Equiv y) : mk x = mk y

theorem ZFSet.exact {x y : PSet.{u_1}} : mk x = mk y → x.Equiv y

def ZFSet.Mem : ZFSet.{u_1} → ZFSet.{u_1} → Prop

The membership relation for ZFC sets is inherited from the membership relation for pre-sets.

instance ZFSet.instMembership : Membership ZFSet.{u_1} ZFSet.{u_1}

@[simp]

theorem ZFSet.mk_mem_iff {x y : PSet.{u_1}} : mk x ∈ mk y ↔ x ∈ y

def ZFSet.toSet (u : ZFSet.{u}) : Set ZFSet.{u}

Convert a ZFC set into a Set of ZFC sets

@[simp]

theorem ZFSet.mem_toSet (a u : ZFSet.{u}) : a ∈ u.toSet ↔ a ∈ u

instance ZFSet.small_toSet (x : ZFSet.{u}) : Small.{u, u + 1} ↑x.toSet

def ZFSet.Nonempty (u : ZFSet.{u_1}) : Prop

A nonempty set is one that contains some element.

theorem ZFSet.nonempty_def (u : ZFSet.{u_1}) : u.Nonempty ↔ ∃ (x : ZFSet.{u_1}), x ∈ u

theorem ZFSet.nonempty_of_mem {x u : ZFSet.{u_1}} (h : x ∈ u) : u.Nonempty

@[simp]

theorem ZFSet.nonempty_toSet_iff {u : ZFSet.{u_1}} : u.toSet.Nonempty ↔ u.Nonempty

def ZFSet.Subset (x y : ZFSet.{u}) : Prop

x ⊆ y as ZFC sets means that all members of x are members of y.

instance ZFSet.hasSubset : HasSubset ZFSet.{u_1}

theorem ZFSet.subset_def {x y : ZFSet.{u}} : x ⊆ y ↔ ∀ ⦃z : ZFSet.{u}⦄, z ∈ x → z ∈ y

instance ZFSet.instIsReflSubset : IsRefl ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

instance ZFSet.instIsTransSubset : IsTrans ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

@[simp]

theorem ZFSet.subset_iff {x y : PSet.{u_1}} : mk x ⊆ mk y ↔ x ⊆ y

@[simp]

theorem ZFSet.toSet_subset_iff {x y : ZFSet.{u_1}} : x.toSet ⊆ y.toSet ↔ x ⊆ y

theorem ZFSet.ext {x y : ZFSet.{u}} : (∀ (z : ZFSet.{u}), z ∈ x ↔ z ∈ y) → x = y

theorem ZFSet.ext_iff {x y : ZFSet.{u}} : x = y ↔ ∀ (z : ZFSet.{u}), z ∈ x ↔ z ∈ y

theorem ZFSet.toSet_injective : Function.Injective toSet

@[simp]

theorem ZFSet.toSet_inj {x y : ZFSet.{u_1}} : x.toSet = y.toSet ↔ x = y

instance ZFSet.instSetLike : SetLike ZFSet.{u_1} ZFSet.{u_1}

instance ZFSet.instHasSSubset : HasSSubset ZFSet.{u_1}

@[simp]

theorem ZFSet.le_def (x y : ZFSet.{u_1}) : x ≤ y ↔ x ⊆ y

@[simp]

theorem ZFSet.lt_def (x y : ZFSet.{u_1}) : x < y ↔ x ⊂ y

instance ZFSet.instIsAntisymmSubset : IsAntisymm ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

instance ZFSet.instIsNonstrictStrictOrderSubsetSSubset : IsNonstrictStrictOrder ZFSet.{u_1} (fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2) fun (x1 x2 : ZFSet.{u_1}) => x1 ⊂ x2

def ZFSet.empty : ZFSet.{u_1}

The empty ZFC set

instance ZFSet.instEmptyCollection : EmptyCollection ZFSet.{u_1}

instance ZFSet.instInhabited : Inhabited ZFSet.{u_1}

@[simp]

theorem ZFSet.notMem_empty (x : ZFSet.{u}) : x ∉ ∅

@[deprecated ZFSet.notMem_empty (since := "2025-05-23")]

theorem ZFSet.not_mem_empty (x : ZFSet.{u}) : x ∉ ∅

Alias of ZFSet.notMem_empty.

@[simp]

theorem ZFSet.toSet_empty : ∅.toSet = ∅

@[simp]

theorem ZFSet.empty_subset (x : ZFSet.{u}) : ∅ ⊆ x

@[simp]

theorem ZFSet.not_nonempty_empty : ¬∅.Nonempty

@[simp]

theorem ZFSet.nonempty_mk_iff {x : PSet.{u_1}} : (mk x).Nonempty ↔ x.Nonempty

theorem ZFSet.eq_empty (x : ZFSet.{u}) : x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x

theorem ZFSet.eq_empty_or_nonempty (u : ZFSet.{u_1}) : u = ∅ ∨ u.Nonempty

def ZFSet.Insert : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}

Insert x y is the set {x} ∪ y

instance ZFSet.instInsert : Insert ZFSet.{u_1} ZFSet.{u_1}

instance ZFSet.instSingleton : Singleton ZFSet.{u_1} ZFSet.{u_1}

instance ZFSet.instLawfulSingleton : LawfulSingleton ZFSet.{u_1} ZFSet.{u_1}

@[simp]

theorem ZFSet.mem_insert_iff {x y z : ZFSet.{u}} : x ∈ insert y z ↔ x = y ∨ x ∈ z

theorem ZFSet.mem_insert (x y : ZFSet.{u_1}) : x ∈ insert x y

theorem ZFSet.mem_insert_of_mem {y z : ZFSet.{u_1}} (x : ZFSet.{u_1}) (h : z ∈ y) : z ∈ insert x y

@[simp]

theorem ZFSet.toSet_insert (x y : ZFSet.{u_1}) : (insert x y).toSet = insert x y.toSet

@[simp]

theorem ZFSet.mem_singleton {x y : ZFSet.{u}} : x ∈ {y} ↔ x = y

@[simp]

theorem ZFSet.toSet_singleton (x : ZFSet.{u_1}) : {x}.toSet = {x}

theorem ZFSet.insert_nonempty (u v : ZFSet.{u_1}) : (insert u v).Nonempty

theorem ZFSet.singleton_nonempty (u : ZFSet.{u_1}) : {u}.Nonempty

theorem ZFSet.mem_pair {x y z : ZFSet.{u}} : x ∈ {y, z} ↔ x = y ∨ x = z

@[simp]

theorem ZFSet.pair_eq_singleton (x : ZFSet.{u_1}) : {x, x} = {x}

@[simp]

theorem ZFSet.pair_eq_singleton_iff {x y z : ZFSet.{u_1}} : {x, y} = {z} ↔ x = z ∧ y = z

@[simp]

theorem ZFSet.singleton_eq_pair_iff {x y z : ZFSet.{u_1}} : {x} = {y, z} ↔ x = y ∧ x = z

def ZFSet.omega : ZFSet.{u_1}

omega is the first infinite von Neumann ordinal

@[simp]

theorem ZFSet.omega_zero : ∅ ∈ omega

@[simp]

theorem ZFSet.omega_succ {n : ZFSet.{u}} : n ∈ omega → insert n n ∈ omega

def ZFSet.sep (p : ZFSet.{u_1} → Prop) : ZFSet.{u_1} → ZFSet.{u_1}

{x ∈ a | p x} is the set of elements in a satisfying p

instance ZFSet.instSep : Sep ZFSet.{u_1} ZFSet.{u_1}

@[simp]

theorem ZFSet.mem_sep {p : ZFSet.{u} → Prop} {x y : ZFSet.{u}} : y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y

@[simp]

theorem ZFSet.sep_empty (p : ZFSet.{u_1} → Prop) : ZFSet.sep p ∅ = ∅

@[simp]

theorem ZFSet.toSet_sep (a : ZFSet.{u_1}) (p : ZFSet.{u_1} → Prop) : (ZFSet.sep p a).toSet = {x : ZFSet.{u_1} | x ∈ a.toSet ∧ p x}

def ZFSet.powerset : ZFSet.{u_1} → ZFSet.{u_1}

The powerset operation, the collection of subsets of a ZFC set

@[simp]

theorem ZFSet.mem_powerset {x y : ZFSet.{u}} : y ∈ x.powerset ↔ y ⊆ x

theorem ZFSet.sUnion_lem {α β : Type u} (A : α → PSet.{u}) (B : β → PSet.{u}) (αβ : ∀ (a : α), ∃ (b : β), (A a).Equiv (B b)) (a : (⋃₀ PSet.mk α A).Type) : ∃ (b : (⋃₀ PSet.mk β B).Type), ((⋃₀ PSet.mk α A).Func a).Equiv ((⋃₀ PSet.mk β B).Func b)

def ZFSet.sUnion : ZFSet.{u_1} → ZFSet.{u_1}

The union operator, the collection of elements of elements of a ZFC set. Uses ⋃₀ notation, scoped under the ZFSet namespace.

def ZFSet.«term⋃₀_» : Lean.ParserDescr

The union operator, the collection of elements of elements of a ZFC set. Uses ⋃₀ notation, scoped under the ZFSet namespace.

def ZFSet.sInter (x : ZFSet.{u_1}) : ZFSet.{u_1}

The intersection operator, the collection of elements in all of the elements of a ZFC set. We define ⋂₀ ∅ = ∅. Uses ⋂₀ notation, scoped under the ZFSet namespace.

def ZFSet.«term⋂₀_» : Lean.ParserDescr

The intersection operator, the collection of elements in all of the elements of a ZFC set. We define ⋂₀ ∅ = ∅. Uses ⋂₀ notation, scoped under the ZFSet namespace.

@[simp]

theorem ZFSet.mem_sUnion {x y : ZFSet.{u}} : y ∈ x.sUnion ↔ ∃ z ∈ x, y ∈ z

theorem ZFSet.mem_sInter {x y : ZFSet.{u_1}} (h : x.Nonempty) : y ∈ x.sInter ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem ZFSet.sUnion_empty : ∅.sUnion = ∅

@[simp]

theorem ZFSet.sInter_empty : ∅.sInter = ∅

theorem ZFSet.mem_of_mem_sInter {x y z : ZFSet.{u_1}} (hy : y ∈ x.sInter) (hz : z ∈ x) : y ∈ z

theorem ZFSet.mem_sUnion_of_mem {x y z : ZFSet.{u_1}} (hy : y ∈ z) (hz : z ∈ x) : y ∈ x.sUnion

theorem ZFSet.notMem_sInter_of_notMem {x y z : ZFSet.{u_1}} (hy : y ∉ z) (hz : z ∈ x) : y ∉ x.sInter

@[deprecated ZFSet.notMem_sInter_of_notMem (since := "2025-05-23")]

theorem ZFSet.not_mem_sInter_of_not_mem {x y z : ZFSet.{u_1}} (hy : y ∉ z) (hz : z ∈ x) : y ∉ x.sInter

Alias of ZFSet.notMem_sInter_of_notMem.

@[simp]

theorem ZFSet.sUnion_singleton {x : ZFSet.{u}} : {x}.sUnion = x

@[simp]

theorem ZFSet.sInter_singleton {x : ZFSet.{u}} : {x}.sInter = x

@[simp]

theorem ZFSet.toSet_sUnion (x : ZFSet.{u}) : x.sUnion.toSet = ⋃₀ (toSet '' x.toSet)

theorem ZFSet.toSet_sInter {x : ZFSet.{u}} (h : x.Nonempty) : x.sInter.toSet = ⋂₀ (toSet '' x.toSet)

theorem ZFSet.singleton_injective : Function.Injective singleton

@[simp]

theorem ZFSet.singleton_inj {x y : ZFSet.{u_1}} : {x} = {y} ↔ x = y

def ZFSet.union (x y : ZFSet.{u}) : ZFSet.{u}

The binary union operation

def ZFSet.inter (x y : ZFSet.{u}) : ZFSet.{u}

The binary intersection operation

def ZFSet.diff (x y : ZFSet.{u}) : ZFSet.{u}

The set difference operation

instance ZFSet.instUnion : Union ZFSet.{u_1}

instance ZFSet.instInter : Inter ZFSet.{u_1}

instance ZFSet.instSDiff : SDiff ZFSet.{u_1}

@[simp]

theorem ZFSet.toSet_union (x y : ZFSet.{u}) : (x ∪ y).toSet = x.toSet ∪ y.toSet

@[simp]

theorem ZFSet.toSet_inter (x y : ZFSet.{u}) : (x ∩ y).toSet = x.toSet ∩ y.toSet

@[simp]

theorem ZFSet.toSet_sdiff (x y : ZFSet.{u}) : (x \ y).toSet = x.toSet \ y.toSet

@[simp]

theorem ZFSet.mem_union {x y z : ZFSet.{u}} : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

@[simp]

theorem ZFSet.mem_inter {x y z : ZFSet.{u}} : z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

@[simp]

theorem ZFSet.mem_diff {x y z : ZFSet.{u}} : z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

@[simp]

theorem ZFSet.sUnion_pair {x y : ZFSet.{u}} : {x, y}.sUnion = x ∪ y

theorem ZFSet.mem_wf : WellFounded fun (x1 x2 : ZFSet.{u_1}) => x1 ∈ x2

theorem ZFSet.inductionOn {p : ZFSet.{u_1} → Prop} (x : ZFSet.{u_1}) (h : ∀ (x : ZFSet.{u_1}), (∀ y ∈ x, p y) → p x) : p x

Induction on the ∈ relation.

instance ZFSet.instIsWellFoundedMem : IsWellFounded ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ∈ x2

instance ZFSet.instWellFoundedRelation : WellFoundedRelation ZFSet.{u_1}

theorem ZFSet.mem_asymm {x y : ZFSet.{u_1}} : x ∈ y → y ∉ x

theorem ZFSet.mem_irrefl (x : ZFSet.{u_1}) : x ∉ x

theorem ZFSet.not_subset_of_mem {x y : ZFSet.{u_1}} (h : x ∈ y) : ¬y ⊆ x

theorem ZFSet.notMem_of_subset {x y : ZFSet.{u_1}} (h : x ⊆ y) : y ∉ x

@[deprecated ZFSet.notMem_of_subset (since := "2025-05-23")]

theorem ZFSet.not_mem_of_subset {x y : ZFSet.{u_1}} (h : x ⊆ y) : y ∉ x

Alias of ZFSet.notMem_of_subset.

theorem ZFSet.regularity (x : ZFSet.{u}) (h : x ≠ ∅) : ∃ y ∈ x, x ∩ y = ∅

def ZFSet.image (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] : ZFSet.{u_1} → ZFSet.{u_1}

The image of a (definable) ZFC set function

theorem ZFSet.image.mk (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] (x : ZFSet.{u}) {y : ZFSet.{u}} : y ∈ x → f y ∈ image f x

@[simp]

theorem ZFSet.mem_image {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}} : y ∈ image f x ↔ ∃ z ∈ x, f z = y

@[simp]

theorem ZFSet.toSet_image (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] (x : ZFSet.{u_1}) : (image f x).toSet = f '' x.toSet

noncomputable def ZFSet.range {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : ZFSet.{u}

The range of a type-indexed family of sets.

@[simp]

theorem ZFSet.mem_range {α : Type u_1} [Small.{u, u_1} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}} : x ∈ range f ↔ x ∈ Set.range f

@[simp]

theorem ZFSet.toSet_range {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : (range f).toSet = Set.range f

theorem ZFSet.mem_range_self {α : Type u_1} [Small.{u, u_1} α] {f : α → ZFSet.{u}} (a : α) : f a ∈ range f

def ZFSet.pair (x y : ZFSet.{u}) : ZFSet.{u}

Kuratowski ordered pair

@[simp]

theorem ZFSet.toSet_pair (x y : ZFSet.{u}) : (x.pair y).toSet = {{x}, {x, y}}

def ZFSet.pairSep (p : ZFSet.{u} → ZFSet.{u} → Prop) (x y : ZFSet.{u}) : ZFSet.{u}

A subset of pairs {(a, b) ∈ x × y | p a b}

@[simp]

theorem ZFSet.mem_pairSep {p : ZFSet.{u} → ZFSet.{u} → Prop} {x y z : ZFSet.{u}} : z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

theorem ZFSet.pair_injective : Function.Injective2 pair

@[simp]

theorem ZFSet.pair_inj {x y x' y' : ZFSet.{u_1}} : x.pair y = x'.pair y' ↔ x = x' ∧ y = y'

def ZFSet.prod : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}

The cartesian product, {(a, b) | a ∈ x, b ∈ y}

@[simp]

theorem ZFSet.mem_prod {x y z : ZFSet.{u}} : z ∈ x.prod y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b

theorem ZFSet.pair_mem_prod {x y a b : ZFSet.{u}} : a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

def ZFSet.IsFunc (x y f : ZFSet.{u}) : Prop

isFunc x y f is the assertion that f is a subset of x × y which relates to each element of x a unique element of y, so that we can consider f as a ZFC function x → y.

def ZFSet.funs (x y : ZFSet.{u}) : ZFSet.{u}

funs x y is y ^ x, the set of all set functions x → y

@[simp]

theorem ZFSet.mem_funs {x y f : ZFSet.{u}} : f ∈ x.funs y ↔ x.IsFunc y f

instance ZFSet.instDefinable₁Singleton : Definable₁ fun (x : ZFSet.{u_1}) => {x}

instance ZFSet.instDefinable₂Insert : Definable₂ insert

instance ZFSet.instDefinable₂Pair : Definable₂ pair

def ZFSet.map (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] : ZFSet.{u_1} → ZFSet.{u_1}

Graph of a function: map f x is the ZFC function which maps a ∈ x to f a

@[simp]

theorem ZFSet.mem_map {f : ZFSet.{u_1} → ZFSet.{u_1}} [Definable₁ f] {x y : ZFSet.{u_1}} : y ∈ map f x ↔ ∃ z ∈ x, z.pair (f z) = y

theorem ZFSet.map_unique {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x z : ZFSet.{u}} (zx : z ∈ x) : ∃! w : ZFSet.{u}, z.pair w ∈ map f x

@[simp]

theorem ZFSet.map_isFunc {f : ZFSet.{u_1} → ZFSet.{u_1}} [Definable₁ f] {x y : ZFSet.{u_1}} : x.IsFunc y (map f x) ↔ ∀ z ∈ x, f z ∈ y

@[irreducible]

def ZFSet.Hereditarily (p : ZFSet.{u_1} → Prop) (x : ZFSet.{u_1}) : Prop

Given a predicate p on ZFC sets. Hereditarily p x means that x has property p and the members of x are all Hereditarily p.

theorem ZFSet.hereditarily_iff {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} : Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

theorem ZFSet.Hereditarily.def {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} : Hereditarily p x → p x ∧ ∀ y ∈ x, Hereditarily p y

Alias of the forward direction of ZFSet.hereditarily_iff.

theorem ZFSet.Hereditarily.self {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} (h : Hereditarily p x) : p x

theorem ZFSet.Hereditarily.mem {p : ZFSet.{u} → Prop} {x y : ZFSet.{u}} (h : Hereditarily p x) (hy : y ∈ x) : Hereditarily p y

theorem ZFSet.Hereditarily.empty {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} : Hereditarily p x → p ∅