# 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 #

• 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 ZFSet.mapDefinableAux computably.

inductive PSet :
Type (u + 1)

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.

Instances For
def PSet.Type :
PSetType u

The underlying type of a pre-set

Equations
• x.Type = match x with | PSet.mk α A => α
Instances For
def PSet.Func (x : PSet) :
x.TypePSet

The underlying pre-set family of a pre-set

Equations
• x.Func = match (motive := (x : PSet) → x.TypePSet) x with | PSet.mk α A => A
Instances For
@[simp]
theorem PSet.mk_type (α : Type u_1) (A : αPSet) :
(PSet.mk α A).Type = α
@[simp]
theorem PSet.mk_func (α : Type u_1) (A : αPSet) :
(PSet.mk α A).Func = A
@[simp]
theorem PSet.eta (x : PSet) :
PSet.mk x.Type x.Func = x
def PSet.Equiv :
PSet

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.mk α A).Equiv (PSet.mk α_1 B) = ((∀ (a : α), ∃ (b : α_1), (A a).Equiv (B b)) ∀ (b : α_1), ∃ (a : α), (A a).Equiv (B b))
Instances For
theorem PSet.equiv_iff {x : PSet} {y : PSet} :
x.Equiv y (∀ (i : x.Type), ∃ (j : y.Type), (x.Func i).Equiv (y.Func j)) ∀ (j : y.Type), ∃ (i : x.Type), (x.Func i).Equiv (y.Func j)
theorem PSet.Equiv.exists_left {x : PSet} {y : PSet} (h : x.Equiv y) (i : x.Type) :
∃ (j : y.Type), (x.Func i).Equiv (y.Func j)
theorem PSet.Equiv.exists_right {x : PSet} {y : PSet} (h : x.Equiv y) (j : y.Type) :
∃ (i : x.Type), (x.Func i).Equiv (y.Func j)
theorem PSet.Equiv.refl (x : PSet) :
x.Equiv x
theorem PSet.Equiv.rfl {x : PSet} :
x.Equiv x
theorem PSet.Equiv.euc {x : PSet} {y : PSet} {z : PSet} :
x.Equiv yz.Equiv yx.Equiv z
theorem PSet.Equiv.symm {x : PSet} {y : PSet} :
x.Equiv yy.Equiv x
theorem PSet.Equiv.comm {x : PSet} {y : PSet} :
x.Equiv y y.Equiv x
theorem PSet.Equiv.trans {x : PSet} {y : PSet} {z : PSet} (h1 : x.Equiv y) (h2 : y.Equiv z) :
x.Equiv z
theorem PSet.equiv_of_isEmpty (x : PSet) (y : PSet) [IsEmpty x.Type] [IsEmpty y.Type] :
x.Equiv y
instance PSet.setoid :
Equations
def PSet.Subset (x : PSet) (y : PSet) :

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.

Equations
• x.Subset y = ∀ (a : x.Type), ∃ (b : y.Type), (x.Func a).Equiv (y.Func b)
Instances For
Equations
instance PSet.instIsReflSubset :
IsRefl PSet fun (x x_1 : PSet) => x x_1
Equations
instance PSet.instIsTransSubset :
IsTrans PSet fun (x x_1 : PSet) => x x_1
Equations
theorem PSet.Equiv.ext (x : PSet) (y : PSet) :
x.Equiv y x y y x
theorem PSet.Subset.congr_left {x : PSet} {y : PSet} {z : PSet} :
x.Equiv y(x z y z)
theorem PSet.Subset.congr_right {x : PSet} {y : PSet} {z : PSet} :
x.Equiv y(z x z y)
def PSet.Mem (x : PSet) (y : PSet) :

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

