Basic theory of models of ZF set theory

This module develops the order-theoretic and membership structure on models of ZF, including the von Neumann hierarchy and foundational lemmas used throughout the Kunen inconsistency development.

def Membership.mem.formula : ZFFormula 2

The formula declaration.

Equations

• Membership.mem.formula = FirstOrder.Language.Relations.boundedFormula₂ memRel.mem ((FirstOrder.Language.var ∘ Sum.inl) 1) ((FirstOrder.Language.var ∘ Sum.inl) 0)

theorem Membership.mem.realize_iff {M : Type u_1} [ZFStructure M] {v₂ : Fin 2 → M} : FirstOrder.Language.Formula.Realize formula v₂ ↔ v₂ 1 ∈ v₂ 0

theorem Membership.mem.to_realize {M : Type u_1} [sM : ZFStructure M] (x₁ x₂ : M) : x₂ ∈ x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem Membership.mem.elementarity {M : Type u_2} [sM : ZFStructure M] {N : Type u_3} [sN : ZFStructure N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₂ ∈ j x₁ ↔ x₂ ∈ x₁

def Ne.formula : ZFFormula 2

The formula declaration.

Equations

• Ne.formula = (((FirstOrder.Language.var ∘ Sum.inl) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inl) 1)).not

theorem Ne.realize_iff {M : Type u_1} [ZFStructure M] {v₂ : Fin 2 → M} : FirstOrder.Language.Formula.Realize formula v₂ ↔ v₂ 0 ≠ v₂ 1

theorem Ne.to_realize {M : Type u_1} [sM : ZFStructure M] (x₁ x₂ : M) : x₁ ≠ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem Ne.elementarity {M : Type u_2} [sM : ZFStructure M] {N : Type u_3} [sN : ZFStructure N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₁ ≠ j x₂ ↔ x₁ ≠ x₂

def Eq.formula : ZFFormula 2

The formula declaration.

Equations

• Eq.formula = ((FirstOrder.Language.var ∘ Sum.inl) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inl) 1)

theorem Eq.realize_iff {M : Type u_1} [ZFStructure M] {v₂ : Fin 2 → M} : FirstOrder.Language.Formula.Realize formula v₂ ↔ v₂ 0 = v₂ 1

theorem Eq.elementarity {M : Type u_2} [sM : ZFStructure M] {N : Type u_3} [sN : ZFStructure N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₁ = j x₂ ↔ x₁ = x₂

theorem Eq.to_realize {M : Type u_1} [sM : ZFStructure M] (x₁ x₂ : M) : x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

def HasSubset.Subset.formula : ZFFormula 2

The formula declaration.

Equations

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

theorem HasSubset.Subset.realize_iff {M : Type u_1} [ZFStructure M] {v₂ : Fin 2 → M} : FirstOrder.Language.Formula.Realize formula v₂ ↔ v₂ 0 ⊆ v₂ 1

theorem HasSubset.Subset.to_realize {M : Type u_1} [sM : ZFStructure M] (x₁ x₂ : M) : x₁ ⊆ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem HasSubset.Subset.elementarity {M : Type u_2} [sM : ZFStructure M] {N : Type u_3} [sN : ZFStructure N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₁ ⊆ j x₂ ↔ x₁ ⊆ x₂

@[simp]

theorem EmptyCollection.emptyCollection.spec {M : Type u_1} [ZFStructure M] [HasEmpty M] (x : M) : x ∉ ∅

theorem EmptyCollection.emptyCollection.eq_iff {M : Type u_1} [ZFStructure M] [HasEmpty M] (x : M) : ∅ = x ↔ ∀ (y : M), y ∉ x

def EmptyCollection.emptyCollection.formula : ZFFormula 1

The formula declaration.

Equations

• EmptyCollection.emptyCollection.formula = EqEmptyN 0

theorem EmptyCollection.emptyCollection.realize_iff {M : Type u_1} [ZFStructure M] {v₁ : Fin 1 → M} [HasEmpty M] : FirstOrder.Language.Formula.Realize formula v₁ ↔ ∅ = v₁ 0

theorem EmptyCollection.emptyCollection.eu {M : Type u_1} [ZFStructure M] [HasEmpty M] : ∃! x : M, ∀ (y : M), y ∉ x

theorem EmptyCollection.emptyCollection.elementarity {M : Type u_2} [sM : ZFStructure M] [cM₁ : HasEmpty M] {N : Type u_3} [sN : ZFStructure N] [cN₁ : HasEmpty N] {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : ∅ = j ∅

theorem EmptyCollection.emptyCollection.to_realize {M : Type u_1} [sM : ZFStructure M] [cM₁ : HasEmpty M] (x₁ : M) : ∅ = x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

instance EmptyCollection.emptyCollection.instFormulaToFunction {M : Type u_1} [sM : ZFStructure M] [cM₁ : HasEmpty M] : FormulaToFunction formula fun (v : Fin 0 → M) => ∅

structure SetTheory.V : Type 1

The von Neumann universe V carrier, wrapping a ground-model ZFSet.

• val : ZFSet.{0}

  The underlying ZFSet of an element of V.

theorem SetTheory.V.ext (x y : V) : x.val = y.val → x = y

theorem SetTheory.V.ext_iff {x y : V} : x = y ↔ x.val = y.val

class SetTheory.ToV (α : Type u_1) : Type (max 1 u_1)

The ToV type.

• toV : α → V

  The toV declaration.

def SetTheory.toZFSet {α : Type u_1} [ToV α] (x : α) : ZFSet.{0}

The toZFSet declaration.

Equations

• ⇓x = (↓x).val

def SetTheory.«term↓_» : Lean.ParserDescr

The ↓_ notation.

Equations

• SetTheory.«term↓_» = Lean.ParserDescr.node `SetTheory.«term↓_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↓") (Lean.ParserDescr.cat `term 1024))

def SetTheory.«term⇓_» : Lean.ParserDescr

The ⇓_ notation.

Equations

• SetTheory.«term⇓_» = Lean.ParserDescr.node `SetTheory.«term⇓_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⇓") (Lean.ParserDescr.cat `term 1024))

@[implicit_reducible]

instance SetTheory.instToVZFSet : ToV ZFSet.{0}

Equations

• SetTheory.instToVZFSet = { toV := fun (x : ZFSet.{0}) => { val := x } }

@[implicit_reducible]

instance SetTheory.structureZFSet {A : ZFSet.{0}} : 𝓛ZF.Structure ↥A

Equations

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

