The predicative part of Hailperin's finite axiomatisation of NF

theorem ConNF.Symmetric.inter [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) {s₁ : Set (ConNF.TSet ↑β)} {s₂ : Set (ConNF.TSet ↑β)} (h₁ : ConNF.Symmetric hβ s₁) (h₂ : ConNF.Symmetric hβ s₂) : ConNF.Symmetric hβ (s₁ ∩ s₂)

theorem ConNF.ModelData.TSet.inter_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑α) (t₂ : ConNF.TSet ↑α) : ConNF.Symmetric hβ {s : ConNF.TSet ↑β | s ∈[hβ] t₁ ∧ s ∈[hβ] t₂}

def ConNF.ModelData.TSet.inter [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑α) (t₂ : ConNF.TSet ↑α) : ConNF.TSet ↑α

Equations

• ConNF.ModelData.TSet.inter hβ t₁ t₂ = ConNF.ModelData.TSet.mk hβ {s : ConNF.TSet ↑β | s ∈[hβ] t₁ ∧ s ∈[hβ] t₂} ⋯

theorem ConNF.Symmetric.compl [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) {s : Set (ConNF.TSet ↑β)} (h : ConNF.Symmetric hβ s) : ConNF.Symmetric hβ sᶜ

theorem ConNF.ModelData.TSet.compl_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑α) : ConNF.Symmetric hβ {s : ConNF.TSet ↑β | ¬s ∈[hβ] t}

def ConNF.ModelData.TSet.compl [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑α) : ConNF.TSet ↑α

Equations

• ConNF.ModelData.TSet.compl hβ t = ConNF.ModelData.TSet.mk hβ {s : ConNF.TSet ↑β | ¬s ∈[hβ] t} ⋯

theorem ConNF.ModelData.TSet.singleton_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑β) : ConNF.Symmetric hβ {t}

def ConNF.ModelData.TSet.singleton [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑β) : ConNF.TSet ↑α

Equations

• ConNF.ModelData.TSet.singleton hβ t = ConNF.ModelData.TSet.mk hβ {t} ⋯

theorem ConNF.ModelData.TSet.up_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) : ConNF.Symmetric hβ {t₁, t₂}

def ConNF.ModelData.TSet.up [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) : ConNF.TSet ↑α

The unordered pair.

Equations

• ConNF.ModelData.TSet.up hβ t₁ t₂ = ConNF.ModelData.TSet.mk hβ {t₁, t₂} ⋯

def ConNF.ModelData.TSet.op [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (t₁ : ConNF.TSet ↑γ) (t₂ : ConNF.TSet ↑γ) : ConNF.TSet ↑α

The Kuratowski ordered pair.

Equations

• ConNF.ModelData.TSet.op hβ hγ t₁ t₂ = ConNF.ModelData.TSet.up hβ (ConNF.ModelData.TSet.singleton hγ t₁) (ConNF.ModelData.TSet.up hγ t₁ t₂)

@[simp]

theorem ConNF.ModelData.TSet.mem_singleton_iff [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑β) (s : ConNF.TSet ↑β) : s ∈[hβ] ConNF.ModelData.TSet.singleton hβ t ↔ s = t

@[simp]

theorem ConNF.smul_singleton [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑β) (ρ : ConNF.Allowable ↑α) : ρ • ConNF.ModelData.TSet.singleton hβ t = ConNF.ModelData.TSet.singleton hβ ((ConNF.cons hβ) ρ • t)

theorem ConNF.singleton_injective' [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) (h : ConNF.ModelData.TSet.singleton hβ t₁ = ConNF.ModelData.TSet.singleton hβ t₂) : t₁ = t₂

@[simp]

theorem ConNF.ModelData.TSet.mem_up_iff [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) (s : ConNF.TSet ↑β) : s ∈[hβ] ConNF.ModelData.TSet.up hβ t₁ t₂ ↔ s = t₁ ∨ s = t₂

@[simp]

theorem ConNF.smul_up [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) (ρ : ConNF.Allowable ↑α) : ρ • ConNF.ModelData.TSet.up hβ t₁ t₂ = ConNF.ModelData.TSet.up hβ ((ConNF.cons hβ) ρ • t₁) ((ConNF.cons hβ) ρ • t₂)

theorem ConNF.up_self [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑β) : ConNF.ModelData.TSet.up hβ t t = ConNF.ModelData.TSet.singleton hβ t

theorem ConNF.up_injective [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) (t₁' : ConNF.TSet ↑β) (t₂' : ConNF.TSet ↑β) (h : ConNF.ModelData.TSet.up hβ t₁ t₂ = ConNF.ModelData.TSet.up hβ t₁' t₂') : t₁ = t₁' ∧ t₂ = t₂' ∨ t₁ = t₂' ∧ t₂ = t₁'

theorem ConNF.up_eq_singleton_iff [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑β) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) : ConNF.ModelData.TSet.up hβ t₁ t₂ = ConNF.ModelData.TSet.singleton hβ t ↔ t₁ = t ∧ t₂ = t

