Equations
Instances For
theorem
ConNF.ext
{α : ConNF.Λ}
{β : ConNF.Λ}
(hβ : β < α)
(t₁ : ConNF.TSet ↑α)
(t₂ : ConNF.TSet ↑α)
:
theorem
ConNF.inter
{α : ConNF.Λ}
{β : ConNF.Λ}
(hβ : β < α)
{t₁ : ConNF.TSet ↑α}
{t₂ : ConNF.TSet ↑α}
:
∃ (t : ConNF.TSet ↑α), ∀ (s : ConNF.TSet ↑β), s ∈[hβ] t ↔ s ∈[hβ] t₁ ∧ s ∈[hβ] t₂
theorem
ConNF.compl
{α : ConNF.Λ}
{β : ConNF.Λ}
(hβ : β < α)
{t : ConNF.TSet ↑α}
:
∃ (t' : ConNF.TSet ↑α), ∀ (s : ConNF.TSet ↑β), s ∈[hβ] t' ↔ ¬s ∈[hβ] t
theorem
ConNF.mem_singleton_iff
{α : ConNF.Λ}
{β : ConNF.Λ}
(hβ : β < α)
(t : ConNF.TSet ↑β)
(s : ConNF.TSet ↑β)
:
s ∈[hβ] ConNF.ModelData.TSet.singleton hβ t ↔ s = t
theorem
ConNF.mem_up_iff
{α : ConNF.Λ}
{β : ConNF.Λ}
(hβ : β < α)
(t₁ : ConNF.TSet ↑β)
(t₂ : ConNF.TSet ↑β)
(s : ConNF.TSet ↑β)
:
theorem
ConNF.mem_op_iff
{α : 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₂
theorem
ConNF.singletonImage
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
{ε : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(hδ : δ < γ)
(hε : ε < δ)
(t : ConNF.TSet ↑β)
:
∃ (t' : ConNF.TSet ↑α),
∀ (a b : ConNF.TSet ↑ε),
ConNF.ModelData.TSet.op hγ hδ (ConNF.ModelData.TSet.singleton hε a) (ConNF.ModelData.TSet.singleton hε b) ∈[hβ] t' ↔ ConNF.ModelData.TSet.op hδ hε a b ∈[hγ] t
theorem
ConNF.insertion2
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
{ε : ConNF.Λ}
{ζ : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(hδ : δ < γ)
(hε : ε < δ)
(hζ : ζ < ε)
(t : ConNF.TSet ↑γ)
:
∃ (t' : ConNF.TSet ↑α),
∀ (a b c : ConNF.TSet ↑ζ),
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) ∈[hβ] t' ↔ ConNF.ModelData.TSet.op hε hζ a c ∈[hδ] t
theorem
ConNF.insertion3
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
{ε : ConNF.Λ}
{ζ : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(hδ : δ < γ)
(hε : ε < δ)
(hζ : ζ < ε)
(t : ConNF.TSet ↑γ)
:
∃ (t' : ConNF.TSet ↑α),
∀ (a b c : ConNF.TSet ↑ζ),
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) ∈[hβ] t' ↔ ConNF.ModelData.TSet.op hε hζ a b ∈[hδ] t
theorem
ConNF.cross
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(hδ : δ < γ)
(t : ConNF.TSet ↑γ)
:
∃ (t' : ConNF.TSet ↑α),
∀ (a : ConNF.TSet ↑β),
a ∈[hβ] t' ↔ ∃ (b : ConNF.TSet ↑δ) (c : ConNF.TSet ↑δ), a = ConNF.ModelData.TSet.op hγ hδ b c ∧ c ∈[hδ] t
theorem
ConNF.typeLower
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
{ε : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(hδ : δ < γ)
(hε : ε < δ)
(t : ConNF.TSet ↑α)
:
∃ (t' : ConNF.TSet ↑δ),
∀ (a : ConNF.TSet ↑ε),
a ∈[hε] t' ↔ ∀ (b : ConNF.TSet ↑δ), ConNF.ModelData.TSet.op hγ hδ b (ConNF.ModelData.TSet.singleton hε a) ∈[hβ] t
theorem
ConNF.converse
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(hδ : δ < γ)
(t : ConNF.TSet ↑α)
:
∃ (t' : ConNF.TSet ↑α),
∀ (a b : ConNF.TSet ↑δ), ConNF.ModelData.TSet.op hγ hδ a b ∈[hβ] t' ↔ ConNF.ModelData.TSet.op hγ hδ b a ∈[hβ] t
theorem
ConNF.cardinalOne
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
:
∃ (t : ConNF.TSet ↑α),
∀ (a : ConNF.TSet ↑β), a ∈[hβ] t ↔ ∃ (b : ConNF.TSet ↑γ), ∀ (c : ConNF.TSet ↑γ), c ∈[hγ] a ↔ c = b
theorem
ConNF.subset
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
{ε : ConNF.Λ}
(hβ : β < α)
(hγ : γ < β)
(hδ : δ < γ)
(hε : ε < δ)
:
∃ (t : ConNF.TSet ↑α),
∀ (a b : ConNF.TSet ↑δ), ConNF.ModelData.TSet.op hγ hδ a b ∈[hβ] t ↔ ∀ (c : ConNF.TSet ↑ε), c ∈[hε] a → c ∈[hε] b