ZFC classes

Classes in set theory are usually defined as collections of elements satisfying some property. We model this by defining ZFClass as Set ZFSet.

Main definitions

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

@[reducible, inline]

abbrev ZFClass : Type (u_1 + 1)

The collection of all classes.

Equations

• ZFClass.{?u.1} = Set ZFSet.{?u.1}

def ZFClass.CMem (A B : ZFClass.{u}) : Prop

Membership of classes. A ᶜ∈ B if A is a ZFC set which satisfies B.

Note that the A ∈ B notation is already taken for the case where A : ZFSet instead (the OutParam in Mem forces the type of A to be uniquely inferrable from the type of B).

Equations

• A.CMem B = ∃ (x : ZFSet.{?u.1}), ↑x = A ∧ x ∈ B

def ZFClass.«term_ᶜ∈_» : Lean.TrailingParserDescr

Membership of classes. A ᶜ∈ B if A is a ZFC set which satisfies B.

Note that the A ∈ B notation is already taken for the case where A : ZFSet instead (the OutParam in Mem forces the type of A to be uniquely inferrable from the type of B).

Equations

• ZFClass.«term_ᶜ∈_» = Lean.ParserDescr.trailingNode `ZFClass.«term_ᶜ∈_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᶜ∈ ") (Lean.ParserDescr.cat `term 50))

def ZFClass.«term_ᶜ∉_» : Lean.TrailingParserDescr

Negated membership of classes, see ZFClass.CMem.

Conventions for notations in identifiers:

• The recommended spelling of ᶜ∉ in identifiers is notCMem.

Equations

• ZFClass.«term_ᶜ∉_» = Lean.ParserDescr.trailingNode `ZFClass.«term_ᶜ∉_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᶜ∉ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem ZFClass.coe_cmem {A : ZFClass.{u}} {x : ZFSet.{u}} : ZFClass.CMem (↑x) A ↔ x ∈ A

@[simp]

theorem ZFClass.notCMem_empty {A : ZFClass.{u}} : ¬A.CMem ∅

@[simp]

theorem ZFClass.cmem_univ {A : ZFClass.{u}} : A.CMem Set.univ ↔ ∃ (x : ZFSet.{u}), ↑x = A

instance ZFClass.wellFounded_cmem : WellFounded fun (x1 x2 : ZFClass.{u_1}) => x1.CMem x2

@[instance_reducible]

instance ZFClass.instWellFoundedRelation : WellFoundedRelation ZFClass.{u_1}

Equations

• ZFClass.instWellFoundedRelation = { rel := fun (x1 x2 : ZFClass.{?u.1}) => x1.CMem x2, wf := ZFClass.instWellFoundedRelation._proof_1 }

theorem ZFClass.cmem_asymm {A B : ZFClass.{u}} : A.CMem B → ¬B.CMem A

theorem ZFClass.cmem_irrefl {A : ZFClass.{u}} : ¬A.CMem A

theorem ZFClass.univ_notCMem_univ : ¬ZFClass.CMem Set.univ Set.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 ZFClass.congToClass (x : Set ZFClass.{u}) : ZFClass.{u}

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

Equations

• ZFClass.congToClass x = SetLike.coe ⁻¹' x

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

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

Equations

• x.classToCong = {y : ZFClass.{?u.1} | y.CMem x}

@[simp]

theorem ZFClass.congToClass_empty : congToClass ∅ = ∅

@[simp]

theorem ZFClass.classToCong_empty : ∅.classToCong = ∅

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

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

Equations

• x.powerset = ZFClass.congToClass (𝒫 x)

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

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

Equations

• x.sUnion = sSup x.classToCong

def ZFClass.«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 ZFClass namespace.

Equations

• ZFClass.«term⋃₀_» = Lean.ParserDescr.node `ZFClass.«term⋃₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

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

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

Equations

• x.sInter = sInf x.classToCong

def ZFClass.«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 ZFClass namespace.