@[simp]

theorem ConNF.ModelData.TSet.mem_op_iff [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (t₁ : ConNF.TSet ↑γ) (t₂ : ConNF.TSet ↑γ) (s : ConNF.TSet ↑β) : s ∈[hβ] ConNF.ModelData.TSet.op hβ hγ t₁ t₂ ↔ s = ConNF.ModelData.TSet.singleton hγ t₁ ∨ s = ConNF.ModelData.TSet.up hγ t₁ t₂

@[simp]

theorem ConNF.smul_op [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (t₁ : ConNF.TSet ↑γ) (t₂ : ConNF.TSet ↑γ) (ρ : ConNF.Allowable ↑α) : ρ • ConNF.ModelData.TSet.op hβ hγ t₁ t₂ = ConNF.ModelData.TSet.op hβ hγ ((ConNF.cons hγ) ((ConNF.cons hβ) ρ) • t₁) ((ConNF.cons hγ) ((ConNF.cons hβ) ρ) • t₂)

theorem ConNF.op_injective [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (t₁ : ConNF.TSet ↑γ) (t₂ : ConNF.TSet ↑γ) (t₁' : ConNF.TSet ↑γ) (t₂' : ConNF.TSet ↑γ) (h : ConNF.ModelData.TSet.op hβ hγ t₁ t₂ = ConNF.ModelData.TSet.op hβ hγ t₁' t₂') : t₁ = t₁' ∧ t₂ = t₂'

theorem ConNF.Symmetric.singletonImage [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) {s : Set (ConNF.TSet ↑γ)} (h : ConNF.Symmetric hγ s) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ε) (b : ConNF.TSet ↑ε), ConNF.ModelData.TSet.op hδ hε a b ∈ s ∧ p = ConNF.ModelData.TSet.op hγ hδ (ConNF.ModelData.TSet.singleton hε a) (ConNF.ModelData.TSet.singleton hε b)}

theorem ConNF.ModelData.TSet.singletonImage_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) (t : ConNF.TSet ↑β) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ε) (b : ConNF.TSet ↑ε), ConNF.ModelData.TSet.op hδ hε a b ∈[hγ] t ∧ p = ConNF.ModelData.TSet.op hγ hδ (ConNF.ModelData.TSet.singleton hε a) (ConNF.ModelData.TSet.singleton hε b)}

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

Equations

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

theorem ConNF.Symmetric.insertion2 [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} {ζ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) (hζ : ζ < ε) {s : Set (ConNF.TSet ↑δ)} (h : ConNF.Symmetric hδ s) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ζ) (b : ConNF.TSet ↑ζ) (c : ConNF.TSet ↑ζ), ConNF.ModelData.TSet.op hε hζ a c ∈ s ∧ p = ConNF.ModelData.TSet.op hγ hδ (ConNF.ModelData.TSet.singleton hε (ConNF.ModelData.TSet.singleton hζ a)) (ConNF.ModelData.TSet.op hε hζ b c)}

theorem ConNF.ModelData.TSet.insertion2_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} {ζ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) (hζ : ζ < ε) (t : ConNF.TSet ↑γ) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ζ) (b : ConNF.TSet ↑ζ) (c : ConNF.TSet ↑ζ), ConNF.ModelData.TSet.op hε hζ a c ∈[hδ] t ∧ p = ConNF.ModelData.TSet.op hγ hδ (ConNF.ModelData.TSet.singleton hε (ConNF.ModelData.TSet.singleton hζ a)) (ConNF.ModelData.TSet.op hε hζ b c)}

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

Equations

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

theorem ConNF.Symmetric.insertion3 [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} {ζ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) (hζ : ζ < ε) {s : Set (ConNF.TSet ↑δ)} (h : ConNF.Symmetric hδ s) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ζ) (b : ConNF.TSet ↑ζ) (c : ConNF.TSet ↑ζ), ConNF.ModelData.TSet.op hε hζ a b ∈ s ∧ p = ConNF.ModelData.TSet.op hγ hδ (ConNF.ModelData.TSet.singleton hε (ConNF.ModelData.TSet.singleton hζ a)) (ConNF.ModelData.TSet.op hε hζ b c)}

