A model of ZFC

In this file, we model Zermelo-Fraenkel set theory (+ Choice) using Lean's underlying type theory. We do this in four main steps:

• Define pre-sets inductively.
• Define extensional equivalence on pre-sets and give it a setoid instance.
• Define ZFC sets by quotienting pre-sets by extensional equivalence.
• Define classes as sets of ZFC sets. Then the rest is usual set theory.

The model

• PSet: Pre-set. A pre-set is inductively defined by its indexing type and its members, which are themselves pre-sets.
• ZFSet: ZFC set. Defined as PSet quotiented by PSet.Equiv, the extensional equivalence.
• Class: Class. Defined as Set ZFSet.
• ZFSet.choice: Axiom of choice. Proved from Lean's axiom of choice.

Other definitions

• Arity α n: n-ary function α → α → ... → α. Defined inductively.
• Arity.const a n: n-ary constant function equal to a.
• PSet.Type: Underlying type of a pre-set.
• PSet.Func: Underlying family of pre-sets of a pre-set.
• PSet.Equiv: Extensional equivalence of pre-sets. Defined inductively.
• PSet.omega, ZFSet.omega: The von Neumann ordinal ω as a PSet, as a Set.
• PSet.Arity.Equiv: Extensional equivalence of n-ary PSet-valued functions. Extension of PSet.Equiv.
• PSet.Resp: Collection of n-ary PSet-valued functions that respect extensional equivalence.
• PSet.eval: Turns a PSet-valued function that respect extensional equivalence into a ZFSet-valued function.
• Classical.allDefinable: 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.
• Class.iota: Definite description operator.

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

TODO

Prove Set.map_definable_aux computably.

def Arity (α : Type u) : ℕ → Type u

The type of n-ary functions α → α → ... → α.

Equations

• Arity α 0 = α
• Arity α (Nat.succ n) = (α → Arity α n)

@[simp]

theorem arity_zero (α : Type u) : Arity α 0 = α

@[simp]

theorem arity_succ (α : Type u) (n : ℕ) : Arity α (Nat.succ n) = (α → Arity α n)

def Arity.const {α : Type u} (a : α) (n : ℕ) : Arity α n

Constant n-ary function with value a.

Equations

• Arity.const a 0 = a
• Arity.const a (Nat.succ n) = fun x => Arity.const a n

@[simp]

theorem Arity.const_zero {α : Type u} (a : α) : Arity.const a 0 = a

@[simp]

theorem Arity.const_succ {α : Type u} (a : α) (n : ℕ) : Arity.const a (Nat.succ n) = fun x => Arity.const a n

theorem Arity.const_succ_apply {α : Type u} (a : α) (n : ℕ) (x : α) : Arity.const α a (Nat.succ n) x = Arity.const a n

instance Arity.Arity.inhabited {α : Type u_1} {n : ℕ} [Inhabited α] : Inhabited (Arity α n)

inductive PSet : Type (u + 1)

• mk: (α : Type u) → (α → PSet) → PSet

The type of pre-sets in universe u. A pre-set is a family of pre-sets indexed by a type in Type u. The ZFC universe is defined as a quotient of this to ensure extensionality.

def PSet.Type : PSet → Type u

The underlying type of a pre-set

def PSet.Func (x : PSet) : PSet.Type x → PSet

The underlying pre-set family of a pre-set

@[simp]

theorem PSet.mk_type (α : Type u_1) (A : α → PSet) : PSet.Type (PSet.mk α A) = α

@[simp]

theorem PSet.mk_func (α : Type u_1) (A : α → PSet) : PSet.Func (PSet.mk α A) = A

@[simp]

theorem PSet.eta (x : PSet) : PSet.mk (PSet.Type x) (PSet.Func x) = x

def PSet.Equiv : PSet → PSet → Prop

Two pre-sets are extensionally equivalent if every element of the first family is extensionally equivalent to some element of the second family and vice-versa.

Equations

• PSet.Equiv (PSet.mk α A) (PSet.mk α_1 B) = ((∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)) ∧ ∀ (b : α_1), ∃ a, PSet.Equiv (A a) (B b))

theorem PSet.equiv_iff {x : PSet} {y : PSet} : PSet.Equiv x y ↔ (∀ (i : PSet.Type x), ∃ j, PSet.Equiv (PSet.Func x i) (PSet.Func y j)) ∧ ∀ (j : PSet.Type y), ∃ i, PSet.Equiv (PSet.Func x i) (PSet.Func y j)

