A model of ZFC

In this file, we model Zermelo-Fraenkel set theory (+ choice) using Lean's underlying type theory, building on the pre-sets defined in Mathlib.SetTheory.ZFC.PSet.

The theory of classes is developed in Mathlib.SetTheory.ZFC.Class.

Main definitions

• ZFSet: ZFC set. Defined as PSet quotiented by PSet.Equiv, the extensional equivalence.
• ZFSet.choice: Axiom of choice. Proved from Lean's axiom of choice.
• ZFSet.omega: The von Neumann ordinal ω as a Set.
• Classical.allZFSetDefinable: 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.

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

def ZFSet : Type (u + 1)

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

Equations

• ZFSet.{?u.3} = Quotient PSet.setoid

def ZFSet.mk : PSet.{u_1} → ZFSet.{u_1}

Turns a pre-set into a ZFC set.

Equations

• ZFSet.mk = Quotient.mk''

@[simp]

theorem ZFSet.mk_eq (x : PSet.{u_1}) : ⟦x⟧ = mk x

@[simp]

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

class ZFSet.Definable (n : ℕ) (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) : Type (u + 1)

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

• out : (Fin n → PSet.{u}) → PSet.{u}

  Turns a definable function into an n-ary PSet function.

• mk_out (xs : Fin n → PSet.{u}) : ZFSet.mk (out f xs) = f fun (x : Fin n) => ZFSet.mk (xs x)

  A set function f is the image of Definable.out f.

@[reducible, inline]

abbrev ZFSet.Definable₁ (f : ZFSet.{u} → ZFSet.{u}) : Type (u + 1)

An abbrev of ZFSet.Definable for unary functions.

Equations

• ZFSet.Definable₁ f = ZFSet.Definable 1 fun (s : Fin 1 → ZFSet.{?u.18}) => f (s 0)

@[reducible, inline]

abbrev ZFSet.Definable₁.mk {f : ZFSet.{u} → ZFSet.{u}} (out : PSet.{u} → PSet.{u}) (mk_out : ∀ (x : PSet.{u}), ⟦out x⟧ = f ⟦x⟧) : Definable₁ f

A simpler constructor for ZFSet.Definable₁.

Equations

• ZFSet.Definable₁.mk out mk_out = { out := fun (xs : Fin 1 → PSet.{?u.42}) => out (xs 0), mk_out := ⋯ }

@[reducible, inline]

abbrev ZFSet.Definable₁.out (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] : PSet.{u} → PSet.{u}

Turns a unary definable function into a unary PSet function.

Equations

• ZFSet.Definable₁.out f x = ZFSet.Definable.out (fun (s : Fin (Nat.succ 0) → ZFSet.{?u.33}) => f (s 0)) ![x]

theorem ZFSet.Definable₁.mk_out {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x : PSet.{u}} : ZFSet.mk (out f x) = f (ZFSet.mk x)

@[reducible, inline]

abbrev ZFSet.Definable₂ (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) : Type (u + 1)

An abbrev of ZFSet.Definable for binary functions.

Equations

• ZFSet.Definable₂ f = ZFSet.Definable 2 fun (s : Fin 2 → ZFSet.{?u.24}) => f (s 0) (s 1)

@[reducible, inline]

abbrev ZFSet.Definable₂.mk {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} (out : PSet.{u} → PSet.{u} → PSet.{u}) (mk_out : ∀ (x y : PSet.{u}), ⟦out x y⟧ = f ⟦x⟧ ⟦y⟧) : Definable₂ f

A simpler constructor for ZFSet.Definable₂.

Equations

• ZFSet.Definable₂.mk out mk_out = { out := fun (xs : Fin 2 → PSet.{?u.56}) => out (xs 0) (xs 1), mk_out := ⋯ }

@[reducible, inline]

abbrev ZFSet.Definable₂.out (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] : PSet.{u} → PSet.{u} → PSet.{u}

Turns a binary definable function into a binary PSet function.

Equations

• ZFSet.Definable₂.out f x y = ZFSet.Definable.out (fun (s : Fin (Nat.succ 0).succ → ZFSet.{?u.48}) => f (s 0) (s 1)) ![x, y]

theorem ZFSet.Definable₂.mk_out {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} [Definable₂ f] {x y : PSet.{u}} : ZFSet.mk (out f x y) = f (ZFSet.mk x) (ZFSet.mk y)