theorem ConNF.ModelData.TSet.insertion3_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} {ζ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) (hζ : ζ < ε) (t : ConNF.TSet ↑γ) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ζ) (b : ConNF.TSet ↑ζ) (c : ConNF.TSet ↑ζ), ConNF.ModelData.TSet.op hε hζ a b ∈[hδ] t ∧ p = ConNF.ModelData.TSet.op hγ hδ (ConNF.ModelData.TSet.singleton hε (ConNF.ModelData.TSet.singleton hζ a)) (ConNF.ModelData.TSet.op hε hζ b c)}

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

Equations

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

theorem ConNF.Symmetric.cross [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) {s : Set (ConNF.TSet ↑δ)} (h : ConNF.Symmetric hδ s) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑δ), ∃ b ∈ s, p = ConNF.ModelData.TSet.op hγ hδ a b}

theorem ConNF.ModelData.TSet.cross_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (t : ConNF.TSet ↑γ) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑δ) (b : ConNF.TSet ↑δ), b ∈[hδ] t ∧ p = ConNF.ModelData.TSet.op hγ hδ a b}

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

Equations

• ConNF.ModelData.TSet.cross hβ hγ hδ t = ConNF.ModelData.TSet.mk hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑δ) (b : ConNF.TSet ↑δ), b ∈[hδ] t ∧ p = ConNF.ModelData.TSet.op hγ hδ a b} ⋯

theorem ConNF.Symmetric.typeLower' [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) {s : Set (ConNF.TSet ↑β)} (h : ConNF.Symmetric hβ s) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ε), (∀ (b : ConNF.TSet ↑δ), ConNF.ModelData.TSet.op hγ hδ b (ConNF.ModelData.TSet.singleton hε a) ∈ s) ∧ p = ConNF.ModelData.TSet.singleton hγ (ConNF.ModelData.TSet.singleton hδ (ConNF.ModelData.TSet.singleton hε a))}

theorem ConNF.ModelData.TSet.typeLower'_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) (t : ConNF.TSet ↑α) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑ε), (∀ (b : ConNF.TSet ↑δ), ConNF.ModelData.TSet.op hγ hδ b (ConNF.ModelData.TSet.singleton hε a) ∈[hβ] t) ∧ p = ConNF.ModelData.TSet.singleton hγ (ConNF.ModelData.TSet.singleton hδ (ConNF.ModelData.TSet.singleton hε a))}

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

This isn't quite the right form of the type lowering axiom, but once we have the axiom of union for singletons, we will be able to deduce the correct form of the result.

Equations

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

theorem ConNF.Symmetric.converse [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) {s : Set (ConNF.TSet ↑β)} (h : ConNF.Symmetric hβ s) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑δ) (b : ConNF.TSet ↑δ), ConNF.ModelData.TSet.op hγ hδ a b ∈ s ∧ p = ConNF.ModelData.TSet.op hγ hδ b a}

theorem ConNF.ModelData.TSet.converse_supported [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (t : ConNF.TSet ↑α) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑δ) (b : ConNF.TSet ↑δ), ConNF.ModelData.TSet.op hγ hδ a b ∈[hβ] t ∧ p = ConNF.ModelData.TSet.op hγ hδ b a}

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

Equations

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

theorem ConNF.Symmetric.cardinalOne [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} (hβ : β < α) (hγ : γ < β) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑γ), p = ConNF.ModelData.TSet.singleton hγ a}

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

Equations

• ConNF.ModelData.TSet.cardinalOne hβ hγ = ConNF.ModelData.TSet.mk hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑γ), p = ConNF.ModelData.TSet.singleton hγ a} ⋯

theorem ConNF.Symmetric.subset [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} {γ : ConNF.Λ} {δ : ConNF.Λ} {ε : ConNF.Λ} (hβ : β < α) (hγ : γ < β) (hδ : δ < γ) (hε : ε < δ) : ConNF.Symmetric hβ {p : ConNF.TSet ↑β | ∃ (a : ConNF.TSet ↑δ) (b : ConNF.TSet ↑δ), (∀ (c : ConNF.TSet ↑ε), c ∈[hε] a → c ∈[hε] b) ∧ p = ConNF.ModelData.TSet.op hγ hδ a b}

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

Equations

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