theorem PSet.Equiv.exists_left {x : PSet} {y : PSet} (h : PSet.Equiv x y) (i : PSet.Type x) : ∃ j, PSet.Equiv (PSet.Func x i) (PSet.Func y j)

theorem PSet.Equiv.exists_right {x : PSet} {y : PSet} (h : PSet.Equiv x y) (j : PSet.Type y) : ∃ i, PSet.Equiv (PSet.Func x i) (PSet.Func y j)

theorem PSet.Equiv.refl (x : PSet) : PSet.Equiv x x

theorem PSet.Equiv.rfl {x : PSet} : PSet.Equiv x x

theorem PSet.Equiv.euc {x : PSet} {y : PSet} {z : PSet} : PSet.Equiv x y → PSet.Equiv z y → PSet.Equiv x z

theorem PSet.Equiv.symm {x : PSet} {y : PSet} : PSet.Equiv x y → PSet.Equiv y x

theorem PSet.Equiv.comm {x : PSet} {y : PSet} : PSet.Equiv x y ↔ PSet.Equiv y x

theorem PSet.Equiv.trans {x : PSet} {y : PSet} {z : PSet} (h1 : PSet.Equiv x y) (h2 : PSet.Equiv y z) : PSet.Equiv x z

theorem PSet.equiv_of_isEmpty (x : PSet) (y : PSet) [IsEmpty (PSet.Type x)] [IsEmpty (PSet.Type y)] : PSet.Equiv x y

instance PSet.setoid : Setoid PSet

def PSet.Subset (x : PSet) (y : PSet) : Prop

A pre-set is a subset of another pre-set if every element of the first family is extensionally equivalent to some element of the second family.

instance PSet.instHasSubsetPSet : HasSubset PSet

instance PSet.instIsReflPSetSubsetInstHasSubsetPSet : IsRefl PSet fun x x_1 => x ⊆ x_1

instance PSet.instIsTransPSetSubsetInstHasSubsetPSet : IsTrans PSet fun x x_1 => x ⊆ x_1

theorem PSet.Equiv.ext (x : PSet) (y : PSet) : PSet.Equiv x y ↔ x ⊆ y ∧ y ⊆ x

theorem PSet.Subset.congr_left {x : PSet} {y : PSet} {z : PSet} : PSet.Equiv x y → (x ⊆ z ↔ y ⊆ z)

theorem PSet.Subset.congr_right {x : PSet} {y : PSet} {z : PSet} : PSet.Equiv x y → (z ⊆ x ↔ z ⊆ y)

def PSet.Mem (x : PSet) (y : PSet) : Prop

x ∈ y as pre-sets if x is extensionally equivalent to a member of the family y.

instance PSet.instMembershipPSetPSet : Membership PSet PSet

theorem PSet.Mem.mk {α : Type u} (A : α → PSet) (a : α) : A a ∈ PSet.mk α A

theorem PSet.func_mem (x : PSet) (i : PSet.Type x) : PSet.Func x i ∈ x

theorem PSet.Mem.ext {x : PSet} {y : PSet} : (∀ (w : PSet), w ∈ x ↔ w ∈ y) → PSet.Equiv x y

theorem PSet.Mem.congr_right {x : PSet} {y : PSet} : PSet.Equiv x y → ∀ {w : PSet}, w ∈ x ↔ w ∈ y

theorem PSet.equiv_iff_mem {x : PSet} {y : PSet} : PSet.Equiv x y ↔ ∀ {w : PSet}, w ∈ x ↔ w ∈ y

theorem PSet.Mem.congr_left {x : PSet} {y : PSet} : PSet.Equiv x y → ∀ {w : PSet}, x ∈ w ↔ y ∈ w

theorem PSet.mem_wf : WellFounded fun x x_1 => x ∈ x_1

instance PSet.instWellFoundedRelationPSet : WellFoundedRelation PSet

instance PSet.instIsAsymmPSetMemInstMembershipPSetPSet : IsAsymm PSet fun x x_1 => x ∈ x_1

instance PSet.instIsIrreflPSetMemInstMembershipPSetPSet : IsIrrefl PSet fun x x_1 => x ∈ x_1

theorem PSet.mem_asymm {x : PSet} {y : PSet} : x ∈ y → ¬y ∈ x

theorem PSet.mem_irrefl (x : PSet) : ¬x ∈ x

def PSet.toSet (u : PSet) : Set PSet

Convert a pre-set to a set of pre-sets.

@[simp]

theorem PSet.mem_toSet (a : PSet) (u : PSet) : a ∈ PSet.toSet u ↔ a ∈ u

def PSet.Nonempty (u : PSet) : Prop

A nonempty set is one that contains some element.

