New file

In this file...

We are roughly following Scott Fenton's development of NF: https://us.metamath.org/nfeuni/mmnf.html.

Main declarations

• ConNF.foo: Something new.

def ConNF.disjoint [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) : TSet ↑α

The set {⟨x, y⟩ | x ∩ y = ∅} (or rather, a set that contains only these Kuratowski pairs).

Equations

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

theorem ConNF.mem_disjoint_iff' [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x y : TSet ↑δ) : ⟨x, y⟩[hγ, hδ] ∈[hβ] disjoint hβ hγ hδ hε ↔ ∀ (z : TSet ↑ε), ¬z ∈[hε] x ⊓[hε] y

@[simp]

theorem ConNF.mem_disjoint_iff [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x y : TSet ↑δ) : ⟨x, y⟩[hγ, hδ] ∈[hβ] disjoint hβ hγ hδ hε ↔ x ⊓[hε] y = empty hε

def ConNF.unionEq [Params] {α β γ δ ε ζ η : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (hη : ↑η < ↑ζ) : TSet ↑α

The set {⟨{{z}}, ⟨y, x⟩ | y ∪ z = x} (or rather, again, a set that contains only these pairs).

Equations

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

theorem ConNF.mem_unionEq_iff' [Params] {α β γ δ ε ζ η : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (hη : ↑η < ↑ζ) (x y z : TSet ↑ζ) : ⟨{{z}[hζ]}[hε], ⟨y, x⟩[hε, hζ]⟩[hγ, hδ] ∈[hβ] unionEq hβ hγ hδ hε hζ hη ↔ ∀ (a : TSet ↑η), ¬(a ∈[hη] x ↔ ¬a ∈[hη] y ∧ ¬a ∈[hη] z)

@[simp]

theorem ConNF.mem_unionEq_iff [Params] {α β γ δ ε ζ η : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (hη : ↑η < ↑ζ) (x y z : TSet ↑ζ) : ⟨{{z}[hζ]}[hε], ⟨y, x⟩[hε, hζ]⟩[hγ, hδ] ∈[hβ] unionEq hβ hγ hδ hε hζ hη ↔ y ⊔[hη] z = x

def ConNF.binPartRel [Params] {α β γ δ ε ζ η : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (hη : ↑η < ↑ζ) : TSet ↑α

The binary partition relation: {⟨x, y, z⟩ | x ∩ y = ∅ ∧ x ∪ y = z}.

Equations

• ConNF.binPartRel hβ hγ hδ hε hζ hη = ConNF.insertion3 hβ hγ hδ hε hζ (ConNF.disjoint hδ hε hζ hη) ⊓[hβ] ConNF.unionEq hβ hγ hδ hε hζ hη

@[simp]

theorem ConNF.mem_binPartRel_iff [Params] {α β γ δ ε ζ η : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (hη : ↑η < ↑ζ) (x y z : TSet ↑ζ) : ⟨{{x}[hζ]}[hε], ⟨y, z⟩[hε, hζ]⟩[hγ, hδ] ∈[hβ] binPartRel hβ hγ hδ hε hζ hη ↔ x ⊓[hη] y = empty hη ∧ x ⊔[hη] y = z

def ConNF.cardAdd [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : TSet ↑α) : TSet ↑α

The sum of two cardinals: x + y = {a ∪ b | a ∈ x ∧ b ∈ y ∧ a ∩ b = ∅}.

Equations

• ConNF.cardAdd hβ hγ x y = ConNF.image ⋯ ⋯ hβ (ConNF.image ⋯ ⋯ ⋯ (ConNF.binPartRel ⋯ ⋯ ⋯ ⋯ hβ hγ) (ConNF.singletons ⋯ ⋯ (ConNF.singletons ⋯ hβ y))) x

@[simp]

theorem ConNF.mem_cardAdd_iff [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : TSet ↑α) (z : TSet ↑β) : z ∈[hβ] cardAdd hβ hγ x y ↔ ∃ (a : TSet ↑β) (b : TSet ↑β), a ∈[hβ] x ∧ b ∈[hβ] y ∧ a ⊓[hγ] b = empty hγ ∧ a ⊔[hγ] b = z

def ConNF.succ [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x : TSet ↑α) : TSet ↑α

The successor of a cardinal: x + 1 = {a ∪ {b} | a ∈ x, b ∉ a}.

Equations

• ConNF.succ hβ hγ x = ConNF.cardAdd hβ hγ x (ConNF.cardinalOne hβ hγ)

@[simp]

theorem ConNF.mem_succ_iff [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x : TSet ↑α) (y : TSet ↑β) : y ∈[hβ] succ hβ hγ x ↔ ∃ (a : TSet ↑β), a ∈[hβ] x ∧ ∃ (b : TSet ↑γ), ¬b ∈[hγ] a ∧ y = a ⊔[hγ] {b}[hγ]

def ConNF.cardinalNat [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) : ℕ → TSet ↑α

Equations

• ConNF.cardinalNat hβ hγ 0 = {ConNF.empty hγ}[hβ]
• ConNF.cardinalNat hβ hγ n.succ = ConNF.succ hβ hγ (ConNF.cardinalNat hβ hγ n)

@[simp]

theorem ConNF.mem_cardinalNat_iff [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (n : ℕ) (a : TSet ↑β) : a ∈[hβ] cardinalNat hβ hγ n ↔ ∃ (s : Finset (TSet ↑γ)), s.card = n ∧ ∀ (b : TSet ↑γ), b ∈[hγ] a ↔ b ∈ s