instance ZFSet.instDefinableOfDefinable₁ (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] (n : ℕ) (g : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) [Definable n g] : Definable n fun (s : Fin n → ZFSet.{u_1}) => f (g s)

Equations

• ZFSet.instDefinableOfDefinable₁ f n g = { out := fun (xs : Fin n → PSet.{?u.62}) => ZFSet.Definable₁.out f (ZFSet.Definable.out g xs), mk_out := ⋯ }

instance ZFSet.instDefinableOfDefinable₂ (f : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}) [Definable₂ f] (n : ℕ) (g₁ g₂ : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) [Definable n g₁] [Definable n g₂] : Definable n fun (s : Fin n → ZFSet.{u_1}) => f (g₁ s) (g₂ s)

Equations

• ZFSet.instDefinableOfDefinable₂ f n g₁ g₂ = { out := fun (xs : Fin n → PSet.{?u.88}) => ZFSet.Definable₂.out f (ZFSet.Definable.out g₁ xs) (ZFSet.Definable.out g₂ xs), mk_out := ⋯ }

instance ZFSet.instDefinable (n : ℕ) (i : Fin n) : Definable n fun (s : Fin n → ZFSet.{u_1}) => s i

Equations

• ZFSet.instDefinable n i = { out := fun (s : Fin n → PSet.{?u.29}) => s i, mk_out := ⋯ }

theorem ZFSet.Definable.out_equiv {n : ℕ} (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) [Definable n f] {xs ys : Fin n → PSet.{u}} (h : ∀ (i : Fin n), xs i ≈ ys i) : out f xs ≈ out f ys

theorem ZFSet.Definable₁.out_equiv (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] {x y : PSet.{u}} (h : x ≈ y) : out f x ≈ out f y

theorem ZFSet.Definable₂.out_equiv (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] {x₁ y₁ x₂ y₂ : PSet.{u}} (h₁ : x₁ ≈ y₁) (h₂ : x₂ ≈ y₂) : out f x₁ x₂ ≈ out f y₁ y₂

noncomputable def Classical.allZFSetDefinable {n : ℕ} (F : (Fin n → ZFSet.{u}) → ZFSet.{u}) : ZFSet.Definable n F

All functions are classically definable.

Equations

• Classical.allZFSetDefinable F = { out := fun (xs : Fin n → PSet.{?u.30}) => Quotient.out (F fun (x : Fin n) => ZFSet.mk (xs x)), mk_out := ⋯ }

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

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

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

def ZFSet.Mem : ZFSet.{u_1} → ZFSet.{u_1} → Prop

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

Equations

• ZFSet.Mem = Quotient.lift₂ (fun (x1 x2 : PSet.{?u.17}) => x1 ∈ x2) ZFSet.Mem.proof_1

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

Equations

• ZFSet.instMembership = { mem := fun (t s : ZFSet.{?u.5}) => s.Mem t }

@[simp]

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

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

Convert a ZFC set into a Set of ZFC sets

Equations

• u.toSet = {x : ZFSet.{?u.2} | x ∈ u}

@[simp]

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

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

def ZFSet.Nonempty (u : ZFSet.{u_1}) : Prop

A nonempty set is one that contains some element.

Equations

• u.Nonempty = u.toSet.Nonempty

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

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

@[simp]

theorem ZFSet.nonempty_toSet_iff {u : ZFSet.{u_1}} : u.toSet.Nonempty ↔ u.Nonempty

def ZFSet.Subset (x y : ZFSet.{u}) : Prop

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

Equations

• x.Subset y = ∀ ⦃z : ZFSet.{?u.19}⦄, z ∈ x → z ∈ y

instance ZFSet.hasSubset : HasSubset ZFSet.{u_1}

Equations

• ZFSet.hasSubset = { Subset := ZFSet.Subset }

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

instance ZFSet.instIsReflSubset : IsRefl ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

instance ZFSet.instIsTransSubset : IsTrans ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

@[simp]

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

@[simp]

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

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

theorem ZFSet.toSet_injective : Function.Injective toSet

@[simp]

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

instance ZFSet.instIsAntisymmSubset : IsAntisymm ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

def ZFSet.empty : ZFSet.{u_1}

The empty ZFC set

Equations

• ZFSet.empty = ZFSet.mk ∅

instance ZFSet.instEmptyCollection : EmptyCollection ZFSet.{u_1}

Equations

• ZFSet.instEmptyCollection = { emptyCollection := ZFSet.empty }

instance ZFSet.instInhabited : Inhabited ZFSet.{u_1}

Equations