theorem PSet.nonempty_def (u : PSet) : PSet.Nonempty u ↔ ∃ x, x ∈ u

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

@[simp]

theorem PSet.nonempty_toSet_iff {u : PSet} : Set.Nonempty (PSet.toSet u) ↔ PSet.Nonempty u

theorem PSet.nonempty_type_iff_nonempty {x : PSet} : Nonempty (PSet.Type x) ↔ PSet.Nonempty x

theorem PSet.nonempty_of_nonempty_type (x : PSet) [h : Nonempty (PSet.Type x)] : PSet.Nonempty x

theorem PSet.Equiv.eq {x : PSet} {y : PSet} : PSet.Equiv x y ↔ PSet.toSet x = PSet.toSet y

Two pre-sets are equivalent iff they have the same members.

instance PSet.instCoePSetSetPSet : Coe PSet (Set PSet)

def PSet.empty : PSet

The empty pre-set

instance PSet.instEmptyCollectionPSet : EmptyCollection PSet

instance PSet.instInhabitedPSet : Inhabited PSet

instance PSet.instIsEmptyTypeEmptyCollectionPSetInstEmptyCollectionPSet : IsEmpty (PSet.Type ∅)

@[simp]

theorem PSet.not_mem_empty (x : PSet) : ¬x ∈ ∅

@[simp]

theorem PSet.toSet_empty : PSet.toSet ∅ = ∅

@[simp]

theorem PSet.empty_subset (x : PSet) : ∅ ⊆ x

@[simp]

theorem PSet.not_nonempty_empty : ¬PSet.Nonempty ∅

theorem PSet.equiv_empty (x : PSet) [IsEmpty (PSet.Type x)] : PSet.Equiv x ∅

def PSet.insert (x : PSet) (y : PSet) : PSet

Insert an element into a pre-set

instance PSet.instInsertPSetPSet : Insert PSet PSet

instance PSet.instSingletonPSetPSet : Singleton PSet PSet

instance PSet.instIsLawfulSingletonPSetInstEmptyCollectionPSetInstInsertPSetPSetInstSingletonPSetPSet : IsLawfulSingleton PSet PSet

instance PSet.instInhabitedTypeInsertPSetInstInsertPSetPSet (x : PSet) (y : PSet) : Inhabited (PSet.Type (insert x y))

def PSet.ofNat : ℕ → PSet

The n-th von Neumann ordinal

Equations

• PSet.ofNat 0 = ∅
• PSet.ofNat (Nat.succ n) = insert (PSet.ofNat n) (PSet.ofNat n)

def PSet.omega : PSet

The von Neumann ordinal ω

def PSet.sep (p : PSet → Prop) (x : PSet) : PSet

The pre-set separation operation {x ∈ a | p x}

instance PSet.instSepPSetPSet : Sep PSet PSet

def PSet.powerset (x : PSet) : PSet

The pre-set powerset operator

@[simp]

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

def PSet.sUnion (a : PSet) : PSet

The pre-set union operator

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

The pre-set union operator

@[simp]

theorem PSet.mem_sUnion {x : PSet} {y : PSet} : y ∈ ⋃₀ x ↔ ∃ z, z ∈ x ∧ y ∈ z

@[simp]

theorem PSet.toSet_sUnion (x : PSet) : PSet.toSet (⋃₀ x) = ⋃₀ (PSet.toSet '' PSet.toSet x)

def PSet.image (f : PSet → PSet) (x : PSet) : PSet

The image of a function from pre-sets to pre-sets.

theorem PSet.mem_image {f : PSet → PSet} (H : ∀ (x y : PSet), PSet.Equiv x y → PSet.Equiv (f x) (f y)) {x : PSet} {y : PSet} : y ∈ PSet.image f x ↔ ∃ z, z ∈ x ∧ PSet.Equiv y (f z)

def PSet.Lift : PSet → PSet

Universe lift operation

Equations

• PSet.Lift (PSet.mk α A) = PSet.mk (ULift.{?u.197, ?u.198} α) fun x => match x with | { down := x } => PSet.Lift (A x)

def PSet.embed : PSet

Embedding of one universe in another

theorem PSet.lift_mem_embed (x : PSet) : PSet.Lift x ∈ PSet.embed

def PSet.Arity.Equiv {n : ℕ} : Arity PSet n → Arity PSet n → Prop

Function equivalence is defined so that f ~ g iff ∀ x y, x ~ y → f x ~ g y. This extends to equivalence of n-ary functions.

Equations

• PSet.Arity.Equiv a b = PSet.Equiv a b
• PSet.Arity.Equiv a b = ∀ (x y : PSet), PSet.Equiv x y → PSet.Arity.Equiv (a x) (b y)