Equations
• x.Mem y = ∃ (b : y.Type), x.Equiv (y.Func b)
Instances For
theorem PSet.Mem.mk {α : Type u} (A : αPSet) (a : α) :
A a PSet.mk α A
theorem PSet.func_mem (x : PSet) (i : x.Type) :
x.Func i x
theorem PSet.Mem.ext {x : PSet} {y : PSet} :
(∀ (w : PSet), w x w y)x.Equiv y
theorem PSet.Mem.congr_right {x : PSet} {y : PSet} :
x.Equiv y∀ {w : PSet}, w x w y
theorem PSet.equiv_iff_mem {x : PSet} {y : PSet} :
x.Equiv y ∀ {w : PSet}, w x w y
theorem PSet.Mem.congr_left {x : PSet} {y : PSet} :
x.Equiv y∀ {w : PSet}, x w y w
theorem PSet.mem_wf :
WellFounded fun (x x_1 : PSet) => x x_1
Equations
instance PSet.instIsAsymmMem :
IsAsymm PSet fun (x x_1 : PSet) => x x_1
Equations
instance PSet.instIsIrreflMem :
IsIrrefl PSet fun (x x_1 : PSet) => x x_1
Equations
theorem PSet.mem_asymm {x : PSet} {y : PSet} :
x yyx
theorem PSet.mem_irrefl (x : PSet) :
xx
def PSet.toSet (u : PSet) :

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

Equations
Instances For
@[simp]
theorem PSet.mem_toSet (a : PSet) (u : PSet) :
a u.toSet a u

A nonempty set is one that contains some element.

Equations
• u.Nonempty = u.toSet.Nonempty
Instances For
theorem PSet.nonempty_def (u : PSet) :
u.Nonempty ∃ (x : PSet), x u
theorem PSet.nonempty_of_mem {x : PSet} {u : PSet} (h : x u) :
u.Nonempty
@[simp]
theorem PSet.nonempty_toSet_iff {u : PSet} :
u.toSet.Nonempty u.Nonempty
theorem PSet.nonempty_type_iff_nonempty {x : PSet} :
Nonempty x.Type x.Nonempty
theorem PSet.nonempty_of_nonempty_type (x : PSet) [h : Nonempty x.Type] :
x.Nonempty
theorem PSet.Equiv.eq {x : PSet} {y : PSet} :
x.Equiv y x.toSet = y.toSet

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

instance PSet.instCoeSet :
Equations

The empty pre-set

Equations
Instances For
Equations
Equations
@[simp]
theorem PSet.not_mem_empty (x : PSet) :
x
@[simp]
theorem PSet.toSet_empty :
.toSet =
@[simp]
theorem PSet.empty_subset (x : PSet) :
@[simp]
theorem PSet.not_nonempty_empty :
¬.Nonempty
theorem PSet.equiv_empty (x : PSet) [IsEmpty x.Type] :
x.Equiv
def PSet.insert (x : PSet) (y : PSet) :

Insert an element into a pre-set

Equations
Instances For
instance PSet.instInsert :
Equations
Equations
Equations
instance PSet.instInhabitedTypeInsert (x : PSet) (y : PSet) :
Inhabited (insert x y).Type
Equations

The n-th von Neumann ordinal

Equations
Instances For

The von Neumann ordinal ω

Equations
Instances For
def PSet.sep (p : ) (x : PSet) :

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