• ZFSet.instInhabited = { default := ∅ }

@[simp]

theorem ZFSet.not_mem_empty (x : ZFSet.{u}) : x ∉ ∅

@[simp]

theorem ZFSet.toSet_empty : ∅.toSet = ∅

@[simp]

theorem ZFSet.empty_subset (x : ZFSet.{u}) : ∅ ⊆ x

@[simp]

theorem ZFSet.not_nonempty_empty : ¬∅.Nonempty

@[simp]

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

theorem ZFSet.eq_empty (x : ZFSet.{u}) : x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x

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

def ZFSet.Insert : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}

Insert x y is the set {x} ∪ y

Equations

• ZFSet.Insert = Quotient.map₂ PSet.insert ZFSet.Insert.proof_1

instance ZFSet.instInsert : Insert ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.instInsert = { insert := ZFSet.Insert }

instance ZFSet.instSingleton : Singleton ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.instSingleton = { singleton := fun (x : ZFSet.{?u.4}) => insert x ∅ }

instance ZFSet.instLawfulSingleton : LawfulSingleton ZFSet.{u_1} ZFSet.{u_1}

@[simp]

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

theorem ZFSet.mem_insert (x y : ZFSet.{u_1}) : x ∈ insert x y

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem ZFSet.insert_nonempty (u v : ZFSet.{u_1}) : (insert u v).Nonempty

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

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

@[simp]

theorem ZFSet.pair_eq_singleton (x : ZFSet.{u_1}) : {x, x} = {x}

@[simp]

theorem ZFSet.pair_eq_singleton_iff {x y z : ZFSet.{u_1}} : {x, y} = {z} ↔ x = z ∧ y = z

@[simp]

theorem ZFSet.singleton_eq_pair_iff {x y z : ZFSet.{u_1}} : {x} = {y, z} ↔ x = y ∧ x = z

def ZFSet.omega : ZFSet.{u_1}

omega is the first infinite von Neumann ordinal

Equations

• ZFSet.omega = ZFSet.mk PSet.omega

@[simp]

theorem ZFSet.omega_zero : ∅ ∈ omega

@[simp]

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

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

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

Equations

• ZFSet.sep p = Quotient.map (PSet.sep fun (y : PSet.{?u.17}) => p (ZFSet.mk y)) ⋯

instance ZFSet.instSep : Sep ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.instSep = { sep := ZFSet.sep }

@[simp]

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

@[simp]

theorem ZFSet.sep_empty (p : ZFSet.{u_1} → Prop) : ZFSet.sep p ∅ = ∅

@[simp]

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

def ZFSet.powerset : ZFSet.{u_1} → ZFSet.{u_1}

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

Equations

• ZFSet.powerset = Quotient.map PSet.powerset ZFSet.powerset.proof_1

@[simp]

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

theorem ZFSet.sUnion_lem {α β : Type u} (A : α → PSet.{u}) (B : β → PSet.{u}) (αβ : ∀ (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)

def ZFSet.sUnion : ZFSet.{u_1} → ZFSet.{u_1}

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

Equations

• ZFSet.sUnion = Quotient.map PSet.sUnion ZFSet.sUnion.proof_1

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

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

Equations

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

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

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

Equations

• ⋂₀ x = ZFSet.sep (fun (y : ZFSet.{?u.2}) => ∀ z ∈ x, y ∈ z) (⋃₀ x)

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

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

Equations

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

@[simp]

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

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

@[simp]

theorem ZFSet.sUnion_empty : ⋃₀ ∅ = ∅

@[simp]

theorem ZFSet.sInter_empty : ⋂₀ ∅ = ∅

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem ZFSet.singleton_injective : Function.Injective singleton

@[simp]

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

def ZFSet.union (x y : ZFSet.{u}) : ZFSet.{u}

The binary union operation

Equations

• x.union y = ⋃₀ {x, y}

def ZFSet.inter (x y : ZFSet.{u}) : ZFSet.{u}

The binary intersection operation

Equations

• x.inter y = ZFSet.sep (fun (z : ZFSet.{?u.18}) => z ∈ y) x

def ZFSet.diff (x y : ZFSet.{u}) : ZFSet.{u}

The set difference operation

Equations

• x.diff y = ZFSet.sep (fun (z : ZFSet.{?u.18}) => z ∉ y) x

instance ZFSet.instUnion : Union ZFSet.{u_1}

Equations

• ZFSet.instUnion = { union := ZFSet.union }

instance ZFSet.instInter : Inter ZFSet.{u_1}

Equations

• ZFSet.instInter = { inter := ZFSet.inter }

instance ZFSet.instSDiff : SDiff ZFSet.{u_1}

Equations

• ZFSet.instSDiff = { sdiff := ZFSet.diff }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem ZFSet.mem_wf : WellFounded fun (x1 x2 : ZFSet.{u_1}) => x1 ∈ x2

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

Induction on the ∈ relation.

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

instance ZFSet.instWellFoundedRelation : WellFoundedRelation ZFSet.{u_1}

Equations

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

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

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

theorem ZFSet.not_subset_of_mem {x y : ZFSet.{u_1}} (h : x ∈ y) : ¬y ⊆ x

theorem ZFSet.not_mem_of_subset {x y : ZFSet.{u_1}} (h : x ⊆ y) : y ∉ x

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

def ZFSet.image (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] : ZFSet.{u_1} → ZFSet.{u_1}

The image of a (definable) ZFC set function

Equations

• ZFSet.image f = Quotient.map (PSet.image (ZFSet.Definable₁.out f)) ⋯

theorem ZFSet.image.mk (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] (x : ZFSet.{u}) {y : ZFSet.{u}} : y ∈ x → f y ∈ image f x

@[simp]

theorem ZFSet.mem_image {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}} : y ∈ image f x ↔ ∃ z ∈ x, f z = y

