NF weak partition development: DefinitionLeaves.Basic.

theorem NFChoice.DefinitionLeaves.Wff.valid_biimp_refl {S : Fol.Structure Foundation.LNF} (p : SemanticCore.Wff) : SemanticCore.Wff.Valid S (p.biimp p)

Every ordinary wff definition becomes this shape after expansion.

theorem NFChoice.DefinitionLeaves.Wff.valid_biimp_of_holds_iff {S : Fol.Structure Foundation.LNF} (p q : SemanticCore.Wff) (h : ∀ (v : SemanticCore.Var → S.carrier), SemanticCore.Wff.Holds S v p ↔ SemanticCore.Wff.Holds S v q) : SemanticCore.Wff.Valid S (p.biimp q)

Pointwise semantic equality is enough to discharge a normalized wff leaf.

theorem NFChoice.DefinitionLeaves.Wff.valid_df_tru {S : Fol.Structure Foundation.LNF} (p : SemanticCore.Wff) : SemanticCore.Wff.Valid S ((SemanticCore.Wff.falsum.imp SemanticCore.Wff.falsum).biimp (p.biimp p))

df-tru after choosing T. to expand to F. → F..

theorem NFChoice.DefinitionLeaves.Class.valid_classEq_refl {S : Fol.Structure Foundation.LNF} (A : SemanticCore.Class) : SemanticCore.Wff.Valid S (SemanticCore.Wff.classEq A A)

Every ordinary class definition without a generated dummy becomes this shape.

theorem NFChoice.DefinitionLeaves.Class.valid_classEq_of_holds_iff {S : Fol.Structure Foundation.LNF} (A B : SemanticCore.Class) (h : ∀ (v : SemanticCore.Var → S.carrier) (z : S.carrier), SemanticCore.Class.Holds S v A z ↔ SemanticCore.Class.Holds S v B z) : SemanticCore.Wff.Valid S (SemanticCore.Wff.classEq A B)

Pointwise class-denotation equality discharges a normalized class leaf.

theorem NFChoice.DefinitionLeaves.Class.holds_update_fresh {S : Fol.Structure Foundation.LNF} (A : SemanticCore.Class) (v : SemanticCore.Var → S.carrier) {x : SemanticCore.Var} (hx : x ∉ A.fv) (a z : S.carrier) : SemanticCore.Class.Holds S (SemanticCore.update v x a) A z ↔ SemanticCore.Class.Holds S v A z

Updating a name fresh for a class cannot change its denotation.

theorem NFChoice.DefinitionLeaves.SemanticBoundary.classMem_cv_iff_holds {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (x : SemanticCore.Var) (B : SemanticCore.Class) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) ↔ SemanticCore.Class.Holds S v B (v x)

A set-variable class represents exactly the corresponding set.

theorem NFChoice.DefinitionLeaves.SemanticBoundary.valid_df_clab {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (x y : SemanticCore.Var) (p : SemanticCore.Wff) : SemanticCore.Wff.Valid S ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cab y p)).biimp (SemanticCore.sbDefiniens x y p))

The exact normalized semantic leaf for source df-clab.

theorem NFChoice.DefinitionLeaves.SemanticBoundary.valid_df_cleq {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hxA : x ∉ A.fv) (hxB : x ∉ B.fv) : SemanticCore.Wff.Valid S ((SemanticCore.Wff.classEq A B).biimp (SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).biimp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B))))

The exact normalized semantic leaf for source df-cleq.

theorem NFChoice.DefinitionLeaves.SemanticBoundary.valid_df_clel {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hxA : x ∉ A.fv) (hxB : x ∉ B.fv) : SemanticCore.Wff.Valid S ((SemanticCore.Wff.classMem A B).biimp (SemanticCore.Wff.ex x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).conj (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B))))

The exact normalized semantic leaf for source df-clel.