theorem
ConNF.exists_inter
[ConNF.Params]
{α β : ConNF.Λ}
(hβ : ↑β < ↑α)
(x y : ConNF.TSet ↑α)
:
∃ (w : ConNF.TSet ↑α), ∀ (z : ConNF.TSet ↑β), z ∈[hβ] w ↔ z ∈[hβ] x ∧ z ∈[hβ] y
theorem
ConNF.exists_compl
[ConNF.Params]
{α β : ConNF.Λ}
(hβ : ↑β < ↑α)
(x : ConNF.TSet ↑α)
:
∃ (y : ConNF.TSet ↑α), ∀ (z : ConNF.TSet ↑β), z ∈[hβ] y ↔ ¬z ∈[hβ] x
theorem
ConNF.mem_singleton_iff
[ConNF.Params]
{α β : ConNF.Λ}
(hβ : ↑β < ↑α)
(x y : ConNF.TSet ↑β)
:
y ∈[hβ] ConNF.singleton hβ x ↔ y = x
theorem
ConNF.op_def
[ConNF.Params]
{α β γ : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(x y : ConNF.TSet ↑γ)
:
ConNF.TSet.op hβ hγ x y = ConNF.TSet.up hβ (ConNF.singleton hγ x) (ConNF.TSet.up hγ x y)
theorem
ConNF.exists_singletonImage
[ConNF.Params]
{α β γ δ ε : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑γ)
(hε : ↑ε < ↑δ)
(x : ConNF.TSet ↑β)
:
∃ (y : ConNF.TSet ↑α),
∀ (z w : ConNF.TSet ↑ε),
ConNF.TSet.op hγ hδ (ConNF.singleton hε z) (ConNF.singleton hε w) ∈[hβ] y ↔ ConNF.TSet.op hδ hε z w ∈[hγ] x
theorem
ConNF.exists_insertion2
[ConNF.Params]
{α β γ δ ε ζ : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑γ)
(hε : ↑ε < ↑δ)
(hζ : ↑ζ < ↑ε)
(x : ConNF.TSet ↑γ)
:
∃ (y : ConNF.TSet ↑α),
∀ (a b c : ConNF.TSet ↑ζ),
ConNF.TSet.op hγ hδ (ConNF.singleton hε (ConNF.singleton hζ a)) (ConNF.TSet.op hε hζ b c) ∈[hβ] y ↔ ConNF.TSet.op hε hζ a c ∈[hδ] x
theorem
ConNF.exists_insertion3
[ConNF.Params]
{α β γ δ ε ζ : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑γ)
(hε : ↑ε < ↑δ)
(hζ : ↑ζ < ↑ε)
(x : ConNF.TSet ↑γ)
:
∃ (y : ConNF.TSet ↑α),
∀ (a b c : ConNF.TSet ↑ζ),
ConNF.TSet.op hγ hδ (ConNF.singleton hε (ConNF.singleton hζ a)) (ConNF.TSet.op hε hζ b c) ∈[hβ] y ↔ ConNF.TSet.op hε hζ a b ∈[hδ] x
theorem
ConNF.exists_cross
[ConNF.Params]
{α β γ δ : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑γ)
(x : ConNF.TSet ↑γ)
:
∃ (y : ConNF.TSet ↑α),
∀ (a : ConNF.TSet ↑β), a ∈[hβ] y ↔ ∃ (b : ConNF.TSet ↑δ) (c : ConNF.TSet ↑δ), a = ConNF.TSet.op hγ hδ b c ∧ c ∈[hδ] x
theorem
ConNF.exists_typeLower
[ConNF.Params]
{α β γ δ ε : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑γ)
(hε : ↑ε < ↑δ)
(x : ConNF.TSet ↑α)
:
∃ (y : ConNF.TSet ↑δ),
∀ (a : ConNF.TSet ↑ε), a ∈[hε] y ↔ ∀ (b : ConNF.TSet ↑δ), ConNF.TSet.op hγ hδ b (ConNF.singleton hε a) ∈[hβ] x
theorem
ConNF.exists_converse
[ConNF.Params]
{α β γ δ : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑γ)
(x : ConNF.TSet ↑α)
:
∃ (y : ConNF.TSet ↑α), ∀ (a b : ConNF.TSet ↑δ), ConNF.TSet.op hγ hδ a b ∈[hβ] y ↔ ConNF.TSet.op hγ hδ b a ∈[hβ] x
theorem
ConNF.exists_cardinalOne
[ConNF.Params]
{α β γ : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
:
∃ (x : ConNF.TSet ↑α),
∀ (a : ConNF.TSet ↑β), a ∈[hβ] x ↔ ∃ (b : ConNF.TSet ↑γ), ∀ (c : ConNF.TSet ↑γ), c ∈[hγ] a ↔ c = b
theorem
ConNF.exists_subset
[ConNF.Params]
{α β γ δ ε : ConNF.Λ}
(hβ : ↑β < ↑α)
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑γ)
(hε : ↑ε < ↑δ)
:
∃ (x : ConNF.TSet ↑α),
∀ (a b : ConNF.TSet ↑δ), ConNF.TSet.op hγ hδ a b ∈[hβ] x ↔ ∀ (c : ConNF.TSet ↑ε), c ∈[hε] a → c ∈[hε] b