Zermelo set theory

reference: Ralf Schindler, "Set Theory, Exploring Independence and Truth" [Sch14]

Axiom of extentionality

theorem LO.FirstOrder.SetTheory.mem_ext_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x = y ↔ ∀ (z : V), z ∈ x ↔ z ∈ y

theorem LO.FirstOrder.SetTheory.mem_ext {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : (∀ (z : V), z ∈ x ↔ z ∈ y) → x = y

Alias of the reverse direction of LO.FirstOrder.SetTheory.mem_ext_iff.

theorem LO.FirstOrder.SetTheory.subset_antisymm {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y

theorem LO.FirstOrder.SetTheory.subset_antisymm_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x ⊆ y ∧ y ⊆ x ↔ x = y

theorem LO.FirstOrder.SetTheory.SSubset.iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x ⊊ y ↔ x ⊆ y ∧ ∃ z ∈ y, z ∉ x

theorem LO.FirstOrder.SetTheory.SSubset.exists_not_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} (hxy : x ⊊ y) : ∃ z ∈ y, z ∉ x

theorem LO.FirstOrder.SetTheory.SSubset.of_subset_of_not_mem_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} (ss : x ⊆ y) (hzx : z ∉ x) (hzy : z ∈ y) : x ⊊ y

Axiom of empty set

theorem LO.FirstOrder.SetTheory.empty_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ∃ (e : V), IsEmpty e

theorem LO.FirstOrder.SetTheory.empty_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ∃! e : V, IsEmpty e

@[implicit_reducible]

noncomputable def LO.FirstOrder.SetTheory.instEmptyCollection {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : EmptyCollection V

Equations

• LO.FirstOrder.SetTheory.instEmptyCollection = { emptyCollection := Classical.choose! ⋯ }

@[simp]

theorem LO.FirstOrder.SetTheory.IsEmpty.empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : IsEmpty ∅

@[simp]

theorem LO.FirstOrder.SetTheory.not_mem_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x : V} : x ∉ ∅

@[simp]

theorem LO.FirstOrder.SetTheory.isEmpty_iff_eq_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x : V} : IsEmpty x ↔ x = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.ne_empty_iff_isNonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x : V} : x ≠ ∅ ↔ IsNonempty x

theorem LO.FirstOrder.SetTheory.eq_empty_or_isNonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x = ∅ ∨ IsNonempty x

@[simp]

theorem LO.FirstOrder.SetTheory.empty_subset {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∅ ⊆ x

@[simp]

theorem LO.FirstOrder.SetTheory.subset_empty_iff_eq_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x : V} : x ⊆ ∅ ↔ x = ∅

Axiom of pairing

theorem LO.FirstOrder.SetTheory.pairing_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : ∃ (z : V), ∀ (w : V), w ∈ z ↔ w = x ∨ w = y

theorem LO.FirstOrder.SetTheory.pairing_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : ∃! z : V, ∀ (w : V), w ∈ z ↔ w = x ∨ w = y

noncomputable def LO.FirstOrder.SetTheory.doubleton {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : V

Equations

• LO.FirstOrder.SetTheory.doubleton x y = Classical.choose! ⋯

@[simp]

theorem LO.FirstOrder.SetTheory.mem_doubleton_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} : z ∈ doubleton x y ↔ z = x ∨ z = y

def LO.FirstOrder.SetTheory.doubleton.dfn : Semisentence ℒₛₑₜ 3

Equations

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

instance LO.FirstOrder.SetTheory.doubleton.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₂ doubleton dfn

instance LO.FirstOrder.SetTheory.doubleton.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₂ doubleton

@[simp]

instance LO.FirstOrder.SetTheory.doubleton_isNonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : IsNonempty (doubleton x y)