theorem SetTheory.mem_inside_ZFSet {A : ZFSet.{0}} {x y : ↥A} : x ∈ y ↔ ↑x ∈ ↑y

@[implicit_reducible]

instance SetTheory.structureV : 𝓛ZF.Structure V

Equations

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

class inductive SetTheory.IsVonNeumann (α : Type 1) [s : ZFStructure α] : Type 1

The IsVonNeumann type.

• vonNeumann {α : Type 1} [s : ZFStructure α] (μ : Ordinal.{0}) (hμ : Order.IsSuccLimit μ) (eq : ⟨α, s⟩ = ⟨↥(ZFSet.vonNeumann μ), structureZFSet⟩) : IsVonNeumann α
• V {α : Type 1} [s : ZFStructure α] (eq : ⟨α, s⟩ = ⟨SetTheory.V, structureV⟩) : IsVonNeumann α

class inductive SetTheory.IsVonNeumannWithOmega (α : Type 1) [s : ZFStructure α] : Type 1

The IsVonNeumannWithOmega type.

• vonNeumann {α : Type 1} [s : ZFStructure α] (μ : Ordinal.{0}) (hμ : Order.IsSuccLimit μ) (omega_lt_μ : Ordinal.omega0 < μ) (eq : ⟨α, s⟩ = ⟨↥(ZFSet.vonNeumann μ), structureZFSet⟩) : IsVonNeumannWithOmega α
• V {α : Type 1} [s : ZFStructure α] (eq : ⟨α, s⟩ = ⟨SetTheory.V, structureV⟩) : IsVonNeumannWithOmega α

def tacticSplit_vonNeumann_ : Lean.ParserDescr

Case-split on the proof h : IsVonNeumann M, introducing μ and hμ in the successor-limit case and discharging the V case, then registering the limit fact.

Equations

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

def tacticSplit_vonNeumann_omega_ : Lean.ParserDescr

Like split_vonNeumann, but for IsVonNeumannWithOmega M, additionally introducing the hypothesis omega_lt_μ that ω < μ.

Equations

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

@[implicit_reducible]

instance SetTheory.instIsVonNeumann {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] : IsVonNeumann M₀

Equations

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

@[implicit_reducible]

instance SetTheory.instIsVonNeumannSubtypeZFSetMemVonNeumannOfFactIsSuccLimitOrdinal {μ : Ordinal.{0}} [hμ : Fact (Order.IsSuccLimit μ)] : IsVonNeumann ↥(ZFSet.vonNeumann μ)

Equations

• SetTheory.instIsVonNeumannSubtypeZFSetMemVonNeumannOfFactIsSuccLimitOrdinal = SetTheory.IsVonNeumann.vonNeumann μ ⋯ ⋯

@[implicit_reducible]

instance SetTheory.instIsVonNeumannWithOmegaV : IsVonNeumannWithOmega V

Equations

• SetTheory.instIsVonNeumannWithOmegaV = SetTheory.IsVonNeumannWithOmega.V SetTheory.instIsVonNeumann._proof_8

@[implicit_reducible]

instance SetTheory.instToV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : ToV M

Equations

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

theorem SetTheory.ToV.reduce_mem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : ↓x ∈ ↓y ↔ x ∈ y

theorem SetTheory.ToV.reduce_eq {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : ↓x = ↓y ↔ x = y

theorem SetTheory.ToV.reduce_ne {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : ↓x ≠ ↓y ↔ x ≠ y

theorem SetTheory.ToV.forall_mem_toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} {p : V → Prop} : (∀ y ∈ ↓x, p y) ↔ ∀ y ∈ x, p ↓y

theorem SetTheory.ToV.reduce_subset {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : ↓x ⊆ ↓y ↔ x ⊆ y

theorem SetTheory.ToV.forall_mem_toV_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} {p : V → Prop} (hp : ∀ (y : V), p y → ∃ (z : M), ↓z = y) : (∀ (y : V), y ∈ ↓x ↔ p y) ↔ ∀ (y : M), y ∈ x ↔ p ↓y

theorem SetTheory.ToV.exists_mem_toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} {p : V → Prop} : (∃ y ∈ ↓x, p y) ↔ ∃ y ∈ x, p ↓y

theorem SetTheory.ToZFSet.toZFSet_toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : ⇓↓x = ⇓x

theorem SetTheory.ToZFSet.toV_vonNeumann {μ : Ordinal.{0}} [Fact (Order.IsSuccLimit μ)] {x : ↥(ZFSet.vonNeumann μ)} : ↓x = { val := ↑x }

theorem SetTheory.ToZFSet.toV_V {x : V} : ↓x = { val := x.val }

theorem SetTheory.ToZFSet.toV_ZFSet {x : ZFSet.{0}} : ↓x = { val := x }

theorem SetTheory.ToZFSet.toZFSet_vonNeumann {μ : Ordinal.{0}} [Fact (Order.IsSuccLimit μ)] {x : ↥(ZFSet.vonNeumann μ)} : ⇓x = ↑x

theorem SetTheory.ToZFSet.toZFSet_V {x : V} : ⇓x = x.val

theorem SetTheory.ToZFSet.forall {p : V → Prop} : (∀ (x : V), p x) ↔ ∀ (x : ZFSet.{0}), p ↓x

theorem SetTheory.ToZFSet.exists {p : V → Prop} : (∃ (x : V), p x) ↔ ∃ (x : ZFSet.{0}), p ↓x

theorem SetTheory.ToZFSet.mem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x ∈ y ↔ ⇓x ∈ ⇓y