theorem PSet.Arity.equiv_const {a : PSet} (n : ℕ) : PSet.Arity.Equiv (Arity.const a n) (Arity.const a n)

def PSet.Resp (n : ℕ) : Type (u + 1)

resp n is the collection of n-ary functions on PSet that respect equivalence, i.e. when the inputs are equivalent the output is as well.

instance PSet.Resp.inhabited {n : ℕ} : Inhabited (PSet.Resp n)

def PSet.Resp.f {n : ℕ} (f : PSet.Resp (n + 1)) (x : PSet) : PSet.Resp n

The n-ary image of a (n + 1)-ary function respecting equivalence as a function respecting equivalence.

def PSet.Resp.Equiv {n : ℕ} (a : PSet.Resp n) (b : PSet.Resp n) : Prop

Function equivalence for functions respecting equivalence. See PSet.Arity.Equiv.

theorem PSet.Resp.Equiv.refl {n : ℕ} (a : PSet.Resp n) : PSet.Resp.Equiv a a

theorem PSet.Resp.Equiv.euc {n : ℕ} {a : PSet.Resp n} {b : PSet.Resp n} {c : PSet.Resp n} : PSet.Resp.Equiv a b → PSet.Resp.Equiv c b → PSet.Resp.Equiv a c

theorem PSet.Resp.Equiv.symm {n : ℕ} {a : PSet.Resp n} {b : PSet.Resp n} : PSet.Resp.Equiv a b → PSet.Resp.Equiv b a

theorem PSet.Resp.Equiv.trans {n : ℕ} {x : PSet.Resp n} {y : PSet.Resp n} {z : PSet.Resp n} (h1 : PSet.Resp.Equiv x y) (h2 : PSet.Resp.Equiv y z) : PSet.Resp.Equiv x z

instance PSet.Resp.setoid {n : ℕ} : Setoid (PSet.Resp n)

def ZFSet : Type (u + 1)

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

