ZFC classes

Classes in set theory are usually defined as collections of elements satisfying some property. Here, however, we define Class as Set ZFSet to derive many instances automatically, most of them being the lifting of set operations to classes. The usual definition is then definitionally equal to ours.

Main definitions

• Class: Defined as Set ZFSet.
• Class.iota: Definite description operator.
• ZFSet.isOrdinal_notMem_univ: The Burali-Forti paradox. Ordinals form a proper class.

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 instHasSubsetClass : HasSubset Class.{u_1}

instance instEmptyCollectionClass : EmptyCollection Class.{u_1}

instance instNonemptyClass : Nonempty Class.{u_1}

instance instUnionClass : Union Class.{u_1}

instance instInterClass : Inter Class.{u_1}

instance instComplClass : Compl Class.{u_1}

instance instSDiffClass : SDiff Class.{u_1}

instance instInsertZFSetClass : Insert ZFSet.{u_1} Class.{u_1}

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

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

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

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

def Class.ofSet (x : ZFSet.{u}) : Class.{u}

Coerce a ZFC set into a class

instance Class.instCoeZFSet : Coe ZFSet.{u_1} Class.{u_1}

def Class.univ : Class.{u_1}

The universal class

def Class.ToSet (B A : Class.{u}) : Prop

Assert that A is a ZFC set satisfying B

def Class.Mem (B A : Class.{u}) : Prop

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

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

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

@[simp]

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

@[simp]

theorem Class.not_empty_hom (x : ZFSet.{u}) : ¬∅ x

@[simp]

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

@[simp]

theorem Class.mem_univ_hom (x : ZFSet.{u}) : univ x

theorem Class.eq_univ_iff_forall {A : Class.{u}} : A = univ ↔ ∀ (x : ZFSet.{u}), A x

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

theorem Class.mem_wf : WellFounded fun (x1 x2 : Class.{u}) => x1 ∈ x2

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

instance Class.instWellFoundedRelation : WellFoundedRelation Class.{u_1}

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

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

theorem Class.univ_notMem_univ : univ ∉ 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.{u}) : Class.{u}

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

@[simp]

theorem Class.congToClass_empty : congToClass ∅ = ∅

def Class.classToCong (x : Class.{u}) : Set Class.{u}

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

@[simp]

theorem Class.classToCong_empty : ∅.classToCong = ∅

def Class.powerset (x : Class.{u_1}) : Class.{u_1}

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

def Class.sUnion (x : Class.{u_1}) : Class.{u_1}

The union of a class is the class of all members of ZFC sets in the class. Uses ⋃₀ notation, scoped under the Class namespace.

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

The union of a class is the class of all members of ZFC sets in the class. Uses ⋃₀ notation, scoped under the Class namespace.

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

The intersection of a class is the class of all members of ZFC sets in the class . Uses ⋂₀ notation, scoped under the Class namespace.

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

The intersection of a class is the class of all members of ZFC sets in the class . Uses ⋂₀ notation, scoped under the Class namespace.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Class.coe_empty : ↑∅ = ∅

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Class.coe_sUnion (x : ZFSet.{u}) : ↑x.sUnion = (↑x).sUnion

@[simp]

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

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

@[simp]

theorem Class.coe_sInter {x : ZFSet.{u}} (h : x.Nonempty) : ↑x.sInter = (↑x).sInter

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

theorem Class.mem_sInter {x y : Class.{u}} (h : Set.Nonempty x) : y ∈ x.sInter ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem Class.sUnion_empty : ∅.sUnion = ∅

@[simp]

theorem Class.sInter_empty : ∅.sInter = univ

theorem Class.eq_univ_of_powerset_subset {A : Class.{u_1}} (hA : A.powerset ⊆ A) : A = 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.{u_1}) : Class.{u_1}

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

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

theorem Class.iota_ex (A : Class.{u}) : A.iota ∈ 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 A : Class.{u}) : Class.{u}

Function value

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

Function value

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

@[simp]

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

noncomputable def ZFSet.choice (x : ZFSet.{u}) : ZFSet.{u}

A choice function on the class of nonempty ZFC sets.

theorem ZFSet.choice_mem_aux (x : ZFSet.{u}) (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) : (Classical.epsilon fun (z : ZFSet.{u}) => z ∈ y) ∈ y

theorem ZFSet.choice_isFunc (x : ZFSet.{u}) (h : ∅ ∉ x) : x.IsFunc x.sUnion x.choice

theorem ZFSet.choice_mem (x : ZFSet.{u}) (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) : ↑x.choice ′ ↑y ∈ ↑y

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

SetLike.coe as an equivalence.

@[simp]

theorem ZFSet.coeEquiv_apply_coe (x : ZFSet.{u}) : ↑(coeEquiv x) = ↑x

@[deprecated ZFSet.coeEquiv (since := "2025-11-05")]

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

Alias of ZFSet.coeEquiv.

---

SetLike.coe as an equivalence.

theorem ZFSet.isOrdinal_notMem_univ : IsOrdinal ∉ Class.univ

The Burali-Forti paradox: ordinals form a proper class.