noncomputable def LO.FirstOrder.SetTheory.singleton {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : V

Equations

• LO.FirstOrder.SetTheory.singleton x = LO.FirstOrder.SetTheory.doubleton x x

@[implicit_reducible]

noncomputable def LO.FirstOrder.SetTheory.instSingleton {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : Singleton V V

Equations

• LO.FirstOrder.SetTheory.instSingleton = { singleton := LO.FirstOrder.SetTheory.singleton }

theorem LO.FirstOrder.SetTheory.singleton_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : {x} = doubleton x x

@[simp]

theorem LO.FirstOrder.SetTheory.mem_singleton_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x z : V} : z ∈ {x} ↔ z = x

def LO.FirstOrder.SetTheory.singleton.dfn : Semisentence ℒₛₑₜ 2

Equations

• LO.FirstOrder.SetTheory.singleton.dfn = LO.FirstOrder.SetTheory.doubleton.dfn/[LO.FirstOrder.Semiterm.bvar 0, LO.FirstOrder.Semiterm.bvar 1, LO.FirstOrder.Semiterm.bvar 1]

instance LO.FirstOrder.SetTheory.singleton.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₁ Singleton.singleton dfn

instance LO.FirstOrder.SetTheory.singleton.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₁ Singleton.singleton

@[simp]

instance LO.FirstOrder.SetTheory.singleton_isNonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : IsNonempty {x}

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_subset_iff_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : {x} ⊆ y ↔ x ∈ y

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_ext_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : {x} = {y} ↔ x = y

Axiom of union

theorem LO.FirstOrder.SetTheory.union_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∃ (y : V), ∀ (z : V), z ∈ y ↔ ∃ w ∈ x, z ∈ w

theorem LO.FirstOrder.SetTheory.union_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∃! y : V, ∀ (z : V), z ∈ y ↔ ∃ w ∈ x, z ∈ w

noncomputable def LO.FirstOrder.SetTheory.sUnion {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : V

Equations

• ⋃ˢ x = Classical.choose! ⋯

def LO.FirstOrder.SetTheory.«term⋃ˢ_» : Lean.ParserDescr

Equations

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

theorem LO.FirstOrder.SetTheory.mem_sUnion_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x z : V} : z ∈ ⋃ˢ x ↔ ∃ y ∈ x, z ∈ y

def LO.FirstOrder.SetTheory.sUnion.dfn : Semisentence ℒₛₑₜ 2

Equations

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

instance LO.FirstOrder.SetTheory.sUnion.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₁ sUnion dfn

instance LO.FirstOrder.SetTheory.sUnion.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₁ sUnion

@[simp]

theorem LO.FirstOrder.SetTheory.sUnion_empty_eq_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ⋃ˢ ∅ = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.sUnion_singleton_eq {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ⋃ˢ {x} = x

@[simp]

theorem LO.FirstOrder.SetTheory.IsNonempty_sUnion_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x : V} : IsNonempty (⋃ˢ x) ↔ ∃ y ∈ x, IsNonempty y

theorem LO.FirstOrder.SetTheory.subset_sUnion_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} (h : x ∈ y) : x ⊆ ⋃ˢ y

Union of two sets