Equations

• ZFClass.«term⋂₀_» = Lean.ParserDescr.node `ZFClass.«term⋂₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

theorem ZFClass.coe_subset {x y : ZFSet.{u}} : ↑x ⊆ ↑y ↔ x ⊆ y

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

theorem ZFClass.coe_empty : ↑∅ = ∅

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

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

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

theorem ZFClass.coe_sdiff (x y : ZFSet.{u}) : ↑(x \ y) = ↑x \ ↑y

@[simp]

theorem ZFClass.mem_powerset {A : ZFClass.{u}} {x : ZFSet.{u}} : x ∈ A.powerset ↔ ↑x ⊆ A

@[simp]

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

@[simp]

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

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

@[simp]

theorem ZFClass.cmem_sUnion {A B : ZFClass.{u}} : B.CMem A.sUnion ↔ ∃ (C : ZFClass.{u}), C.CMem A ∧ B.CMem C

theorem ZFClass.mem_sInter {A : ZFClass.{u}} {y : ZFSet.{u}} : y ∈ A.sInter ↔ ∀ z ∈ A, y ∈ z

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

theorem ZFClass.cmem_of_cmem_sInter {A B C : ZFClass.{u}} (hy : B.CMem A.sInter) (hz : C.CMem A) : B.CMem C

theorem ZFClass.cmem_sInter {A B : ZFClass.{u}} (h : Set.Nonempty A) : B.CMem A.sInter ↔ ∀ (z : ZFClass.{u}), z.CMem A → B.CMem z

@[simp]

theorem ZFClass.sUnion_empty : ∅.sUnion = ∅

@[simp]

theorem ZFClass.sInter_empty : ∅.sInter = Set.univ

theorem ZFClass.eq_univ_of_powerset_subset {A : ZFClass.{u}} (hA : A.powerset ⊆ A) : A = Set.univ

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

def ZFClass.iota (A : ZFClass.{u_1}) : ZFClass.{u_1}

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

Equations

• A.iota = ZFClass.sUnion {x : ZFSet.{?u.1} | ∀ (y : ZFSet.{?u.1}), ZFClass.CMem (↑y) A ↔ y = x}

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

theorem ZFClass.iota_ex (A : ZFClass.{u}) : A.iota.CMem Set.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 ZFClass → Set function.

def ZFClass.fval (F A : ZFClass.{u}) : ZFClass.{u}

Function value

Equations

• F ′ A = ZFClass.iota {y : ZFSet.{?u.1} | A.CMem {x : ZFSet.{?u.1} | ZFClass.CMem (↑(x.pair y)) F}}

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

Function value

Equations

• ZFClass.«term_′_» = Lean.ParserDescr.trailingNode `ZFClass.«term_′_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ′ ") (Lean.ParserDescr.cat `term 101))

theorem ZFClass.fval_ex (F A : ZFClass.{u}) : (F ′ A).CMem Set.univ

@[deprecated ZFClass (since := "2026-09-25")]

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. This is poor practice, and one of the reasons why Class is deprecated in favor of ZFClass.

Equations

• Class.{?u.1} = Set ZFSet.{?u.1}

@[instance_reducible]

instance instLEClass : LE Class.{u_1}

Equations

• instLEClass = { le := instLEClass._aux_1 }

@[instance_reducible]

instance instEmptyCollectionClass : EmptyCollection Class.{u_1}

Equations

• instEmptyCollectionClass = { emptyCollection := instEmptyCollectionClass._aux_1 }

instance instNonemptyClass : Nonempty Class.{u_1}

@[instance_reducible]

instance instUnionClass : Union Class.{u_1}

Equations

• instUnionClass = { union := instUnionClass._aux_1 }

@[instance_reducible]

instance instInterClass : Inter Class.{u_1}

Equations

• instInterClass = { inter := instInterClass._aux_1 }

@[instance_reducible]

instance instComplClass : Compl Class.{u_1}

Equations