def PSet.Resp.evalAux {n : ℕ} : { f // ∀ (a b : PSet.Resp n), PSet.Resp.Equiv a b → f a = f b }

Helper function for PSet.eval.

Equations

• One or more equations did not get rendered due to their size.

def PSet.Resp.eval (n : ℕ) : PSet.Resp n → Arity ZFSet n

An equivalence-respecting function yields an n-ary ZFC set function.

theorem PSet.Resp.eval_val {n : ℕ} {f : PSet.Resp (n + 1)} {x : PSet} : PSet.Resp.eval (n + 1) f (Quotient.mk PSet.setoid x) = PSet.Resp.eval n (PSet.Resp.f f x)

class inductive PSet.Definable (n : ℕ) : Arity ZFSet n → Type (u + 1)

• mk: {n : ℕ} → (f : PSet.Resp n) → PSet.Definable n (PSet.Resp.eval n f)

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

def PSet.Definable.EqMk {n : ℕ} (f : PSet.Resp n) {s : Arity ZFSet n} : PSet.Resp.eval n f = s → PSet.Definable n s

The evaluation of a function respecting equivalence is definable, by that same function.

def PSet.Definable.Resp {n : ℕ} (s : Arity ZFSet n) [PSet.Definable n s] : PSet.Resp n

Turns a definable function into a function that respects equivalence.

theorem PSet.Definable.eq {n : ℕ} (s : Arity ZFSet n) [H : PSet.Definable n s] : PSet.Resp.eval n (PSet.Definable.Resp s) = s

noncomputable def Classical.allDefinable {n : ℕ} (F : Arity ZFSet n) : PSet.Definable n F

All functions are classically definable.

Equations

• One or more equations did not get rendered due to their size.

def ZFSet.mk : PSet → ZFSet

Turns a pre-set into a ZFC set.

@[simp]

theorem ZFSet.mk_eq (x : PSet) : Quotient.mk PSet.setoid x = ZFSet.mk x

@[simp]

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

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

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

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

@[simp]

theorem ZFSet.eval_mk {n : ℕ} {f : PSet.Resp (n + 1)} {x : PSet} : PSet.Resp.eval (n + 1) f (ZFSet.mk x) = PSet.Resp.eval n (PSet.Resp.f f x)

def ZFSet.Mem : ZFSet → ZFSet → Prop

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

instance ZFSet.instMembershipZFSetZFSet : Membership ZFSet ZFSet

@[simp]

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

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

Convert a ZFC set into a set of ZFC sets

@[simp]

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

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

def ZFSet.Nonempty (u : ZFSet) : Prop

A nonempty set is one that contains some element.

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

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

@[simp]

theorem ZFSet.nonempty_toSet_iff {u : ZFSet} : Set.Nonempty (ZFSet.toSet u) ↔ ZFSet.Nonempty u

def ZFSet.Subset (x : ZFSet) (y : ZFSet) : Prop

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

instance ZFSet.hasSubset : HasSubset ZFSet

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

instance ZFSet.instIsReflZFSetSubsetHasSubset : IsRefl ZFSet fun x x_1 => x ⊆ x_1

instance ZFSet.instIsTransZFSetSubsetHasSubset : IsTrans ZFSet fun x x_1 => x ⊆ x_1

@[simp]

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

@[simp]

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

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

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

theorem ZFSet.toSet_injective : Function.Injective ZFSet.toSet

@[simp]

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

instance ZFSet.instIsAntisymmZFSetSubsetHasSubset : IsAntisymm ZFSet fun x x_1 => x ⊆ x_1

def ZFSet.empty : ZFSet

The empty ZFC set

instance ZFSet.instEmptyCollectionZFSet : EmptyCollection ZFSet

instance ZFSet.instInhabitedZFSet : Inhabited ZFSet

@[simp]

theorem ZFSet.not_mem_empty (x : ZFSet) : ¬x ∈ ∅

@[simp]

theorem ZFSet.toSet_empty : ZFSet.toSet ∅ = ∅

@[simp]

theorem ZFSet.empty_subset (x : ZFSet) : ∅ ⊆ x

@[simp]

theorem ZFSet.not_nonempty_empty : ¬ZFSet.Nonempty ∅

@[simp]

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

theorem ZFSet.eq_empty (x : ZFSet) : x = ∅ ↔ ∀ (y : ZFSet), ¬y ∈ x

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

def ZFSet.Insert : ZFSet → ZFSet → ZFSet

Insert x y is the set {x} ∪ y

instance ZFSet.instInsertZFSetZFSet : Insert ZFSet ZFSet

instance ZFSet.instSingletonZFSetZFSet : Singleton ZFSet ZFSet

instance ZFSet.instIsLawfulSingletonZFSetInstEmptyCollectionZFSetInstInsertZFSetZFSetInstSingletonZFSetZFSet : IsLawfulSingleton ZFSet ZFSet

@[simp]

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

theorem ZFSet.mem_insert (x : ZFSet) (y : ZFSet) : x ∈ insert x y

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem ZFSet.insert_nonempty (u : ZFSet) (v : ZFSet) : ZFSet.Nonempty (insert u v)

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

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

def ZFSet.omega : ZFSet

omega is the first infinite von Neumann ordinal

@[simp]

theorem ZFSet.omega_zero : ∅ ∈ ZFSet.omega

@[simp]

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

def ZFSet.sep (p : ZFSet → Prop) : ZFSet → ZFSet

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

instance ZFSet.instSepZFSetZFSet : Sep ZFSet ZFSet

@[simp]

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

@[simp]

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

def ZFSet.powerset : ZFSet → ZFSet

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

@[simp]

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

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

def ZFSet.sUnion : ZFSet → ZFSet

The union operator, the collection of elements of elements of a ZFC set

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

The union operator, the collection of elements of elements of a ZFC set

noncomputable def ZFSet.sInter (x : ZFSet) : ZFSet

The intersection operator, the collection of elements in all of the elements of a ZFC set. We special-case ⋂₀ ∅ = ∅.

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

The intersection operator, the collection of elements in all of the elements of a ZFC set. We special-case ⋂₀ ∅ = ∅.

@[simp]

theorem ZFSet.mem_sUnion {x : ZFSet} {y : ZFSet} : y ∈ ⋃₀ x ↔ ∃ z, z ∈ x ∧ y ∈ z

theorem ZFSet.mem_sInter {x : ZFSet} {y : ZFSet} (h : ZFSet.Nonempty x) : y ∈ ⋂₀ x ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z

@[simp]

theorem ZFSet.sUnion_empty : ⋃₀ ∅ = ∅

@[simp]

theorem ZFSet.sInter_empty : ⋂₀ ∅ = ∅

theorem ZFSet.mem_of_mem_sInter {x : ZFSet} {y : ZFSet} {z : ZFSet} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) : y ∈ z

theorem ZFSet.mem_sUnion_of_mem {x : ZFSet} {y : ZFSet} {z : ZFSet} (hy : y ∈ z) (hz : z ∈ x) : y ∈ ⋃₀ x