@[simp]

theorem ZFSet.toSet_image (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] (x : ZFSet.{u_1}) : (image f x).toSet = f '' x.toSet

noncomputable def ZFSet.range {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : ZFSet.{u}

The range of a type-indexed family of sets.

Equations

• ZFSet.range f = ⟦PSet.mk (Shrink.{?u.30, ?u.29} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)⟧

@[simp]

theorem ZFSet.mem_range {α : Type u_1} [Small.{u, u_1} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}} : x ∈ range f ↔ x ∈ Set.range f

@[simp]

theorem ZFSet.toSet_range {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : (range f).toSet = Set.range f

def ZFSet.pair (x y : ZFSet.{u}) : ZFSet.{u}

Kuratowski ordered pair

Equations

• x.pair y = {{x}, {x, y}}

@[simp]

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

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

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

Equations

• ZFSet.pairSep p x y = ZFSet.sep (fun (z : ZFSet.{?u.29}) => ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b) (x ∪ y).powerset.powerset

@[simp]

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

theorem ZFSet.pair_injective : Function.Injective2 pair

@[simp]

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

def ZFSet.prod : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}

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

Equations

• ZFSet.prod = ZFSet.pairSep fun (x x : ZFSet.{?u.6}) => True

@[simp]

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

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

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

Equations

• x.IsFunc y f = (f ⊆ x.prod y ∧ ∀ z ∈ x, ∃! w : ZFSet.{?u.4}, z.pair w ∈ f)

def ZFSet.funs (x y : ZFSet.{u}) : ZFSet.{u}

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

@[simp]

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

instance ZFSet.instDefinable₁Singleton : Definable₁ fun (x : ZFSet.{u_1}) => {x}

Equations

• ZFSet.instDefinable₁Singleton = ZFSet.Definable₁.mk (fun (x : PSet.{?u.17}) => {x}) ZFSet.instDefinable₁Singleton.proof_1

instance ZFSet.instDefinable₂Insert : Definable₂ insert

Equations

• ZFSet.instDefinable₂Insert = ZFSet.Definable₂.mk insert ZFSet.instDefinable₂Insert.proof_1

instance ZFSet.instDefinable₂Pair : Definable₂ pair

Equations

• ZFSet.instDefinable₂Pair = id inferInstance

def ZFSet.map (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] : ZFSet.{u_1} → ZFSet.{u_1}

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

Equations

• ZFSet.map f = ZFSet.image fun (y : ZFSet.{?u.32}) => y.pair (f y)

@[simp]

theorem ZFSet.mem_map {f : ZFSet.{u_1} → ZFSet.{u_1}} [Definable₁ f] {x y : ZFSet.{u_1}} : y ∈ map f x ↔ ∃ z ∈ x, z.pair (f z) = y

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

@[simp]

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

@[irreducible]

def ZFSet.Hereditarily (p : ZFSet.{u_1} → Prop) (x : ZFSet.{u_1}) : 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 ∈ x, ZFSet.Hereditarily p y)

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

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

Alias of the forward direction of ZFSet.hereditarily_iff.

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

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

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