• instComplClass = { compl := instComplClass._aux_1 }

@[instance_reducible]

instance instSDiffClass : SDiff Class.{u_1}

Equations

• instSDiffClass = { sdiff := instSDiffClass._aux_1 }

@[instance_reducible, deprecated Set.insert (since := "2026-09-25")]

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

Equations

• instInsertZFSetClass = { insert := Set.insert }

@[instance_reducible, deprecated "without replacement" (since := "2026-09-25")]

instance instCoeFunClassForallZFSetProp : CoeFun Class.{u_1} fun (x : Class.{u_1}) => ZFSet.{u_1} → Prop

Class is treated as (the definitionally equal) ZFSet → Prop, so that A x means that the ZFC set x belongs to the class A.

Equations

• instCoeFunClassForallZFSetProp = { coe := Set.Mem }

@[deprecated Sep.sep (since := "2026-09-25")]

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

Equations

• Class.sep p A = {y : ZFSet.{?u.1} | A.Mem y ∧ p y}

@[deprecated Set.ext (since := "2026-09-25")]

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

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

@[deprecated SetLike.coe (since := "2026-09-25")]

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

Coerce a ZFC set into a class

Equations

• ↑x = {y : ZFSet.{?u.1} | y ∈ x}

@[instance_reducible, deprecated inferInstance (since := "2026-09-25")]

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

Equations

• Class.instCoeZFSet = { coe := Class.coe }

@[deprecated Set.univ (since := "2026-09-25")]

def Class.univ : Class.{u_1}

The universal class

Equations

• Class.univ = Set.univ

@[instance_reducible, deprecated inferInstance (since := "2026-09-25")]

instance Class.instTop : Top Class.{u_1}

Equations

• Class.instTop = { top := Class.univ }

@[instance_reducible]

instance Class.instCompleteLattice : CompleteLattice Class.{u_1}

Equations

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

@[deprecated ZFClass.CMem (since := "2026-09-25")]

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

Assert that A is a ZFC set satisfying B

Equations

• B.ToSet A = ∃ (x : ZFSet.{?u.1}), ↑x = A ∧ B.Mem x

@[deprecated ZFClass.CMem (since := "2026-09-25")]

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

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

Equations

• B.Mem A = B.ToSet A

@[instance_reducible, deprecated inferInstance (since := "2026-09-25")]

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

Equations

• Class.instMembership = { mem := Class.Mem }