theorem ZFSet.not_mem_sInter_of_not_mem {x : ZFSet} {y : ZFSet} {z : ZFSet} (hy : ¬y ∈ z) (hz : z ∈ x) : ¬y ∈ ⋂₀ x

@[simp]

theorem ZFSet.sUnion_singleton {x : ZFSet} : ⋃₀ {x} = x

@[simp]

theorem ZFSet.sInter_singleton {x : ZFSet} : ⋂₀ {x} = x

@[simp]

theorem ZFSet.toSet_sUnion (x : ZFSet) : ZFSet.toSet (⋃₀ x) = ⋃₀ (ZFSet.toSet '' ZFSet.toSet x)

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

theorem ZFSet.singleton_injective : Function.Injective singleton

@[simp]

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

def ZFSet.union (x : ZFSet) (y : ZFSet) : ZFSet

The binary union operation

def ZFSet.inter (x : ZFSet) (y : ZFSet) : ZFSet

The binary intersection operation

def ZFSet.diff (x : ZFSet) (y : ZFSet) : ZFSet

The set difference operation

instance ZFSet.instUnionZFSet : Union ZFSet

instance ZFSet.instInterZFSet : Inter ZFSet

instance ZFSet.instSDiffZFSet : SDiff ZFSet

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ZFSet.sUnion_pair {x : ZFSet} {y : ZFSet} : ⋃₀ {x, y} = x ∪ y

theorem ZFSet.mem_wf : WellFounded fun x x_1 => x ∈ x_1

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

Induction on the ∈ relation.

instance ZFSet.instWellFoundedRelationZFSet : WellFoundedRelation ZFSet

instance ZFSet.instIsAsymmZFSetMemInstMembershipZFSetZFSet : IsAsymm ZFSet fun x x_1 => x ∈ x_1

instance ZFSet.instIsIrreflZFSetMemInstMembershipZFSetZFSet : IsIrrefl ZFSet fun x x_1 => x ∈ x_1

theorem ZFSet.mem_asymm {x : ZFSet} {y : ZFSet} : x ∈ y → ¬y ∈ x

theorem ZFSet.mem_irrefl (x : ZFSet) : ¬x ∈ x

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

def ZFSet.image (f : ZFSet → ZFSet) [PSet.Definable 1 f] : ZFSet → ZFSet

The image of a (definable) ZFC set function

theorem ZFSet.image.mk (f : ZFSet → ZFSet) [H : PSet.Definable 1 f] (x : ZFSet) {y : ZFSet} : y ∈ x → f y ∈ ZFSet.image f x

@[simp]

theorem ZFSet.mem_image {f : ZFSet → ZFSet} [H : PSet.Definable 1 f] {x : ZFSet} {y : ZFSet} : y ∈ ZFSet.image f x ↔ ∃ z, z ∈ x ∧ f z = y

@[simp]

theorem ZFSet.toSet_image (f : ZFSet → ZFSet) [H : PSet.Definable 1 f] (x : ZFSet) : ZFSet.toSet (ZFSet.image f x) = f '' ZFSet.toSet x

noncomputable def ZFSet.range {α : Type u} (f : α → ZFSet) : ZFSet

The range of an indexed family of sets. The universes allow for a more general index type without manual use of ULift.

@[simp]

theorem ZFSet.mem_range {α : Type u} {f : α → ZFSet} {x : ZFSet} : x ∈ ZFSet.range f ↔ x ∈ Set.range f

@[simp]

theorem ZFSet.toSet_range {α : Type u} (f : α → ZFSet) : ZFSet.toSet (ZFSet.range f) = Set.range f

def ZFSet.pair (x : ZFSet) (y : ZFSet) : ZFSet

Kuratowski ordered pair

@[simp]

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

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

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

@[simp]

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

theorem ZFSet.pair_injective : Function.Injective2 ZFSet.pair

@[simp]

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

def ZFSet.prod : ZFSet → ZFSet → ZFSet

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

@[simp]

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

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

def ZFSet.IsFunc (x : ZFSet) (y : ZFSet) (f : ZFSet) : 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 : ZFSet) (y : ZFSet) : ZFSet

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

@[simp]

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

noncomputable instance ZFSet.mapDefinableAux (f : ZFSet → ZFSet) [PSet.Definable 1 f] : PSet.Definable 1 fun y => ZFSet.pair y (f y)

noncomputable def ZFSet.map (f : ZFSet → ZFSet) [PSet.Definable 1 f] : ZFSet → ZFSet

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 → ZFSet} [PSet.Definable 1 f] {x : ZFSet} {y : ZFSet} : y ∈ ZFSet.map f x ↔ ∃ z, z ∈ x ∧ ZFSet.pair z (f z) = y

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