Equations
• PSet.sep p x = PSet.mk { a : x.Type // p (x.Func a) } fun (y : { a : x.Type // p (x.Func a) }) => x.Func y
Instances For
instance PSet.instSep :
Equations

The pre-set powerset operator

Equations
• x.powerset = PSet.mk (Set x.Type) fun (p : Set x.Type) => PSet.mk { a : x.Type // p a } fun (y : { a : x.Type // p a }) => x.Func y
Instances For
@[simp]
theorem PSet.mem_powerset {x : PSet} {y : PSet} :
y x.powerset y x
def PSet.sUnion (a : PSet) :

The pre-set union operator

Equations
• ⋃₀ a = PSet.mk ((x : a.Type) × (a.Func x).Type) fun (x : (x : a.Type) × (a.Func x).Type) => match x with | x, y => (a.Func x).Func y
Instances For

The pre-set union operator

Equations
Instances For
@[simp]
theorem PSet.mem_sUnion {x : PSet} {y : PSet} :
y ⋃₀ x zx, y z
@[simp]
theorem PSet.toSet_sUnion (x : PSet) :
(⋃₀ x).toSet = ⋃₀ (PSet.toSet '' x.toSet)
def PSet.image (f : ) (x : PSet) :

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

Equations
Instances For
theorem PSet.mem_image {f : } (H : ∀ (x y : PSet), x.Equiv y(f x).Equiv (f y)) {x : PSet} {y : PSet} :
y zx, y.Equiv (f z)
def PSet.Lift :

Universe lift operation

Equations
• (PSet.mk α A).Lift = PSet.mk () fun (x : ) => match x with | { down := x } => (A x).Lift
Instances For

Embedding of one universe in another

Equations
Instances For
def PSet.Arity.Equiv {n : } :

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
Instances For
theorem PSet.Arity.equiv_const {a : PSet} (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.

Equations
• = { x : // }
Instances For
instance PSet.Resp.inhabited {n : } :
Equations
def PSet.Resp.f {n : } (f : PSet.Resp (n + 1)) (x : PSet) :

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

Equations
• f.f x = f x,
Instances For
def PSet.Resp.Equiv {n : } (a : ) (b : ) :

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

Equations
Instances For
theorem PSet.Resp.Equiv.refl {n : } (a : ) :
a.Equiv a
theorem PSet.Resp.Equiv.euc {n : } {a : } {b : } {c : } :
a.Equiv bc.Equiv ba.Equiv c
theorem PSet.Resp.Equiv.symm {n : } {a : } {b : } :
a.Equiv bb.Equiv a
theorem PSet.Resp.Equiv.trans {n : } {x : } {y : } {z : } (h1 : x.Equiv y) (h2 : y.Equiv z) :
x.Equiv z
instance PSet.Resp.setoid {n : } :
Equations
• PSet.Resp.setoid = { r := PSet.Resp.Equiv, iseqv := }
def ZFSet :
Type (u + 1)

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

Equations
Instances For
def PSet.Resp.evalAux {n : } :
{ f : // ∀ (a b : ), a.Equiv bf a = f b }

Helper function for PSet.eval.

Equations
Instances For
def PSet.Resp.eval (n : ) :

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

Equations
• = PSet.Resp.evalAux
Instances For
theorem PSet.Resp.eval_val {n : } {f : PSet.Resp (n + 1)} {x : PSet} :
PSet.Resp.eval (n + 1) f x = PSet.Resp.eval n (f.f x)
class inductive PSet.Definable (n : ) :
Type (u + 1)

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.

Instances
def PSet.Definable.EqMk {n : } (f : ) {s : } :
= s

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

Equations
• = match x✝, x with | .(), =>
Instances For
def PSet.Definable.Resp {n : } (s : ) [] :

Turns a definable function into a function that respects equivalence.

Equations
• = match x✝, x with | .(), => f
Instances For
theorem PSet.Definable.eq {n : } (s : ) [H : ] :
noncomputable def Classical.allDefinable {n : } (F : ) :

All functions are classically definable.

Equations
Instances For
def ZFSet.mk :

Turns a pre-set into a ZFC set.

Equations
Instances For
@[simp]
theorem ZFSet.mk_eq (x : PSet) :
x =
@[simp]
theorem ZFSet.mk_out (x : ZFSet) :
= x
theorem ZFSet.eq {x : PSet} {y : PSet} :
x.Equiv y
theorem ZFSet.sound {x : PSet} {y : PSet} (h : x.Equiv y) :
theorem ZFSet.exact {x : PSet} {y : PSet} :
x.Equiv y
@[simp]
theorem ZFSet.eval_mk {n : } {f : PSet.Resp (n + 1)} {x : PSet} :
PSet.Resp.eval (n + 1) f () = PSet.Resp.eval n (f.f x)
def ZFSet.Mem :

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

Equations
Instances For
@[simp]
theorem ZFSet.mk_mem_iff {x : PSet} {y : PSet} :
x y
def ZFSet.toSet (u : ZFSet) :

Convert a ZFC set into a Set of ZFC sets

Equations
Instances For
@[simp]
theorem ZFSet.mem_toSet (a : ZFSet) (u : ZFSet) :
a u.toSet a u
instance ZFSet.small_toSet (x : ZFSet) :
Small.{u, u + 1} x.toSet
Equations
• =

A nonempty set is one that contains some element.

Equations
• u.Nonempty = u.toSet.Nonempty
Instances For
theorem ZFSet.nonempty_def (u : ZFSet) :
u.Nonempty ∃ (x : ZFSet), x u
theorem ZFSet.nonempty_of_mem {x : ZFSet} {u : ZFSet} (h : x u) :
u.Nonempty
@[simp]
theorem ZFSet.nonempty_toSet_iff {u : ZFSet} :
u.toSet.Nonempty u.Nonempty
def ZFSet.Subset (x : ZFSet) (y : ZFSet) :

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

Equations
Instances For
instance ZFSet.hasSubset :
Equations
theorem ZFSet.subset_def {x : ZFSet} {y : ZFSet} :
x y ∀ ⦃z : ZFSet⦄, z xz y
instance ZFSet.instIsReflSubset :
IsRefl ZFSet fun (x x_1 : ZFSet) => x x_1
Equations
instance ZFSet.instIsTransSubset :
IsTrans ZFSet fun (x x_1 : ZFSet) => x x_1
Equations
@[simp]
theorem ZFSet.subset_iff {x : PSet} {y : PSet} :
x y
@[simp]
theorem ZFSet.toSet_subset_iff {x : ZFSet} {y : ZFSet} :
x.toSet y.toSet 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
@[simp]
theorem ZFSet.toSet_inj {x : ZFSet} {y : ZFSet} :
x.toSet = y.toSet x = y
instance ZFSet.instIsAntisymmSubset :
IsAntisymm ZFSet fun (x x_1 : ZFSet) => x x_1
Equations

The empty ZFC set

Equations
Instances For
Equations
Equations
@[simp]
theorem ZFSet.not_mem_empty (x : ZFSet) :
x
@[simp]
theorem ZFSet.toSet_empty :
.toSet =
@[simp]
theorem ZFSet.empty_subset (x : ZFSet) :
@[simp]
@[simp]
theorem ZFSet.nonempty_mk_iff {x : PSet} :
().Nonempty x.Nonempty
theorem ZFSet.eq_empty (x : ZFSet) :
x = ∀ (y : ZFSet), yx
theorem ZFSet.eq_empty_or_nonempty (u : ZFSet) :
u = u.Nonempty

Insert x y is the set {x} ∪ y

Equations
Instances For
instance ZFSet.instInsert :
Equations
Equations
Equations
@[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) :
(insert x y).toSet = insert x y.toSet
@[simp]
theorem ZFSet.mem_singleton {x : ZFSet} {y : ZFSet} :
x {y} x = y
@[simp]
theorem ZFSet.toSet_singleton (x : ZFSet) :
{x}.toSet = {x}
theorem ZFSet.insert_nonempty (u : ZFSet) (v : ZFSet) :
(insert u v).Nonempty
theorem ZFSet.singleton_nonempty (u : ZFSet) :
{u}.Nonempty
theorem ZFSet.mem_pair {x : ZFSet} {y : ZFSet} {z : ZFSet} :
x {y, z} x = y x = z

omega is the first infinite von Neumann ordinal

Equations
Instances For
@[simp]
@[simp]
theorem ZFSet.omega_succ {n : ZFSet} :
def ZFSet.sep (p : ) :

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

Equations
Instances For
instance ZFSet.instSep :
Equations
@[simp]
theorem ZFSet.mem_sep {p : } {x : ZFSet} {y : ZFSet} :
y y x p y
@[simp]
theorem ZFSet.toSet_sep (a : ZFSet) (p : ) :
().toSet = {x : ZFSet | x a.toSet p x}

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

Equations
Instances For
@[simp]
theorem ZFSet.mem_powerset {x : ZFSet} {y : ZFSet} :
y x.powerset y x
theorem ZFSet.sUnion_lem {α : Type u} {β : Type u} (A : αPSet) (B : βPSet) (αβ : ∀ (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)

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

Equations
Instances For

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

Equations
Instances For
noncomputable def ZFSet.sInter (x : ZFSet) :

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

Equations
Instances For

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

Equations
Instances For
@[simp]
theorem ZFSet.mem_sUnion {x : ZFSet} {y : ZFSet} :
y ⋃₀ x zx, y z
theorem ZFSet.mem_sInter {x : ZFSet} {y : ZFSet} (h : x.Nonempty) :
y ⋂₀ x zx, y z
@[simp]
@[simp]
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) :
theorem ZFSet.not_mem_sInter_of_not_mem {x : ZFSet} {y : ZFSet} {z : ZFSet} (hy : yz) (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) :
(⋃₀ x).toSet = ⋃₀ (ZFSet.toSet '' x.toSet)
theorem ZFSet.toSet_sInter {x : ZFSet} (h : x.Nonempty) :
(⋂₀ x).toSet = ⋂₀ (ZFSet.toSet '' x.toSet)
@[simp]
theorem ZFSet.singleton_inj {x : ZFSet} {y : ZFSet} :
{x} = {y} x = y
def ZFSet.union (x : ZFSet) (y : ZFSet) :

The binary union operation

Equations
Instances For
def ZFSet.inter (x : ZFSet) (y : ZFSet) :

The binary intersection operation

Equations
Instances For
def ZFSet.diff (x : ZFSet) (y : ZFSet) :

The set difference operation

Equations
Instances For
instance ZFSet.instUnion :
Equations
instance ZFSet.instInter :
Equations
instance ZFSet.instSDiff :
Equations
@[simp]
theorem ZFSet.toSet_union (x : ZFSet) (y : ZFSet) :
(x y).toSet = x.toSet y.toSet
@[simp]
theorem ZFSet.toSet_inter (x : ZFSet) (y : ZFSet) :
(x y).toSet = x.toSet y.toSet
@[simp]
theorem ZFSet.toSet_sdiff (x : ZFSet) (y : ZFSet) :
(x \ y).toSet = x.toSet \ y.toSet
@[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 zy
@[simp]
theorem ZFSet.sUnion_pair {x : ZFSet} {y : ZFSet} :
⋃₀ {x, y} = x y
theorem ZFSet.mem_wf :
WellFounded fun (x x_1 : ZFSet) => x x_1
theorem ZFSet.inductionOn {p : } (x : ZFSet) (h : ∀ (x : ZFSet), (yx, p y)p x) :
p x

Induction on the ∈ relation.

Equations
instance ZFSet.instIsAsymmMem :
IsAsymm ZFSet fun (x x_1 : ZFSet) => x x_1
Equations
instance ZFSet.instIsIrreflMem :
IsIrrefl ZFSet fun (x x_1 : ZFSet) => x x_1
Equations
theorem ZFSet.mem_asymm {x : ZFSet} {y : ZFSet} :
x yyx
theorem ZFSet.mem_irrefl (x : ZFSet) :
xx
theorem ZFSet.regularity (x : ZFSet) (h : x ) :
yx, x y =
def ZFSet.image (f : ) [] :

The image of a (definable) ZFC set function

Equations
• = match (motive := ) with | r, hr => PSet.Resp.eval 1 ⟨,
Instances For
theorem ZFSet.image.mk (f : ) [H : ] (x : ZFSet) {y : ZFSet} :
y xf y
@[simp]
theorem ZFSet.mem_image {f : } [H : ] {x : ZFSet} {y : ZFSet} :
y zx, f z = y
@[simp]
theorem ZFSet.toSet_image (f : ) [H : ] (x : ZFSet) :
().toSet = f '' x.toSet
noncomputable def ZFSet.range {α : Type u} (f : αZFSet) :

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

Equations
Instances For
@[simp]
theorem ZFSet.mem_range {α : Type u} {f : αZFSet} {x : ZFSet} :
x x
@[simp]
theorem ZFSet.toSet_range {α : Type u} (f : αZFSet) :
().toSet =
def ZFSet.pair (x : ZFSet) (y : ZFSet) :

Kuratowski ordered pair

Equations
• x.pair y = {{x}, {x, y}}
Instances For
@[simp]
theorem ZFSet.toSet_pair (x : ZFSet) (y : ZFSet) :
(x.pair y).toSet = {{x}, {x, y}}
def ZFSet.pairSep (p : ) (x : ZFSet) (y : ZFSet) :

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

Equations
• = ZFSet.sep (fun (z : ZFSet) => ax, by, z = a.pair b p a b) (x y).powerset.powerset
Instances For
@[simp]
theorem ZFSet.mem_pairSep {p : } {x : ZFSet} {y : ZFSet} {z : ZFSet} :
z ax, by, z = a.pair b p a b
@[simp]
theorem ZFSet.pair_inj {x : ZFSet} {y : ZFSet} {x' : ZFSet} {y' : ZFSet} :
x.pair y = x'.pair y' x = x' y = y'

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

Equations
Instances For
@[simp]
theorem ZFSet.mem_prod {x : ZFSet} {y : ZFSet} {z : ZFSet} :
z x.prod y ax, by, z = a.pair b
theorem ZFSet.pair_mem_prod {x : ZFSet} {y : ZFSet} {a : ZFSet} {b : ZFSet} :
a.pair b x.prod y a x b y
def ZFSet.IsFunc (x : ZFSet) (y : ZFSet) (f : ZFSet) :

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.

Equations
• x.IsFunc y f = (f x.prod y zx, ∃! w : ZFSet, z.pair w f)
Instances For
def ZFSet.funs (x : ZFSet) (y : ZFSet) :

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

Equations
• x.funs y = ZFSet.sep (x.IsFunc y) (x.prod y).powerset
Instances For
@[simp]
theorem ZFSet.mem_funs {x : ZFSet} {y : ZFSet} {f : ZFSet} :
f x.funs y x.IsFunc y f
noncomputable instance ZFSet.mapDefinableAux (f : ) [] :
PSet.Definable 1 fun (y : ZFSet) => y.pair (f y)
Equations
noncomputable def ZFSet.map (f : ) [] :

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

Equations
Instances For
@[simp]
theorem ZFSet.mem_map {f : } [] {x : ZFSet} {y : ZFSet} :
y zx, z.pair (f z) = y
theorem ZFSet.map_unique {f : } [H : ] {x : ZFSet} {z : ZFSet} (zx : z x) :
∃! w : ZFSet, z.pair w
@[simp]
theorem ZFSet.map_isFunc {f : } [] {x : ZFSet} {y : ZFSet} :
x.IsFunc y () zx, f z y
@[irreducible]
def ZFSet.Hereditarily (p : ) (x : ZFSet) :

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
• = (p x yx, )
Instances For
theorem ZFSet.hereditarily_iff {p : } {x : ZFSet} :
p x yx,
theorem ZFSet.Hereditarily.def {p : } {x : ZFSet} :
p x yx,

Alias of the forward direction of ZFSet.hereditarily_iff.

theorem ZFSet.Hereditarily.self {p : } {x : ZFSet} (h : ) :
p x
theorem ZFSet.Hereditarily.mem {p : } {x : ZFSet} {y : ZFSet} (h : ) (hy : y x) :
theorem ZFSet.Hereditarily.empty {p : } {x : ZFSet} :
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.

Equations
Instances For
Equations
def Class.sep (p : ) (A : Class) :

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

Equations
Instances For
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

Coerce a ZFC set into a class

Equations
Instances For

The universal class

Equations
Instances For
def Class.ToSet (B : Class) (A : Class) :

Assert that A is a ZFC set satisfying B

Equations
Instances For
def Class.Mem (A : Class) (B : Class) :

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

Equations
• A.Mem B = B.ToSet A
Instances For
theorem Class.mem_def (A : Class) (B : Class) :
A B ∃ (x : ZFSet), x = A B x
@[simp]
theorem Class.not_mem_empty (x : Class) :
x
@[simp]
@[simp]
theorem Class.mem_univ {A : Class} :
∃ (x : ZFSet), x = A
@[simp]
theorem Class.mem_univ_hom (x : ZFSet) :
theorem Class.eq_univ_iff_forall {A : Class} :
∀ (x : ZFSet), A x
theorem Class.eq_univ_of_forall {A : Class} :
(∀ (x : ZFSet), A x)
theorem Class.mem_wf :
WellFounded fun (x x_1 : Class) => x x_1
Equations
instance Class.instIsAsymmMem :
IsAsymm Class fun (x x_1 : Class) => x x_1
Equations
instance Class.instIsIrreflMem :
IsIrrefl Class fun (x x_1 : Class) => x x_1
Equations
theorem Class.mem_asymm {x : Class} {y : Class} :
x yyx
theorem Class.mem_irrefl (x : Class) :
xx

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

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

Equations
Instances For

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

Equations
Instances For
@[simp]
theorem Class.classToCong_empty :
.classToCong =

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

Equations
• x.powerset =
Instances For

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

Equations
Instances For

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

Equations
Instances For

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

Equations
Instances For

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

Equations
Instances For
theorem Class.ofSet.inj {x : ZFSet} {y : ZFSet} (h : x = y) :
x = y
@[simp]
theorem Class.toSet_of_ZFSet (A : Class) (x : ZFSet) :
A.ToSet 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) :
() = {y : ZFSet | 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) :
x.powerset = (x).powerset
@[simp]
theorem Class.powerset_apply {A : Class} {x : ZFSet} :
A.powerset x x A
@[simp]
theorem Class.sUnion_apply {x : Class} {y : ZFSet} :
(⋃₀ x) y ∃ (z : ZFSet), x z y z
@[simp]
theorem Class.coe_sUnion (x : ZFSet) :
(⋃₀ x) = ⋃₀ x
@[simp]
theorem Class.mem_sUnion {x : Class} {y : Class} :
y ⋃₀ x zx, y z
theorem Class.sInter_apply {x : Class} {y : ZFSet} :
(⋂₀ x) y ∀ (z : ZFSet), x zy z
@[simp]
theorem Class.coe_sInter {x : ZFSet} (h : x.Nonempty) :
(⋂₀ 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 : ) :
y ⋂₀ x zx, y z
@[simp]
@[simp]
theorem Class.eq_univ_of_powerset_subset {A : Class} (hA : A.powerset A) :

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

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

Equations
Instances For
theorem Class.iota_val (A : Class) (x : ZFSet) (H : ∀ (y : ZFSet), A y y = x) :
A.iota = x
theorem Class.iota_ex (A : Class) :

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) :

Function value

Equations
Instances For

Function value

Equations
Instances For
theorem Class.fval_ex (F : Class) (A : Class) :
@[simp]
theorem ZFSet.map_fval {f : } [H : ] {x : ZFSet} {y : ZFSet} (h : y x) :
() y = (f y)
noncomputable def ZFSet.choice (x : ZFSet) :

A choice function on the class of nonempty ZFC sets.

Equations
Instances For
theorem ZFSet.choice_mem_aux (x : ZFSet) (h : x) (y : ZFSet) (yx : y x) :
(Classical.epsilon fun (z : ZFSet) => z y) y
theorem ZFSet.choice_isFunc (x : ZFSet) (h : x) :
x.IsFunc (⋃₀ x) x.choice
theorem ZFSet.choice_mem (x : ZFSet) (h : x) (y : ZFSet) (yx : y x) :
x.choice y y
@[simp]
theorem ZFSet.toSet_equiv_apply_coe (x : ZFSet) :
(ZFSet.toSet_equiv x) = x.toSet
noncomputable def ZFSet.toSet_equiv :
ZFSet { s : // }

ZFSet.toSet as an equivalence.

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