theorem SetTheory.ToZFSet.subset {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x ⊆ y ↔ ⇓x ⊆ ⇓y

theorem SetTheory.ToZFSet.eq {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x = y ↔ ⇓x = ⇓y

theorem SetTheory.ToZFSet.ne {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x ≠ y ↔ ⇓x ≠ ⇓y

instance SetTheory.instReflSubset_leanPool {M : Type 1} [ZFStructure M] : Std.Refl fun (x1 x2 : M) => x1 ⊆ x2

theorem SetTheory.ext {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} (eq : ∀ (z : M), z ∈ x ↔ z ∈ y) : x = y

theorem SetTheory.ext_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x = y ↔ ∀ (z : M), z ∈ x ↔ z ∈ y

theorem SetTheory.ext_of_subset {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {X A B : M} (A_sub : A ⊆ X) (B_sub : B ⊆ X) (ext : ∀ x ∈ X, x ∈ A ↔ x ∈ B) : A = B

@[implicit_reducible]

instance SetTheory.instSetLike {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : SetLike M M

Equations

• SetTheory.instSetLike = { coe := fun (x : M) => {y : M | y ∈ x}, coe_injective := ⋯ }

@[implicit_reducible]

instance SetTheory.instPartialOrderM {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : PartialOrder M

Equations

• SetTheory.instPartialOrderM = PartialOrder.ofSetLike M M

theorem SetTheory.le_def {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x ≤ y ↔ x ⊆ y

theorem SetTheory.le_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x ≤ y ↔ ∀ ⦃z : M⦄, z ∈ x → z ∈ y

theorem SetTheory.mem_of_le {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y z : M} (hsub : x ≤ y) (hz : z ∈ x) : z ∈ y

theorem SetTheory.mem_coe {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x ∈ ↑y ↔ x ∈ y

theorem SetTheory.lt_iff_le_and_exists {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : x < y ↔ x ≤ y ∧ ∃ z ∈ y, z ∉ x

theorem SetTheory.ToZFSet.le {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : x ≤ y ↔ ⇓x ≤ ⇓y

theorem SetTheory.ToZFSet.lt {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : x < y ↔ ⇓x < ⇓y

def SetTheory.IsSet {M : Type 1} [ZFStructure M] (C : Set M) : Prop

The IsSet declaration.

Equations

• SetTheory.IsSet C = ∃! x : M, ∀ (y : M), y ∈ x ↔ y ∈ C

theorem SetTheory.isSet_iff_exists_set {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {C : Set M} : IsSet C ↔ ∃ (x : M), ∀ (y : M), y ∈ x ↔ y ∈ C

theorem SetTheory.not_mem_self {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : x ∉ x

theorem SetTheory.exists_separate {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) (p : M → Prop) : IsSet {y : M | y ∈ x ∧ p y}

noncomputable def SetTheory.separate {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) (p : M → Prop) : M

The separate declaration.

Equations

• SetTheory.separate x p = Exists.choose ⋯

@[simp]

theorem SetTheory.mem_separate_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} {p : M → Prop} (z : M) : z ∈ separate x p ↔ z ∈ x ∧ p z

theorem SetTheory.separate_sub {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} {p : M → Prop} : separate x p ⊆ x

theorem SetTheory.isSet_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {C : Set M} : IsSet C ↔ ∃ (x : M), ∀ y ∈ C, y ∈ x

instance SetTheory.instHasEmpty {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : HasEmpty M

theorem SetTheory.empty.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : ∅ = ↓∅

theorem SetTheory.empty.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : ⇓∅ = ∅

theorem SetTheory.mem_vonNeumann_powerset {μ : Ordinal.{u_1}} {x : ZFSet.{u_1}} (hμ : Order.IsSuccLimit μ) (hx : x ∈ ZFSet.vonNeumann μ) : x.powerset ∈ ZFSet.vonNeumann μ

theorem SetTheory.mem_vonNeumann_singleton {μ : Ordinal.{u_1}} {x : ZFSet.{u_1}} (hμ : Order.IsSuccLimit μ) (hx : x ∈ ZFSet.vonNeumann μ) : {x} ∈ ZFSet.vonNeumann μ

theorem SetTheory.mem_vonNeumann_union {μ : Ordinal.{u_1}} {x y : ZFSet.{u_1}} (hx : x ∈ ZFSet.vonNeumann μ) (hy : y ∈ ZFSet.vonNeumann μ) : x ∪ y ∈ ZFSet.vonNeumann μ

theorem SetTheory.powerset.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : IsSet {y : M | y ⊆ x}

@[simp]

theorem SetTheory.powerset.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ y : M) : y ∈ 𝓟 x₁ ↔ y ⊆ x₁

instance SetTheory.powerset.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => 𝓟 (v 0)

noncomputable def SetTheory.powerset {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• 𝓟 x₁ = Exists.choose ⋯

theorem SetTheory.powerset.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : 𝓟 x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.powerset.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : 𝓟 x₁ = v ↔ ∀ (y : M), y ∈ v ↔ y ⊆ x₁

theorem SetTheory.powerset.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ 𝓟 (v✝ 0) = v✝ 1

theorem SetTheory.powerset.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : 𝓟 (j x₁) = j 𝓟 x₁

def SetTheory.term𝓟_ : Lean.ParserDescr

The 𝓟_ declaration.

Equations

• SetTheory.term𝓟_ = Lean.ParserDescr.node `SetTheory.term𝓟_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓟 ") (Lean.ParserDescr.cat `term 1024))

theorem SetTheory.powerset.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : 𝓟 ↓x = ↓𝓟 x

theorem SetTheory.singleton.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : IsSet {y : M | y = x}

instance SetTheory.singleton.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => singleton (v 0)

theorem SetTheory.singleton.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : singleton x₁ = v ↔ ∀ (y : M), y ∈ v ↔ y = x₁

theorem SetTheory.singleton.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : singleton x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.singleton.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ singleton (v✝ 0) = v✝ 1

noncomputable def SetTheory.singleton {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.singleton x₁ = Exists.choose ⋯

theorem SetTheory.singleton.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : singleton (j x₁) = j (singleton x₁)

theorem SetTheory.singleton.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ y : M) : y ∈ singleton x₁ ↔ y = x₁

theorem SetTheory.insert.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : IsSet {z : M | z = x ∨ z ∈ y}

theorem SetTheory.insert.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ x₃ : M) : insert x₁ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

theorem SetTheory.insert.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ v : M) : insert x₁ x₂ = v ↔ ∀ (y : M), y ∈ v ↔ y = x₁ ∨ y ∈ x₂

noncomputable def SetTheory.insert {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.insert x₁ x₂ = Exists.choose ⋯

theorem SetTheory.insert.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ y : M) : y ∈ insert x₁ x₂ ↔ y = x₁ ∨ y ∈ x₂

theorem SetTheory.insert.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ insert (v✝ 0) (v✝ 1) = v✝ 2

instance SetTheory.insert.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => insert (v 0) (v 1)

theorem SetTheory.insert.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : insert (j x₁) (j x₂) = j (insert x₁ x₂)

def LE.le.formula : ZFFormula 2

The formula declaration.

Equations

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

theorem LE.le.realize_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] {v : Fin 2 → M} : FirstOrder.Language.Formula.Realize formula v ↔ v 0 ≤ v 1

theorem LE.le.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : SetTheory.IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₁ ≤ j x₂ ↔ x₁ ≤ x₂

theorem LE.le.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] (x₁ x₂ : M) : x₁ ≤ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

def LT.lt.formula : ZFFormula 2

The formula declaration.

Equations

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

theorem LT.lt.realize_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] {v : Fin 2 → M} : FirstOrder.Language.Formula.Realize formula v ↔ v 0 < v 1

theorem LT.lt.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] (x₁ x₂ : M) : x₁ < x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem LT.lt.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : SetTheory.IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₁ < j x₂ ↔ x₁ < x₂

@[implicit_reducible]

noncomputable instance instSingletonMM {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] : Singleton M M

Equations

• instSingletonMM = { singleton := SetTheory.singleton }

@[simp]

theorem Singleton.singleton.spec {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y : M) : y ∈ {x} ↔ y = x

theorem Singleton.singleton.eq_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y : M) : {x} = y ↔ ∀ (z : M), z ∈ y ↔ z = x

noncomputable def Singleton.singleton.formula : ZFFormula 2

The formula declaration.

Equations

• Singleton.singleton.formula = SetTheory.singleton.formula

theorem Singleton.singleton.realize_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (v : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v ↔ {v 0} = v 1

theorem Singleton.singleton.eu {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x : M) : SetTheory.IsSet {y : M | y = x}

theorem Singleton.singleton.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : SetTheory.IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : {j x₁} = j {x₁}

instance Singleton.singleton.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => {v 0}

theorem Singleton.singleton.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] (x₁ x₂ : M) : {x₁} = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

@[implicit_reducible]

noncomputable instance instInsertMM {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] : Insert M M

Equations

• instInsertMM = { insert := SetTheory.insert }

@[simp]

theorem Insert.insert.spec {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y z : M) : z ∈ insert x y ↔ z = x ∨ z ∈ y

theorem Insert.insert.eq_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y z : M) : insert x y = z ↔ ∀ (w : M), w ∈ z ↔ w = x ∨ w ∈ y

noncomputable def Insert.insert.formula : ZFFormula 3

The formula declaration.

Equations

• Insert.insert.formula = SetTheory.insert.formula

theorem Insert.insert.realize_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (v : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v ↔ insert (v 0) (v 1) = v 2

theorem Insert.insert.eu {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y : M) : SetTheory.IsSet {z : M | z = x ∨ z ∈ y}

theorem Insert.insert.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] (x₁ x₂ x₃ : M) : insert x₁ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

instance Insert.insert.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => insert (v 0) (v 1)

theorem Insert.insert.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : SetTheory.IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : insert (j x₁) (j x₂) = j (insert x₁ x₂)

theorem SetTheory.singleton.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : {↓x} = ↓{x}

theorem SetTheory.singleton.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : ⇓{x} = {⇓x}

theorem SetTheory.mem_singleton {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : x ∈ {x}

theorem SetTheory.singleton_subset_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : {x} ⊆ y ↔ x ∈ y

theorem SetTheory.exists_toZFSet_of_mem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} {y : ZFSet.{0}} (hy : y ∈ ⇓x) : ∃ (z : M), ⇓z = y

theorem SetTheory.exists_toV_of_mem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} {y : V} (hy : y ∈ ↓x) : ∃ (z : M), ↓z = y

theorem SetTheory.insert.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : Insert.insert ↓x ↓y = ↓(Insert.insert x y)

theorem SetTheory.insert.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : ⇓(Insert.insert x y) = Insert.insert ⇓x ⇓y

def SetTheory.ExistsUniqueAt {α : Type u_1} (x : α) (p : α → Prop) : Prop

The ExistsUniqueAt declaration.

Equations

• SetTheory.ExistsUniqueAt x p = (p x ∧ ∀ (y : α), p y → y = x)

theorem SetTheory.isGLB_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {C : Set M} {x : M} : IsGLB C x ↔ ∀ (y : M), y ∈ x ↔ ∀ t ∈ C, y ∈ t

theorem SetTheory.isLUB_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {C : Set M} {x : M} : IsLUB C x ↔ ∀ (y : M), y ∈ x ↔ ∃ t ∈ C, y ∈ t

theorem SetTheory.exists_minimal {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {p : M → Prop} : (∃! x : M, IsGLB {x : M | p x} x) ↔ ∃ (x : M), p x

def SetTheory.IsTransitive {M : Type 1} [ZFStructure M] (X : M) : Prop

The IsTransitive declaration.

Equations

• SetTheory.IsTransitive X = ∀ ⦃x : M⦄, x ∈ X → x ⊆ X

theorem SetTheory.IsTransitive.elementarity {M : Type 1} [sM : ZFStructure M] {N : Type 1} [sN : ZFStructure N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsTransitive (j x₁) ↔ IsTransitive x₁

theorem SetTheory.IsTransitive.to_realize {M : Type 1} [sM : ZFStructure M] (x₁ : M) : IsTransitive x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

theorem SetTheory.IsTransitive.realize_iff {M : Type 1} [sM : ZFStructure M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsTransitive (v✝ 0)

theorem SetTheory.IsTransitive.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (α : M) : IsTransitive ↓α ↔ IsTransitive α

theorem SetTheory.IsTransitive.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (α : M) : IsTransitive α ↔ (⇓α).IsTransitive

noncomputable def SetTheory.enoughTransitive {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : { y : M // IsTransitive y ∧ x ⊆ y }

The enoughTransitive declaration.

Equations

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

theorem SetTheory.toZFSet_enoughTransitive {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : ⇓↑(enoughTransitive x) = ZFSet.vonNeumann (⇓x).rank

theorem SetTheory.trcl.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : ∃! y : M, IsGLB {t : M | IsTransitive t ∧ x ⊆ t} y

noncomputable def SetTheory.trcl {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.trcl x₁ = Exists.choose ⋯

theorem SetTheory.trcl.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsGLB {t : M | IsTransitive t ∧ x₁ ⊆ t} (trcl x₁)

theorem SetTheory.trcl.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ trcl (v✝ 0) = v✝ 1

theorem SetTheory.trcl.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : trcl (j x₁) = j (trcl x₁)

theorem SetTheory.trcl.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : trcl x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

instance SetTheory.trcl.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => trcl (v 0)

theorem SetTheory.trcl.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : trcl x₁ = v ↔ IsGLB {t : M | IsTransitive t ∧ x₁ ⊆ t} v

theorem SetTheory.mem_trcl_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : y ∈ trcl x ↔ ∀ (t : M), IsTransitive t ∧ x ⊆ t → y ∈ t

theorem SetTheory.isTransitive_trcl {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : IsTransitive (trcl x)

theorem SetTheory.trcl_trans {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y z : M} (hz : z ∈ y) (hy : y ∈ trcl x) : z ∈ trcl x

theorem SetTheory.sub_trcl {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x : M} : x ⊆ trcl x

theorem SetTheory.trcl_sub {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} (hx : IsTransitive y) (sub : x ⊆ y) : trcl x ⊆ y

theorem SetTheory.union.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : IsSet {z : M | z ∈ x ∨ z ∈ y}

theorem SetTheory.union.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : union (j x₁) (j x₂) = j (union x₁ x₂)

theorem SetTheory.union.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ x₃ : M) : union x₁ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

instance SetTheory.union.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => union (v 0) (v 1)

theorem SetTheory.union.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ y : M) : y ∈ union x₁ x₂ ↔ y ∈ x₁ ∨ y ∈ x₂

noncomputable def SetTheory.union {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.union x₁ x₂ = Exists.choose ⋯

theorem SetTheory.union.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ v : M) : union x₁ x₂ = v ↔ ∀ (y : M), y ∈ v ↔ y ∈ x₁ ∨ y ∈ x₂

theorem SetTheory.union.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ union (v✝ 0) (v✝ 1) = v✝ 2

theorem SetTheory.inter.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : IsSet {z : M | z ∈ x ∧ z ∈ y}

instance SetTheory.inter.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => inter (v 0) (v 1)

noncomputable def SetTheory.inter {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.inter x₁ x₂ = Exists.choose ⋯

theorem SetTheory.inter.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ y : M) : y ∈ inter x₁ x₂ ↔ y ∈ x₁ ∧ y ∈ x₂

theorem SetTheory.inter.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ x₃ : M) : inter x₁ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

theorem SetTheory.inter.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ v : M) : inter x₁ x₂ = v ↔ ∀ (y : M), y ∈ v ↔ y ∈ x₁ ∧ y ∈ x₂

theorem SetTheory.inter.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ inter (v✝ 0) (v✝ 1) = v✝ 2

theorem SetTheory.inter.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : inter (j x₁) (j x₂) = j (inter x₁ x₂)

@[implicit_reducible]

noncomputable instance instUnionM {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] : Union M

Equations

• instUnionM = { union := SetTheory.union }

@[simp]

theorem Union.union.spec {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y z : M) : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

theorem Union.union.eq_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y z : M) : x ∪ y = z ↔ ∀ (w : M), w ∈ z ↔ w ∈ x ∨ w ∈ y

noncomputable def Union.union.formula : ZFFormula 3

The formula declaration.

Equations

• Union.union.formula = SetTheory.union.formula

theorem Union.union.realize_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (v : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v ↔ v 0 ∪ v 1 = v 2

theorem Union.union.eu {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y : M) : SetTheory.IsSet {z : M | z ∈ x ∨ z ∈ y}

instance Union.union.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => v 0 ∪ v 1

theorem Union.union.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] (x₁ x₂ x₃ : M) : x₁ ∪ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

theorem Union.union.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : SetTheory.IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₁ ∪ j x₂ = j (x₁ ∪ x₂)

@[implicit_reducible]

noncomputable instance instInterM {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] : Inter M

Equations

• instInterM = { inter := SetTheory.inter }

@[simp]

theorem Inter.inter.spec {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y z : M) : z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

theorem Inter.inter.eq_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y z : M) : x ∩ y = z ↔ ∀ (w : M), w ∈ z ↔ w ∈ x ∧ w ∈ y

noncomputable def Inter.inter.formula : ZFFormula 3

The formula declaration.

Equations

• Inter.inter.formula = SetTheory.inter.formula

theorem Inter.inter.realize_iff {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (v : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v ↔ v 0 ∩ v 1 = v 2

theorem Inter.inter.eu {M : Type 1} [ZFStructure M] [hM : SetTheory.IsVonNeumann M] (x y : M) : SetTheory.IsSet {z : M | z ∈ x ∧ z ∈ y}

theorem Inter.inter.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : SetTheory.IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : j x₁ ∩ j x₂ = j (x₁ ∩ x₂)

theorem Inter.inter.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] (x₁ x₂ x₃ : M) : x₁ ∩ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

instance Inter.inter.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : SetTheory.IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => v 0 ∩ v 1

theorem SetTheory.union.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : ↓x ∪ ↓y = ↓(x ∪ y)

theorem SetTheory.union.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : ⇓(x ∪ y) = ⇓x ∪ ⇓y

@[implicit_reducible]

noncomputable instance SetTheory.instInfSetM {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : InfSet M

Equations

• SetTheory.instInfSetM = { sInf := fun (s : Set M) => if hs : s.Nonempty then SetTheory.separate hs.some fun (x : M) => ∀ t ∈ s, x ∈ t else ∅ }

@[implicit_reducible]

noncomputable instance SetTheory.instConditionallyCompleteLatticeM {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : ConditionallyCompleteLattice M

Equations

• SetTheory.instConditionallyCompleteLatticeM = conditionallyCompleteLatticeOfsInf M ⋯ ⋯ ⋯

@[implicit_reducible]

noncomputable instance SetTheory.instOrderBotM {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : OrderBot M

Equations

• SetTheory.instOrderBotM = { bot := ∅, bot_le := ⋯ }

theorem SetTheory.succ.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : ∃! y : M, y = Insert.insert x x

noncomputable def SetTheory.succ {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.succ x₁ = Exists.choose ⋯

theorem SetTheory.succ.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : succ x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.succ.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ succ (v✝ 0) = v✝ 1

theorem SetTheory.succ.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : succ x₁ = Insert.insert x₁ x₁

theorem SetTheory.succ.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : succ (j x₁) = j (succ x₁)

instance SetTheory.succ.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => succ (v 0)

theorem SetTheory.succ.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : succ x₁ = v ↔ v = Insert.insert x₁ x₁

theorem SetTheory.succ.toV {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (α : M) : succ ↓α = ↓(succ α)

theorem SetTheory.succ.toZFSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (α : M) : ⇓(succ α) = Insert.insert ⇓α ⇓α

@[simp]

theorem SetTheory.lt_succ {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {α : M} : α < succ α

theorem SetTheory.pair.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : ∃! z : M, z = {{x}, {x, y}}

theorem SetTheory.pair.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ ⸨v✝ 0, v✝ 1⸩ = v✝ 2

noncomputable def SetTheory.pair {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• ⸨x₁, x₂⸩ = Exists.choose ⋯

theorem SetTheory.pair.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : ⸨j x₁, j x₂⸩ = j ⸨x₁, x₂⸩

theorem SetTheory.pair.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ x₃ : M) : ⸨x₁, x₂⸩ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

theorem SetTheory.pair.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : ⸨x₁, x₂⸩ = {{x₁}, {x₁, x₂}}

theorem SetTheory.pair.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ v : M) : ⸨x₁, x₂⸩ = v ↔ v = {{x₁}, {x₁, x₂}}

instance SetTheory.pair.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => ⸨v 0, v 1⸩

def SetTheory.«term⸨_,_⸩» : Lean.ParserDescr

The ⸨_,_⸩ notation.

Equations

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

def SetTheory.IsPair {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (z : M) : Prop

The IsPair declaration.

Equations

• SetTheory.IsPair z = ∃ (x : M) (y : M), z = ⸨x, y⸩

theorem SetTheory.IsPair.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsPair (j x₁) ↔ IsPair x₁

theorem SetTheory.IsPair.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsPair x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

theorem SetTheory.IsPair.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsPair (v✝ 0)

@[simp]

theorem SetTheory.isPair_pair {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y : M} : IsPair ⸨x, y⸩

theorem SetTheory.fst_aux {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y z : M} (hz : z = ⸨x, y⸩) : ExistsUniqueAt x fun (x : M) => ∀ w ∈ z, x ∈ w

theorem SetTheory.fst.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {z : M} (hz : IsPair z) : ∃! x : M, ∀ w ∈ z, x ∈ w

noncomputable def SetTheory.fst {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.fst x₁ = if h₁ : SetTheory.IsPair x₁ then Exists.choose ⋯ else ∅

theorem SetTheory.fst.realize_iff {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ fst (v✝ 0) = v✝ 1

theorem SetTheory.fst.elementarity {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [HasEmpty N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : fst (j x₁) = j (fst x₁)

instance SetTheory.fst.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => fst (v 0)

theorem SetTheory.fst.eq_iff {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ : M) (h₁ : IsPair x₁) (v : M) : fst x₁ = v ↔ ∀ w ∈ x₁, v ∈ w

theorem SetTheory.fst.spec {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ : M) (h₁ : IsPair x₁) (w : M) ([anonymous] : w ∈ x₁) : SetTheory.fst✝ x₁ ∈ w

theorem SetTheory.fst.to_realize {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : fst x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

@[simp]

theorem SetTheory.fst_pair {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : fst ⸨x, y⸩ = x

theorem SetTheory.pair_eq_singleton_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y z : M} : {x, y} = {z} ↔ x = z ∧ y = z

theorem SetTheory.snd_aux {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {x y z : M} (hz : z = ⸨x, y⸩) : ExistsUniqueAt y fun (y : M) => (∃ w ∈ z, y ∈ w) ∧ ((∀ w ∈ z, y ∈ w) → ∀ a ∈ z, ∀ b ∈ z, a = b)

theorem SetTheory.snd.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {z : M} (hz : IsPair z) : ∃! x : M, (∃ w ∈ z, x ∈ w) ∧ ((∀ w ∈ z, x ∈ w) → ∀ x ∈ z, ∀ y ∈ z, x = y)

theorem SetTheory.snd.to_realize {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : snd x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

instance SetTheory.snd.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => snd (v 0)

noncomputable def SetTheory.snd {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.snd x₁ = if h₁ : SetTheory.IsPair x₁ then Exists.choose ⋯ else ∅

theorem SetTheory.snd.spec {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ : M) (h₁ : IsPair x₁) : (∃ w ∈ x₁, snd x₁ ∈ w) ∧ ((∀ w ∈ x₁, snd x₁ ∈ w) → ∀ x ∈ x₁, ∀ y ∈ x₁, x = y)

theorem SetTheory.snd.eq_iff {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ : M) (h₁ : IsPair x₁) (v : M) : snd x₁ = v ↔ (∃ w ∈ x₁, v ∈ w) ∧ ((∀ w ∈ x₁, v ∈ w) → ∀ x ∈ x₁, ∀ y ∈ x₁, x = y)

theorem SetTheory.snd.elementarity {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [HasEmpty N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : snd (j x₁) = j (snd x₁)

theorem SetTheory.snd.realize_iff {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ snd (v✝ 0) = v✝ 1

@[simp]

theorem SetTheory.snd_pair {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : snd ⸨x, y⸩ = y

@[simp]

theorem SetTheory.pair_eta {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {z : M} (hz : IsPair z) : ⸨fst z, snd z⸩ = z

theorem SetTheory.singleton_mem_pair {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : {x} ∈ ⸨x, y⸩

theorem SetTheory.unordered_pair_mem_pair {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : {x, y} ∈ ⸨x, y⸩

theorem SetTheory.Pairs.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (A B : M) : IsSet {x : M | IsPair x ∧ fst x ∈ A ∧ snd x ∈ B}

theorem SetTheory.Pairs.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ v : M) : Pairs x₁ x₂ = v ↔ ∀ (y : M), y ∈ v ↔ IsPair y ∧ fst y ∈ x₁ ∧ snd y ∈ x₂

@[simp]

theorem SetTheory.Pairs.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ y : M) : y ∈ Pairs x₁ x₂ ↔ IsPair y ∧ fst y ∈ x₁ ∧ snd y ∈ x₂

theorem SetTheory.Pairs.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : Pairs (j x₁) (j x₂) = j (Pairs x₁ x₂)

theorem SetTheory.Pairs.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ x₃ : M) : Pairs x₁ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

noncomputable def SetTheory.Pairs {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.Pairs x₁ x₂ = Exists.choose ⋯

instance SetTheory.Pairs.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => Pairs (v 0) (v 1)

theorem SetTheory.Pairs.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ Pairs (v✝ 0) (v✝ 1) = v✝ 2

def SetTheory.IsRelation {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (r : M) : Prop

The IsRelation declaration.

Equations

• SetTheory.IsRelation r = ∀ ⦃x : M⦄, x ∈ r → SetTheory.IsPair x

theorem SetTheory.IsRelation.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsRelation (v✝ 0)

theorem SetTheory.IsRelation.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsRelation (j x₁) ↔ IsRelation x₁

theorem SetTheory.IsRelation.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsRelation x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

def SetTheory.IsFunc {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (f : M) : Prop

The IsFunc declaration.

Equations

• SetTheory.IsFunc f = (SetTheory.IsRelation f ∧ ∀ ⦃x y z : M⦄, ⸨x, y⸩ ∈ f → ⸨x, z⸩ ∈ f → y = z)

theorem SetTheory.IsFunc.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsFunc x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

theorem SetTheory.IsFunc.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsFunc (v✝ 0)

theorem SetTheory.IsFunc.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsFunc (j x₁) ↔ IsFunc x₁

theorem SetTheory.Dom.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (f : M) : IsSet {x : M | ∃ (y : M), ⸨x, y⸩ ∈ f}

theorem SetTheory.Dom.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : Dom x₁ = v ↔ ∀ (y : M), y ∈ v ↔ ∃ (y_1 : M), ⸨y, y_1⸩ ∈ x₁

theorem SetTheory.Dom.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ Dom (v✝ 0) = v✝ 1

instance SetTheory.Dom.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => Dom (v 0)

noncomputable def SetTheory.Dom {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.Dom x₁ = Exists.choose ⋯

theorem SetTheory.Dom.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ y : M) : y ∈ Dom x₁ ↔ ∃ (y_1 : M), ⸨y, y_1⸩ ∈ x₁

theorem SetTheory.Dom.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : Dom x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.Dom.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : Dom (j x₁) = j (Dom x₁)

theorem SetTheory.Ran.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (f : M) : IsSet {y : M | ∃ (x : M), ⸨x, y⸩ ∈ f}

noncomputable def SetTheory.Ran {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.Ran x₁ = Exists.choose ⋯

theorem SetTheory.Ran.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ y : M) : y ∈ Ran x₁ ↔ ∃ (x : M), ⸨x, y⸩ ∈ x₁

theorem SetTheory.Ran.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : Ran x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.Ran.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : Ran x₁ = v ↔ ∀ (y : M), y ∈ v ↔ ∃ (x : M), ⸨x, y⸩ ∈ x₁

theorem SetTheory.Ran.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : Ran (j x₁) = j (Ran x₁)

instance SetTheory.Ran.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => Ran (v 0)

theorem SetTheory.Ran.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ Ran (v✝ 0) = v✝ 1

theorem SetTheory.func_sub_pairs {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B f : M} (hf : IsFunc f ∧ Dom f = A ∧ Ran f ⊆ B) : f ⊆ Pairs A B

theorem SetTheory.Func.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (A B : M) : IsSet {f : M | IsFunc f ∧ Dom f = A ∧ Ran f ⊆ B}

noncomputable def SetTheory.Func {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.Func x₁ x₂ = Exists.choose ⋯

theorem SetTheory.Func.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ v : M) : Func x₁ x₂ = v ↔ ∀ (y : M), y ∈ v ↔ IsFunc y ∧ Dom y = x₁ ∧ Ran y ⊆ x₂

theorem SetTheory.Func.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ Func (v✝ 0) (v✝ 1) = v✝ 2

theorem SetTheory.Func.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ y : M) : y ∈ Func x₁ x₂ ↔ IsFunc y ∧ Dom y = x₁ ∧ Ran y ⊆ x₂

instance SetTheory.Func.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => Func (v 0) (v 1)

theorem SetTheory.Func.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : Func (j x₁) (j x₂) = j (Func x₁ x₂)

theorem SetTheory.Func.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ x₃ : M) : Func x₁ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

theorem SetTheory.apply.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {f x : M} (hf : IsFunc f) (hx : x ∈ Dom f) : ∃! y : M, ⸨x, y⸩ ∈ f

theorem SetTheory.apply.realize_iff {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (v✝ : Fin 3 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ apply (v✝ 0) (v✝ 1) = v✝ 2

instance SetTheory.apply.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 2 → M) => apply (v 0) (v 1)

theorem SetTheory.apply.eq_iff {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) (h₁ : IsFunc x₁) (h₂ : x₂ ∈ Dom x₁) (v : M) : apply x₁ x₂ = v ↔ ⸨x₂, v⸩ ∈ x₁

theorem SetTheory.apply.to_realize {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ x₂ x₃ : M) : apply x₁ x₂ = x₃ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂, x₃]

theorem SetTheory.apply.elementarity {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [HasEmpty N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : apply (j x₁) (j x₂) = j (apply x₁ x₂)

theorem SetTheory.apply.spec {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) (h₁ : IsFunc x₁) (h₂ : x₂ ∈ Dom x₁) : ⸨x₂, apply x₁ x₂⸩ ∈ x₁

noncomputable def SetTheory.apply {M : Type 1} [sM : ZFStructure M] [HasEmpty M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.apply x₁ x₂ = if h₁ : SetTheory.IsFunc x₁ then if h₂ : x₂ ∈ SetTheory.Dom x₁ then Exists.choose ⋯ else ∅ else ∅

def SetTheory.PreserveMem {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (f : M) : Prop

The PreserveMem declaration.

Equations

• SetTheory.PreserveMem f = ∀ x ∈ SetTheory.Dom f, ∀ y ∈ SetTheory.Dom f, x ∈ y → SetTheory.apply f x ∈ SetTheory.apply f y

theorem SetTheory.PreserveMem.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ PreserveMem (v✝ 0)

theorem SetTheory.PreserveMem.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : PreserveMem x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

theorem SetTheory.PreserveMem.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : PreserveMem (j x₁) ↔ PreserveMem x₁

noncomputable def SetTheory.funcToSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} (f : ↥A → ↥B) : M

The funcToSet declaration.

Equations

• SetTheory.funcToSet f = SetTheory.separate (SetTheory.Pairs A B) fun (x : M) => ∃ (hx : SetTheory.fst x ∈ A), ↑(f ⟨SetTheory.fst x, hx⟩) = SetTheory.snd x

@[simp]

theorem SetTheory.isFunc_funcToSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} : IsFunc (funcToSet f)

@[simp]

theorem SetTheory.dom_funcToSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} : Dom (funcToSet f) = A

theorem SetTheory.mem_Ran_funcToSet_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} (y : M) : y ∈ Ran (funcToSet f) ↔ ∃ (x : M) (hx : x ∈ A), ↑(f ⟨x, hx⟩) = y

theorem SetTheory.ran_funcToSet_sub {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} : Ran (funcToSet f) ⊆ B

theorem SetTheory.funcToSet_mem_Func {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} (f : ↥A → ↥B) : funcToSet f ∈ Func A B

theorem SetTheory.apply_mem_Ran {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {f x : M} (hf : IsFunc f) (hx : x ∈ Dom f) : apply f x ∈ Ran f

noncomputable def SetTheory.setToFunc {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} (f : ↥(Func A B)) : ↥A → ↥B

The setToFunc declaration.

Equations

• SetTheory.setToFunc f = fun (x : ↥A) => match x with | ⟨x, hx⟩ => ⟨SetTheory.apply (↑f) x, ⋯⟩

theorem SetTheory.apply_funcToSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} (f : ↥A → ↥B) {x : M} (hx : x ∈ A) : apply (funcToSet f) x = ↑(f ⟨x, hx⟩)

theorem SetTheory.apply_funcToSet_rev {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} (f : ↥A → ↥B) {x : ↥A} : ↑(f x) = apply (funcToSet f) ↑x

theorem SetTheory.setToFunc_funcToSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} : setToFunc ⟨funcToSet f, ⋯⟩ = f

theorem SetTheory.funcToSet_setToFunc {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} (f : ↥(Func A B)) : funcToSet (setToFunc f) = ↑f

noncomputable def SetTheory.funcEquiv {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} : ↥(Func A B) ≃ (↥A → ↥B)

The funcEquiv declaration.

Equations

• SetTheory.funcEquiv = { toFun := fun (f : ↥(SetTheory.Func A B)) => SetTheory.setToFunc f, invFun := fun (f : ↥A → ↥B) => ⟨SetTheory.funcToSet f, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem SetTheory.forall_func {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {p : M → Prop} : (∀ f ∈ Func A B, p f) ↔ ∀ (f : ↥A → ↥B), p (funcToSet f)

theorem SetTheory.exists_func {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {p : M → Prop} : (∃ f ∈ Func A B, p f) ↔ ∃ (f : ↥A → ↥B), p (funcToSet f)

theorem SetTheory.subset_func {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {f g : M} (hf : IsFunc f) (hg : IsFunc g) (dom_sub : Dom f ⊆ Dom g) (ext : ∀ x ∈ Dom f, apply f x = apply g x) : f ⊆ g

theorem SetTheory.ext_func {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {f g : M} (hf : IsFunc f) (hg : IsFunc g) (dom_eq : Dom f = Dom g) (ext : ∀ x ∈ Dom f, apply f x = apply g x) : f = g

@[simp]

theorem SetTheory.sSup_empty {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : sSup ∅ = ∅

@[simp]

theorem SetTheory.sInf_empty {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] : sInf ∅ = ∅

def SetTheory.IsInjective {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (f : M) : Prop

The IsInjective declaration.

Equations

• SetTheory.IsInjective f = (SetTheory.IsFunc f ∧ ∀ x ∈ SetTheory.Dom f, ∀ y ∈ SetTheory.Dom f, SetTheory.apply f x = SetTheory.apply f y → x = y)

theorem SetTheory.IsInjective.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : IsInjective x₁ ↔ FirstOrder.Language.Formula.Realize formula ![x₁]

theorem SetTheory.IsInjective.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsInjective (j x₁) ↔ IsInjective x₁

theorem SetTheory.IsInjective.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 1 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsInjective (v✝ 0)

@[simp]

theorem SetTheory.isInjective_funcToSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} : IsInjective (funcToSet f) ↔ Function.Injective f

theorem SetTheory.nonempty_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x : M) : Nonempty ↥x ↔ x ≠ ∅

def SetTheory.cardLE {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : Prop

The cardLE declaration.

Equations

• SetTheory.cardLE x y = ∃ f ∈ SetTheory.Func x y, SetTheory.IsInjective f

theorem SetTheory.cardLE.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : cardLE (j x₁) (j x₂) ↔ cardLE x₁ x₂

theorem SetTheory.cardLE.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : cardLE x₁ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.cardLE.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ cardLE (v✝ 0) (v✝ 1)

def SetTheory.cardEq {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : Prop

The cardEq declaration.

Equations

• SetTheory.cardEq x y = ∃ f ∈ SetTheory.Func x y, SetTheory.IsInjective f ∧ SetTheory.Ran f = y

theorem SetTheory.cardEq.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : cardEq x₁ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.cardEq.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ cardEq (v✝ 0) (v✝ 1)

theorem SetTheory.cardEq.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : cardEq (j x₁) (j x₂) ↔ cardEq x₁ x₂

def SetTheory.cardLT {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : Prop

The cardLT declaration.

Equations

• SetTheory.cardLT x y = (SetTheory.cardLE x y ∧ ¬SetTheory.cardEq x y)

theorem SetTheory.cardLT.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : cardLT x₁ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.cardLT.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ cardLT (v✝ 0) (v✝ 1)

theorem SetTheory.cardLT.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : cardLT (j x₁) (j x₂) ↔ cardLT x₁ x₂

theorem SetTheory.cardLE_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : cardLE x y ↔ Cardinal.mk ↥x ≤ Cardinal.mk ↥y

theorem SetTheory.ran_funcToSet_eq {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} : Ran (funcToSet f) = B ↔ Function.Surjective f

theorem SetTheory.cardEq_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : cardEq x y ↔ Cardinal.mk ↥x = Cardinal.mk ↥y

theorem SetTheory.cardLT_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (x y : M) : cardLT x y ↔ Cardinal.mk ↥x < Cardinal.mk ↥y

theorem SetTheory.iUnion.eu {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (f : M) : IsSet {y : M | ∃ x ∈ Ran f, y ∈ x}

theorem SetTheory.iUnion.eq_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ v : M) : iUnion x₁ = v ↔ ∀ (y : M), y ∈ v ↔ ∃ x ∈ Ran x₁, y ∈ x

theorem SetTheory.iUnion.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ x₂ : M) : iUnion x₁ = x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

noncomputable def SetTheory.iUnion {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ : M) : M

The set-theoretic function automatically realized from its defining property.

Equations

• SetTheory.iUnion x₁ = Exists.choose ⋯

theorem SetTheory.iUnion.spec {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (x₁ y : M) : y ∈ iUnion x₁ ↔ ∃ x ∈ Ran x₁, y ∈ x

theorem SetTheory.iUnion.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumann N] (x₁ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : iUnion (j x₁) = j (iUnion x₁)

instance SetTheory.iUnion.instFormulaToFunction {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] : FormulaToFunction formula fun (v : Fin 1 → M) => iUnion (v 0)

theorem SetTheory.iUnion.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumann M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ iUnion (v✝ 0) = v✝ 1

theorem SetTheory.mem_sSup_iff {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {C : Set M} {x : M} (hC : BddAbove C) : x ∈ sSup C ↔ ∃ t ∈ C, x ∈ t

theorem SetTheory.iUnion_funcToSet {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {A B : M} {f : ↥A → ↥B} : iUnion (funcToSet f) = ⨆ (x : ↥A), ↑(f x)