noncomputable def LO.FirstOrder.SetTheory.union {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : V

Equations

• LO.FirstOrder.SetTheory.union x y = ⋃ˢ LO.FirstOrder.SetTheory.doubleton x y

@[implicit_reducible]

noncomputable def LO.FirstOrder.SetTheory.instUnion {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : Union V

Equations

• LO.FirstOrder.SetTheory.instUnion = { union := LO.FirstOrder.SetTheory.union }

theorem LO.FirstOrder.SetTheory.union_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : x ∪ y = ⋃ˢ doubleton x y

def LO.FirstOrder.SetTheory.union.dfn : Semisentence ℒₛₑₜ 3

Equations

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

instance LO.FirstOrder.SetTheory.union.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₂ Union.union dfn

instance LO.FirstOrder.SetTheory.union.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₂ Union.union

@[simp]

theorem LO.FirstOrder.SetTheory.mem_union_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

@[simp]

theorem LO.FirstOrder.SetTheory.union_self_eq {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∪ x = x

theorem LO.FirstOrder.SetTheory.union_comm {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : x ∪ y = y ∪ x

theorem LO.FirstOrder.SetTheory.union_assoc {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y z : V) : x ∪ y ∪ z = x ∪ (y ∪ z)

@[simp]

theorem LO.FirstOrder.SetTheory.union_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∪ ∅ = x

@[simp]

theorem LO.FirstOrder.SetTheory.empty_union {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∅ ∪ x = x

@[simp]

theorem LO.FirstOrder.SetTheory.IsNonempty_union_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : IsNonempty (x ∪ y) ↔ IsNonempty x ∨ IsNonempty y

@[simp]

theorem LO.FirstOrder.SetTheory.subset_union_left {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : x ⊆ x ∪ y

@[simp]

theorem LO.FirstOrder.SetTheory.subset_union_right {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : y ⊆ x ∪ y

@[simp]

theorem LO.FirstOrder.SetTheory.union_eq_iff_right {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x ∪ y = x ↔ y ⊆ x

@[simp]

theorem LO.FirstOrder.SetTheory.union_eq_iff_left {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x ∪ y = y ↔ x ⊆ y

Insert

noncomputable def LO.FirstOrder.SetTheory.insert {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : V

Equations

• LO.FirstOrder.SetTheory.insert x y = {x} ∪ y

@[implicit_reducible]

noncomputable def LO.FirstOrder.SetTheory.instInsert {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : Insert V V

Equations

• LO.FirstOrder.SetTheory.instInsert = { insert := LO.FirstOrder.SetTheory.insert }

theorem LO.FirstOrder.SetTheory.insert_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : insert x y = {x} ∪ y

def LO.FirstOrder.SetTheory.insert.dfn : Semisentence ℒₛₑₜ 3

Equations

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

instance LO.FirstOrder.SetTheory.insert.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₂ insert dfn

instance LO.FirstOrder.SetTheory.insert.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₂ insert

@[simp]

theorem LO.FirstOrder.SetTheory.mem_insert {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} : z ∈ insert x y ↔ z = x ∨ z ∈ y

@[simp]

theorem LO.FirstOrder.SetTheory.insert_empty_eq {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : insert x ∅ = {x}

theorem LO.FirstOrder.SetTheory.union_insert {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {z : V} (x y : V) : x ∪ insert y z = insert y (x ∪ z)

theorem LO.FirstOrder.SetTheory.pair_eq_doubleton {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : {x, y} = doubleton x y

@[simp]

theorem LO.FirstOrder.SetTheory.sUnion_insert {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : ⋃ˢ insert x y = x ∪ ⋃ˢ y

@[simp]

theorem LO.FirstOrder.SetTheory.subset_insert {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : y ⊆ insert x y

@[simp]

instance LO.FirstOrder.SetTheory.insert_isNonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : IsNonempty (insert x y)

@[simp]

theorem LO.FirstOrder.SetTheory.intsert_union {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y z : V) : insert x y ∪ z = insert x (y ∪ z)

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_inter {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : {x} ∪ y = insert x y

@[simp]

theorem LO.FirstOrder.SetTheory.insert_eq_self_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} (hx : x ∈ y) : insert x y = y

Axiom of power set

theorem LO.FirstOrder.SetTheory.power_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∃ (y : V), ∀ (z : V), z ∈ y ↔ z ⊆ x

theorem LO.FirstOrder.SetTheory.power_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∃! y : V, ∀ (z : V), z ∈ y ↔ z ⊆ x

noncomputable def LO.FirstOrder.SetTheory.power {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : V

Equations

• ℘ x = Classical.choose! ⋯

def LO.FirstOrder.SetTheory.term℘_ : Lean.ParserDescr

Equations

• LO.FirstOrder.SetTheory.term℘_ = Lean.ParserDescr.node `LO.FirstOrder.SetTheory.term℘_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "℘ ") (Lean.ParserDescr.cat `term 110))

@[simp]

theorem LO.FirstOrder.SetTheory.mem_power_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x z : V} : z ∈ ℘ x ↔ z ⊆ x

def LO.FirstOrder.SetTheory.power.dfn : Semisentence ℒₛₑₜ 2

Equations

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

instance LO.FirstOrder.SetTheory.power.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₁ power dfn

instance LO.FirstOrder.SetTheory.power.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₁ power

@[simp]

theorem LO.FirstOrder.SetTheory.empty_mem_power {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∅ ∈ ℘ x

@[simp]

theorem LO.FirstOrder.SetTheory.self_mem_power {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∈ ℘ x

@[simp]

theorem LO.FirstOrder.SetTheory.power_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℘ ∅ = {∅}

@[simp]

instance LO.FirstOrder.SetTheory.power_nonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : IsNonempty (℘ x)

Aussonderungsaxiom

theorem LO.FirstOrder.SetTheory.separation_exists_eval {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) (φ : Semiformula ℒₛₑₜ V 1) : ∃ (y : V), ∀ (z : V), z ∈ y ↔ z ∈ x ∧ (Semiformula.Evalm V ![z] id) φ

theorem LO.FirstOrder.SetTheory.separation_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) (P : V → Prop) (hP : ℒₛₑₜ-predicate P) : ∃ (y : V), ∀ (z : V), z ∈ y ↔ z ∈ x ∧ P z

theorem LO.FirstOrder.SetTheory.separation_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) (P : V → Prop) (hP : ℒₛₑₜ-predicate P) : ∃! y : V, ∀ (z : V), z ∈ y ↔ z ∈ x ∧ P z

noncomputable def LO.FirstOrder.SetTheory.sep {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) (P : V → Prop) (hP : ℒₛₑₜ-predicate P) : V

Equations

• LO.FirstOrder.SetTheory.sep x P hP = Classical.choose! ⋯

@[simp]

theorem LO.FirstOrder.SetTheory.mem_sep_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {P : V → Prop} {hP : ℒₛₑₜ-predicate P} {z x : V} : z ∈ sep x P hP ↔ z ∈ x ∧ P z

@[simp]

theorem LO.FirstOrder.SetTheory.sep_empty_eq {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (P : V → Prop) (hP : ℒₛₑₜ-predicate P) : sep ∅ P hP = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.sep_subset {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {P : V → Prop} {hP : ℒₛₑₜ-predicate P} {x : V} : sep x P hP ⊆ x

def LO.FirstOrder.SetTheory.internalSetBuilder : Lean.ParserDescr

Set-builder notation.

Equations

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

def LO.FirstOrder.SetTheory.elabInternalSetBuilder : Lean.Elab.Term.TermElab

Equations

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

def LO.FirstOrder.SetTheory.sep.unexpander : Lean.PrettyPrinter.Unexpander

Equations

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

Intersection

noncomputable def LO.FirstOrder.SetTheory.sInter {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : V

Equations

• ⋂ˢ x = LO.FirstOrder.SetTheory.sep (⋃ˢ x) (fun (z : V) => ∀ y ∈ x, z ∈ y) ⋯

def LO.FirstOrder.SetTheory.«term⋂ˢ_» : Lean.ParserDescr

Equations

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

theorem LO.FirstOrder.SetTheory.mem_sInter_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {z x : V} : z ∈ ⋂ˢ x ↔ IsNonempty x ∧ ∀ y ∈ x, z ∈ y

def LO.FirstOrder.SetTheory.sInter.dfn : Semisentence ℒₛₑₜ 2

Equations

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

instance LO.FirstOrder.SetTheory.sInter.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₁ sInter dfn

instance LO.FirstOrder.SetTheory.sInter.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₁ sInter

@[simp]

theorem LO.FirstOrder.SetTheory.mem_sInter_iff_of_nonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {z x : V} [hx : IsNonempty x] : z ∈ ⋂ˢ x ↔ ∀ y ∈ x, z ∈ y

@[simp]

theorem LO.FirstOrder.SetTheory.sInter_empty_eq {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ⋂ˢ ∅ = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.sInter_singleton {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ⋂ˢ {x} = x

theorem LO.FirstOrder.SetTheory.sInter_subset_of_mem_of_nonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} [IsNonempty y] (h : x ∈ y) : ⋂ˢ y ⊆ x

@[simp]

theorem LO.FirstOrder.SetTheory.subset_sInter_iff_of_nonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} [IsNonempty y] : x ⊆ ⋂ˢ y ↔ ∀ z ∈ y, x ⊆ z

Intersection of two sets

noncomputable def LO.FirstOrder.SetTheory.inter {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : V

Equations

• LO.FirstOrder.SetTheory.inter x y = ⋂ˢ {x, y}

@[implicit_reducible]

noncomputable instance LO.FirstOrder.SetTheory.instInter {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : Inter V

Equations

• LO.FirstOrder.SetTheory.instInter = { inter := LO.FirstOrder.SetTheory.inter }

theorem LO.FirstOrder.SetTheory.inter_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : x ∩ y = ⋂ˢ {x, y}

@[simp]

theorem LO.FirstOrder.SetTheory.mem_inter_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} : z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

def LO.FirstOrder.SetTheory.inter.dfn : Semisentence ℒₛₑₜ 3

Equations

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

instance LO.FirstOrder.SetTheory.inter.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₂ Inter.inter dfn

instance LO.FirstOrder.SetTheory.inter.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₂ Inter.inter

@[simp]

theorem LO.FirstOrder.SetTheory.inter_self {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∩ x = x

theorem LO.FirstOrder.SetTheory.inter_comm {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : x ∩ y = y ∩ x

theorem LO.FirstOrder.SetTheory.inter_assoc {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y z : V) : x ∩ y ∩ z = x ∩ (y ∩ z)

@[simp]

theorem LO.FirstOrder.SetTheory.inter_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∩ ∅ = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.empty_inter {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∅ ∩ x = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.sInter_insert {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) [hy : IsNonempty y] : ⋂ˢ insert x y = x ∩ ⋂ˢ y

@[simp]

theorem LO.FirstOrder.SetTheory.intsert_inter_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y z : V) (hx : x ∈ z) : insert x y ∩ z = insert x (y ∩ z)

@[simp]

theorem LO.FirstOrder.SetTheory.intsert_inter_of_not_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y z : V) (hx : x ∉ z) : insert x y ∩ z = y ∩ z

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_inter_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} (hx : x ∈ y) : {x} ∩ y = {x}

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_inter_of_not_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} (hx : x ∉ y) : {x} ∩ y = ∅

Set difference

noncomputable def LO.FirstOrder.SetTheory.sdiff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : V

Equations

• LO.FirstOrder.SetTheory.sdiff x y = LO.FirstOrder.SetTheory.sep x (fun (z : V) => z ∉ y) ⋯

@[implicit_reducible]

noncomputable instance LO.FirstOrder.SetTheory.instSDiff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : SDiff V

Equations

• LO.FirstOrder.SetTheory.instSDiff = { sdiff := LO.FirstOrder.SetTheory.sdiff }

theorem LO.FirstOrder.SetTheory.sdiff_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : x \ y = sep x (fun (z : V) => z ∉ y) ⋯

@[simp]

theorem LO.FirstOrder.SetTheory.mem_sdiff_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} : z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

def LO.FirstOrder.SetTheory.sdiff.dfn : Semisentence ℒₛₑₜ 3

Equations

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

instance LO.FirstOrder.SetTheory.sdiff.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₂ SDiff.sdiff dfn

instance LO.FirstOrder.SetTheory.sdiff.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₂ SDiff.sdiff

@[simp]

theorem LO.FirstOrder.SetTheory.sdiff_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x \ ∅ = x

@[simp]

theorem LO.FirstOrder.SetTheory.empty_sdiff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∅ \ x = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_sdiff_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x z : V} (hx : x ∈ z) : {x} \ z = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_sdiff_of_not_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x z : V} (hx : x ∉ z) : {x} \ z = {x}

@[simp]

theorem LO.FirstOrder.SetTheory.insert_sdiff_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} (hx : x ∈ z) : insert x y \ z = y \ z

@[simp]

theorem LO.FirstOrder.SetTheory.insert_sdiff_of_not_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} (hx : x ∉ z) : insert x y \ z = insert x (y \ z)

theorem LO.FirstOrder.SetTheory.isNonempty_sdiff_of_ssubset {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x ⊊ y → IsNonempty (y \ x)

Kuratowski's ordered pair

noncomputable def LO.FirstOrder.SetTheory.kpair {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : V

Equations

• ⟨x, y⟩ₖ = {{x}, {x, y}}

def LO.FirstOrder.SetTheory.«term⟨_⟩ₖ» : Lean.ParserDescr

⟨x, y, z, ...⟩ₖ notation for kpair

Equations

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

def LO.FirstOrder.SetTheory.pairUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

noncomputable def LO.FirstOrder.SetTheory.kpair.π₁ {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (z : V) : V

Equations

• LO.FirstOrder.SetTheory.kpair.π₁ z = ⋃ˢ ⋂ˢ z

noncomputable def LO.FirstOrder.SetTheory.kpair.π₂ {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (z : V) : V

Equations

• LO.FirstOrder.SetTheory.kpair.π₂ z = ⋃ˢ LO.FirstOrder.SetTheory.sep (⋃ˢ z) (fun (x : V) => x ∈ ⋂ˢ z → ⋃ˢ z = ⋂ˢ z) ⋯

def LO.FirstOrder.SetTheory.kpair.dfn : Semisentence ℒₛₑₜ 3

Equations

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

instance LO.FirstOrder.SetTheory.kpair.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₂ kpair dfn

instance LO.FirstOrder.SetTheory.kpair.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₂ kpair

def LO.FirstOrder.SetTheory.kpair.π₁.dfn : Semisentence ℒₛₑₜ 2

Equations

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

instance LO.FirstOrder.SetTheory.kpair.π₁.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₁ π₁ dfn

instance LO.FirstOrder.SetTheory.kpair.π₁.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₁ π₁

def LO.FirstOrder.SetTheory.kpair.π₂.dfn : Semisentence ℒₛₑₜ 2

Equations

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

instance LO.FirstOrder.SetTheory.kpair.π₂.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₁ π₂ dfn

instance LO.FirstOrder.SetTheory.kpair.π₂.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₁ π₂

@[simp]

theorem LO.FirstOrder.SetTheory.kpair.π₁_kpair {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : π₁ ⟨x, y⟩ₖ = x

@[simp]

theorem LO.FirstOrder.SetTheory.kpair.π₂_kpair {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : π₂ ⟨x, y⟩ₖ = y

theorem LO.FirstOrder.SetTheory.kpair_inj {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x₁ x₂ y₁ y₂ : V} : ⟨x₁, y₁⟩ₖ = ⟨x₂, y₂⟩ₖ → x₁ = x₂ ∧ y₁ = y₂

@[simp]

theorem LO.FirstOrder.SetTheory.kpair_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x₁ x₂ y₁ y₂ : V} : ⟨x₁, y₁⟩ₖ = ⟨x₂, y₂⟩ₖ ↔ x₁ = x₂ ∧ y₁ = y₂

Product

noncomputable def LO.FirstOrder.SetTheory.prod {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (X Y : V) : V

Equations

• X ×ˢ Y = LO.FirstOrder.SetTheory.sep (℘ ℘ (X ∪ Y)) (fun (z : V) => ∃ x ∈ X, ∃ y ∈ Y, z = ⟨x, y⟩ₖ) ⋯

def LO.FirstOrder.SetTheory.«term_×ˢ_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.SetTheory.mem_prod_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {X Y z : V} : z ∈ X ×ˢ Y ↔ ∃ x ∈ X, ∃ y ∈ Y, z = ⟨x, y⟩ₖ

def LO.FirstOrder.SetTheory.prod.dfn : Semisentence ℒₛₑₜ 3

Equations

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

instance LO.FirstOrder.SetTheory.prod.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₂ prod dfn

instance LO.FirstOrder.SetTheory.prod.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₂ prod

@[simp]

theorem LO.FirstOrder.SetTheory.prod_empty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ×ˢ ∅ = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.empty_prod {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : ∅ ×ˢ x = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.kpair_mem_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y X Y : V} : ⟨x, y⟩ₖ ∈ X ×ˢ Y ↔ x ∈ X ∧ y ∈ Y

theorem LO.FirstOrder.SetTheory.prod_subset_prod_of_subset {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {X₁ X₂ Y₁ Y₂ : V} (hX : X₁ ⊆ X₂) (hY : Y₁ ⊆ Y₂) : X₁ ×ˢ Y₁ ⊆ X₂ ×ˢ Y₂

theorem LO.FirstOrder.SetTheory.union_prod {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y z : V) : x ∪ y ×ˢ z = (x ×ˢ z) ∪ (y ×ˢ z)

@[simp]

theorem LO.FirstOrder.SetTheory.singleton_prod_singleton {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x y : V) : {x} ×ˢ {y} = {⟨x, y⟩ₖ}

theorem LO.FirstOrder.SetTheory.insert_kpair_subset_insert_prod_insert_of_subset_prod {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {R X Y : V} (h : R ⊆ X ×ˢ Y) (x y : V) : insert ⟨x, y⟩ₖ R ⊆ insert x X ×ˢ insert y Y

Axiom of infinity

noncomputable def LO.FirstOrder.SetTheory.succ {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : V

Equations

• LO.FirstOrder.SetTheory.succ x = insert x x

theorem LO.FirstOrder.SetTheory.mem_succ_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : y ∈ succ x ↔ y = x ∨ y ∈ x

@[reducible, inline]

abbrev LO.FirstOrder.SetTheory.succ.dfn : Semisentence ℒₛₑₜ 2

Equations

• LO.FirstOrder.SetTheory.succ.dfn = LO.FirstOrder.SetTheory.isSucc

instance LO.FirstOrder.SetTheory.succ.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₁ succ dfn

instance LO.FirstOrder.SetTheory.succ.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-function₁ succ

@[simp]

theorem LO.FirstOrder.SetTheory.mem_succ_self {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∈ succ x

@[simp]

theorem LO.FirstOrder.SetTheory.mem_subset_refl {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ⊆ succ x

def LO.FirstOrder.SetTheory.IsInductive {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : Prop

Equations

• LO.FirstOrder.SetTheory.IsInductive x = (∅ ∈ x ∧ ∀ y ∈ x, LO.FirstOrder.SetTheory.succ y ∈ x)

def LO.FirstOrder.SetTheory.IsInductive.dfn : Semisentence ℒₛₑₜ 1

Equations

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

instance LO.FirstOrder.SetTheory.IsInductive.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedPred IsInductive dfn

instance LO.FirstOrder.SetTheory.IsInductive.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℒₛₑₜ-predicate IsInductive

theorem LO.FirstOrder.SetTheory.IsInductive.zero {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {I : V} (hI : IsInductive I) : ∅ ∈ I

theorem LO.FirstOrder.SetTheory.IsInductive.succ {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {I : V} (hI : IsInductive I) {x : V} (hx : x ∈ I) : SetTheory.succ x ∈ I

theorem LO.FirstOrder.SetTheory.isInductive_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ∃ (I : V), IsInductive I

theorem LO.FirstOrder.SetTheory.omega_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ∃! ω : V, ∀ (x : V), x ∈ ω ↔ ∀ (I : V), IsInductive I → x ∈ I

noncomputable def LO.FirstOrder.SetTheory.ω {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : V

Equations

• LO.FirstOrder.SetTheory.ω = Classical.choose! ⋯

theorem LO.FirstOrder.SetTheory.mem_ω_iff_mem_all_inductive {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x : V} : x ∈ ω ↔ ∀ (I : V), IsInductive I → x ∈ I

def LO.FirstOrder.SetTheory.isω : Semisentence ℒₛₑₜ 1

Equations

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

instance LO.FirstOrder.SetTheory.ω.defined {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : DefinedFunction₀ ω isω

@[simp]

theorem LO.FirstOrder.SetTheory.empty_mem_ω {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ∅ ∈ ω

@[simp]

instance LO.FirstOrder.SetTheory.ω_nonempty {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : IsNonempty ω

@[simp]

theorem LO.FirstOrder.SetTheory.ω_succ_closed {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x : V} : x ∈ ω → succ x ∈ ω

@[simp]

theorem LO.FirstOrder.SetTheory.ω_isInductive {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : IsInductive ω

theorem LO.FirstOrder.SetTheory.IsInductive.ω_subset {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {I : V} (hI : IsInductive I) : ω ⊆ I

noncomputable def LO.FirstOrder.SetTheory.ofNat {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ℕ → V

Equations

• LO.FirstOrder.SetTheory.ofNat 0 = ∅
• LO.FirstOrder.SetTheory.ofNat n.succ = LO.FirstOrder.SetTheory.succ (LO.FirstOrder.SetTheory.ofNat n)

@[implicit_reducible]

noncomputable def LO.FirstOrder.SetTheory.instOfNat {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (n : ℕ) : OfNat V n

Equations

• LO.FirstOrder.SetTheory.instOfNat n = { ofNat := LO.FirstOrder.SetTheory.ofNat n }

@[implicit_reducible]

noncomputable def LO.FirstOrder.SetTheory.instNatCast {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : NatCast V

Equations

• LO.FirstOrder.SetTheory.instNatCast = { natCast := LO.FirstOrder.SetTheory.ofNat }

theorem LO.FirstOrder.SetTheory.zero_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 0 = ∅

theorem LO.FirstOrder.SetTheory.num_succ_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (n : ℕ) : ↑(n + 1) = succ ↑n

@[simp]

theorem LO.FirstOrder.SetTheory.cast_zero_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ↑0 = 0

@[simp]

theorem LO.FirstOrder.SetTheory.cast_one_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : ↑1 = 1

theorem LO.FirstOrder.SetTheory.one_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 1 = {0}

theorem LO.FirstOrder.SetTheory.one_def' {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 1 = {∅}

theorem LO.FirstOrder.SetTheory.two_def {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 2 = {0, 1}

@[simp]

theorem LO.FirstOrder.SetTheory.zero_ne_one {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 0 ≠ 1

@[simp]

theorem LO.FirstOrder.SetTheory.one_ne_zero {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 1 ≠ 0

@[simp]

theorem LO.FirstOrder.SetTheory.mem_two_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∈ 2 ↔ x = 0 ∨ x = 1

@[simp]

theorem LO.FirstOrder.SetTheory.zero_mem_one {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 0 ∈ 1

@[simp]

theorem LO.FirstOrder.SetTheory.ofNat_mem_ω {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (n : ℕ) : ↑n ∈ ω

@[simp]

theorem LO.FirstOrder.SetTheory.zero_mem_ω {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 0 ∈ ω

@[simp]

theorem LO.FirstOrder.SetTheory.one_mem_ω {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 1 ∈ ω

@[simp]

theorem LO.FirstOrder.SetTheory.two_mem_ω {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] : 2 ∈ ω

theorem LO.FirstOrder.SetTheory.naturalNumber_induction {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (P : V → Prop) (hP : ℒₛₑₜ-predicate P) (zero : P 0) (succ : ∀ x ∈ ω, P x → P (succ x)) (x : V) : x ∈ ω → P x

Axiom of foundation

theorem LO.FirstOrder.SetTheory.foundation {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) [IsNonempty x] : ∃ y ∈ x, ∀ z ∈ x, z ∉ y

theorem LO.FirstOrder.SetTheory.foundation' {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) [IsNonempty x] : ∃ y ∈ x, x ∩ y = ∅

@[simp]

theorem LO.FirstOrder.SetTheory.mem_irrefl {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ∉ x

theorem LO.FirstOrder.SetTheory.ne_of_mem {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x ∈ y → x ≠ y

theorem LO.FirstOrder.SetTheory.mem_asymm {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y : V} : x ∈ y → y ∉ x

theorem LO.FirstOrder.SetTheory.mem_asymm₃ {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] {x y z : V} : x ∈ y → y ∈ z → z ∉ x

@[simp]

theorem LO.FirstOrder.SetTheory.ne_succ {V : Type u_1} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭] (x : V) : x ≠ succ x