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

Equations

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

instance instClassHasSubset : HasSubset Class.{u_1}

Equations

• instClassHasSubset = Set.instHasSubset

instance instClassEmptyCollection : EmptyCollection Class.{u_1}

Equations

• instClassEmptyCollection = Set.instEmptyCollection

instance instClassNonempty : Nonempty Class.{u_1}

Equations

• instClassNonempty = ⋯

instance instClassUnion : Union Class.{u_1}

Equations

• instClassUnion = Set.instUnion

instance instClassInter : Inter Class.{u_1}

Equations

• instClassInter = Set.instInter

instance instClassHasCompl : HasCompl Class.{u_1}

Equations

• instClassHasCompl = Set.instHasCompl

instance instClassSDiff : SDiff Class.{u_1}

Equations

• instClassSDiff = Set.instSDiff

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

Equations

• instInsertZFSetClass = { insert := Set.insert }

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.19} | A y ∧ p y}

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

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

Coerce a ZFC set into a class

Equations

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

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

Equations

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

def Class.univ : Class.{u_1}

The universal class

Equations

• Class.univ = Set.univ

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

Assert that A is a ZFC set satisfying B

Equations

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

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 Class.instMembership : Membership Class.{u_1} Class.{u_1}

Equations

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

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

@[simp]

theorem Class.not_mem_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}

Equations

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

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

Equations

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

@[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)

Equations

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

@[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

Equations

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

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

Equations

• ⋃₀ x = ⋃₀ x.classToCong

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

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

Equations

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

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

Equations

• ⋂₀ x = ⋂₀ x.classToCong

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

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

Equations

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

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) y ↔ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

theorem Class.sUnion_empty : ⋃₀ ∅ = ∅

@[simp]

theorem Class.sInter_empty : ⋂₀ ∅ = 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.

Equations

• A.iota = ⋃₀ {x : ZFSet.{?u.13} | ∀ (y : ZFSet.{?u.13}), A y ↔ y = x}

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

Equations

• F ′ A = Class.iota fun (y : ZFSet.{?u.19}) => Class.ToSet (fun (x : ZFSet.{?u.19}) => F (x.pair y)) A

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

Function value

Equations

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

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.

Equations

• x.choice = ZFSet.map (fun (y : ZFSet.{?u.15}) => Classical.epsilon fun (z : ZFSet.{?u.15}) => 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) x.choice

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

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

ZFSet.toSet as an equivalence.

Equations

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

@[simp]

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

theorem ZFSet.isOrdinal_not_mem_univ : IsOrdinal ∉ Class.univ

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