@[deprecated ZFClass.CMem (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.notCMem_empty (since := "2026-09-25")]

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

@[simp, deprecated Set.notMem_empty (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.cmem_univ (since := "2026-09-25")]

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

@[simp, deprecated Set.mem_univ (since := "2026-09-25")]

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

@[deprecated Set.eq_univ_iff_forall (since := "2026-09-25")]

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

@[deprecated Set.eq_univ_of_forall (since := "2026-09-25")]

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

@[deprecated inferInstance (since := "2026-09-25")]

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

@[instance_reducible, deprecated ZFClass.instWellFoundedRelation (since := "2026-09-25")]

instance Class.instWellFoundedRelation : WellFoundedRelation Class.{u_1}

Equations

• Class.instWellFoundedRelation = { rel := fun (x1 x2 : Class.{?u.1}) => x1 ∈ x2, wf := Class.mem_wf }

@[deprecated ZFClass.cmem_asymm (since := "2026-09-25")]

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

@[deprecated ZFClass.cmem_irrefl (since := "2026-09-25")]

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

@[deprecated ZFClass.univ_notCMem_univ (since := "2026-09-25")]

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

@[deprecated ZFClass.congToClass (since := "2026-09-25")]

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

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

Equations

• Class.congToClass x = {y : ZFSet.{?u.1} | ↑y ∈ x}

@[simp, deprecated ZFClass.congToClass_empty (since := "2026-09-25")]

theorem Class.congToClass_empty : congToClass ∅ = ∅

@[deprecated ZFClass.classToCong (since := "2026-09-25")]

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

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

Equations

• x.classToCong = {y : Class.{?u.1} | y ∈ x}

@[simp, deprecated ZFClass.classToCong_empty (since := "2026-09-25")]

theorem Class.classToCong_empty : ∅.classToCong = ∅

@[deprecated ZFClass.powerset (since := "2026-09-25")]

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

Equations

• x.powerset = Class.congToClass (𝒫 x)

@[deprecated ZFClass.sUnion (since := "2026-09-25")]

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.

Equations

• x.sUnion = sSup x.classToCong

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.

Equations

• Class.«term⋃₀_» = Lean.ParserDescr.node `Class.«term⋃₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

@[deprecated ZFClass.sInter (since := "2026-09-25")]

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.

Equations

• x.sInter = sInf x.classToCong

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.

Equations

• Class.«term⋂₀_» = Lean.ParserDescr.node `Class.«term⋂₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

@[deprecated SetLike.coe_injective (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_cmem (since := "2026-09-25")]

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

@[simp, deprecated SetLike.mem_coe (since := "2026-09-25")]

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

@[simp, deprecated SetLike.mem_coe (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_subset (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_sep (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_empty (since := "2026-09-25")]

theorem Class.coe_empty : ↑∅ = ∅

@[simp, deprecated ZFClass.coe_insert (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_union (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_inter (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_sdiff (since := "2026-09-25")]

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

@[deprecated Class.coe_sdiff (since := "2026-06-03")]

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

Alias of Class.coe_sdiff.

@[simp, deprecated ZFClass.coe_powerset (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.mem_powerset (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.mem_sUnion (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_sUnion (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.cmem_sUnion (since := "2026-09-25")]

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

@[deprecated ZFClass.mem_sInter (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.coe_sInter (since := "2026-09-25")]

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

@[deprecated ZFClass.cmem_of_cmem_sInter (since := "2026-09-25")]

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

@[deprecated ZFClass.cmem_sInter (since := "2026-09-25")]

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

@[simp, deprecated ZFClass.sUnion_empty (since := "2026-09-25")]

theorem Class.sUnion_empty : ∅.sUnion = ∅

@[simp, deprecated ZFClass.sInter_empty (since := "2026-09-25")]

theorem Class.sInter_empty : ∅.sInter = univ

@[deprecated ZFClass.eq_univ_of_powerset_subset (since := "2026-09-25")]

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.

@[deprecated ZFClass.iota (since := "2026-09-25")]

def Class.iota (A : Class.{u_1}) : Class.{u_1}

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

Equations

• A.iota = Class.sUnion {x : ZFSet.{?u.1} | ∀ (y : ZFSet.{?u.1}), A.Mem y ↔ y = x}

@[deprecated ZFClass.iota_val (since := "2026-09-25")]

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

@[deprecated ZFClass.iota_ex (since := "2026-09-25")]

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.

@[deprecated ZFClass.fval (since := "2026-09-25")]

def Class.fval (F A : Class.{u}) : Class.{u}

Function value

Equations

• F.fval A = Class.iota {y : ZFSet.{?u.1} | Class.ToSet {x : ZFSet.{?u.1} | F.Mem (x.pair y)} A}

@[deprecated ZFClass.fval_ex (since := "2026-09-25")]

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

@[simp]

theorem ZFSet.map_fval {x y : ZFSet.{u}} {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] (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.

Equations

• x.choice = ZFSet.map (fun (y : ZFSet.{?u.1}) => Classical.epsilon fun (z : ZFSet.{?u.1}) => z ∈ y) x

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_cmem (x : ZFSet.{u}) (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) : (↑x.choice ′ ↑y).CMem ↑y

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

SetLike.coe as an equivalence.

Equations

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

@[simp]

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

theorem ZFSet.isOrdinal_notCMem_univ : ¬ZFClass.CMem {x : ZFSet.{u} | x.IsOrdinal} Set.univ

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