@[simp]

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

def ZFSet.Hereditarily (p : ZFSet → Prop) (x : ZFSet) : 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.

Equations

• ZFSet.Hereditarily p x = (p x ∧ ∀ (y : ZFSet), y ∈ x → ZFSet.Hereditarily p y)

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

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

Alias of the forward direction of ZFSet.hereditarily_iff.

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

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

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

def Class : Type (u_1 + 1)

The collection of all classes. We define Class as Set ZFSet, as this allows us to get many instances automatically. However, in practice, we treat it as (the definitionally equal) ZFSet → Prop. This means, the preferred way to state that x : ZFSet belongs to A : Class is to write A x.

instance instInsertZFSetClass : Insert ZFSet Class

def Class.sep (p : ZFSet → Prop) (A : Class) : Class

{x ∈ A | p x} is the class of elements in A satisfying p

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

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

def Class.ofSet (x : ZFSet) : Class

Coerce a ZFC set into a class

instance Class.instCoeZFSetClass : Coe ZFSet Class

def Class.univ : Class

The universal class

def Class.ToSet (B : Class) (A : Class) : Prop

Assert that A is a ZFC set satisfying B

def Class.Mem (A : Class) (B : Class) : Prop

A ∈ B if A is a ZFC set which satisfies B

instance Class.instMembershipClassClass : Membership Class Class

theorem Class.mem_def (A : Class) (B : Class) : A ∈ B ↔ ∃ x, ↑x = A ∧ B x

@[simp]

theorem Class.not_mem_empty (x : Class) : ¬x ∈ ∅

@[simp]

theorem Class.not_empty_hom (x : ZFSet) : ¬∅ x

@[simp]

theorem Class.mem_univ {A : Class} : A ∈ Class.univ ↔ ∃ x, ↑x = A

@[simp]

theorem Class.mem_univ_hom (x : ZFSet) : Class.univ x

theorem Class.eq_univ_iff_forall {A : Class} : A = Class.univ ↔ (x : ZFSet) → A x

theorem Class.eq_univ_of_forall {A : Class} : ((x : ZFSet) → A x) → A = Class.univ

theorem Class.mem_wf : WellFounded fun x x_1 => x ∈ x_1

instance Class.instWellFoundedRelationClass : WellFoundedRelation Class

instance Class.instIsAsymmClassMemInstMembershipClassClass : IsAsymm Class fun x x_1 => x ∈ x_1

instance Class.instIsIrreflClassMemInstMembershipClassClass : IsIrrefl Class fun x x_1 => x ∈ x_1

theorem Class.mem_asymm {x : Class} {y : Class} : x ∈ y → ¬y ∈ x

theorem Class.mem_irrefl (x : Class) : ¬x ∈ x

theorem Class.univ_not_mem_univ : ¬Class.univ ∈ Class.univ

There is no universal set. This is stated as univ ∉ univ, meaning that univ (the class of all sets) is proper (does not belong to the class of all sets).

def Class.congToClass (x : Set Class) : Class

Convert a conglomerate (a collection of classes) into a class

@[simp]

theorem Class.congToClass_empty : Class.congToClass ∅ = ∅

def Class.classToCong (x : Class) : Set Class

Convert a class into a conglomerate (a collection of classes)

@[simp]

theorem Class.classToCong_empty : Class.classToCong ∅ = ∅

def Class.powerset (x : Class) : Class

The power class of a class is the class of all subclasses that are ZFC sets

def Class.sUnion (x : Class) : Class

The union of a class is the class of all members of ZFC sets in the class

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

The union of a class is the class of all members of ZFC sets in the class

def Class.sInter (x : Class) : Class

The intersection of a class is the class of all members of ZFC sets in the class

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

The intersection of a class is the class of all members of ZFC sets in the class

theorem Class.ofSet.inj {x : ZFSet} {y : ZFSet} (h : ↑x = ↑y) : x = y

@[simp]

theorem Class.toSet_of_ZFSet (A : Class) (x : ZFSet) : Class.ToSet A ↑x ↔ A x

@[simp]

theorem Class.coe_mem {x : ZFSet} {A : Class} : ↑x ∈ A ↔ A x

@[simp]

theorem Class.coe_apply {x : ZFSet} {y : ZFSet} : ↑y x ↔ x ∈ y

@[simp]

theorem Class.coe_subset (x : ZFSet) (y : ZFSet) : ↑x ⊆ ↑y ↔ x ⊆ y

@[simp]

theorem Class.coe_sep (p : Class) (x : ZFSet) : ↑(ZFSet.sep p x) = {y | y ∈ x ∧ p y}

@[simp]

theorem Class.coe_empty : ↑∅ = ∅

@[simp]

theorem Class.coe_insert (x : ZFSet) (y : ZFSet) : ↑(insert x y) = insert x ↑y

@[simp]

theorem Class.coe_union (x : ZFSet) (y : ZFSet) : ↑(x ∪ y) = ↑x ∪ ↑y

@[simp]

theorem Class.coe_inter (x : ZFSet) (y : ZFSet) : ↑(x ∩ y) = ↑x ∩ ↑y

@[simp]

theorem Class.coe_diff (x : ZFSet) (y : ZFSet) : ↑(x \ y) = ↑x \ ↑y

@[simp]

theorem Class.coe_powerset (x : ZFSet) : ↑(ZFSet.powerset x) = Class.powerset ↑x

@[simp]

theorem Class.powerset_apply {A : Class} {x : ZFSet} : Class.powerset A x ↔ ↑x ⊆ A

@[simp]

theorem Class.sUnion_apply {x : Class} {y : ZFSet} : (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z

@[simp]

theorem Class.coe_sUnion (x : ZFSet) : ↑(⋃₀ x) = ⋃₀ ↑x

@[simp]

theorem Class.mem_sUnion {x : Class} {y : Class} : y ∈ ⋃₀ x ↔ ∃ z, z ∈ x ∧ y ∈ z

theorem Class.sInter_apply {x : Class} {y : ZFSet} : (⋂₀ x) y ↔ ∀ (z : ZFSet), x z → y ∈ z

@[simp]

theorem Class.coe_sInter {x : ZFSet} (h : ZFSet.Nonempty x) : ↑(⋂₀ x) = ⋂₀ ↑x

theorem Class.mem_of_mem_sInter {x : Class} {y : Class} {z : Class} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) : y ∈ z

theorem Class.mem_sInter {x : Class} {y : Class} (h : Set.Nonempty x) : y ∈ ⋂₀ x ↔ ∀ (z : Class), z ∈ x → y ∈ z

@[simp]

theorem Class.sUnion_empty : ⋃₀ ∅ = ∅

@[simp]

theorem Class.sInter_empty : ⋂₀ ∅ = Class.univ

theorem Class.eq_univ_of_powerset_subset {A : Class} (hA : Class.powerset A ⊆ A) : A = Class.univ

An induction principle for sets. If every subset of a class is a member, then the class is universal.

def Class.iota (A : Class) : Class

The definite description operator, which is {x} if {y | A y} = {x} and ∅ otherwise.

theorem Class.iota_val (A : Class) (x : ZFSet) (H : ∀ (y : ZFSet), A y ↔ y = x) : Class.iota A = ↑x

theorem Class.iota_ex (A : Class) : Class.iota A ∈ Class.univ

Unlike the other set constructors, the iota definite descriptor is a set for any set input, but not constructively so, so there is no associated Class → Set function.

def Class.fval (F : Class) (A : Class) : Class

Function value

def Class.«term_′_» : Lean.TrailingParserDescr

Function value

theorem Class.fval_ex (F : Class) (A : Class) : F ′ A ∈ Class.univ

@[simp]

theorem ZFSet.map_fval {f : ZFSet → ZFSet} [H : PSet.Definable 1 f] {x : ZFSet} {y : ZFSet} (h : y ∈ x) : ↑(ZFSet.map f x) ′ ↑y = ↑(f y)

noncomputable def ZFSet.choice (x : ZFSet) : ZFSet

A choice function on the class of nonempty ZFC sets.

theorem ZFSet.choice_mem_aux (x : ZFSet) (h : ¬∅ ∈ x) (y : ZFSet) (yx : y ∈ x) : (Classical.epsilon fun z => z ∈ y) ∈ y

theorem ZFSet.choice_isFunc (x : ZFSet) (h : ¬∅ ∈ x) : ZFSet.IsFunc x (⋃₀ x) (ZFSet.choice x)

theorem ZFSet.choice_mem (x : ZFSet) (h : ¬∅ ∈ x) (y : ZFSet) (yx : y ∈ x) : ↑(ZFSet.choice x) ′ ↑y ∈ ↑y

@[simp]

theorem ZFSet.toSet_equiv_apply_coe (x : ZFSet) : ↑(↑ZFSet.toSet_equiv x) = ZFSet.toSet x

noncomputable def ZFSet.toSet_equiv : ZFSet ≃ { s // Small.{u, u + 1} ↑s }

ZFSet.toSet as an equivalence.