NF weak partition development: NominalDefinitionLeafAdapterDev014.

Exporter-facing adapters for the three non-identity Metamath definitions.

The source replay has already checked every substituted $d pair. These lemmas turn the resulting x ∉ A.fv evidence into the exact de-Bruijn lowering equalities expected by dfCleqOfShift and dfClelOfShift.

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.shiftRhoAt_lift_one (rho : SemanticCore.Var → ℕ) : shiftRhoAt (liftRho rho) 1 = liftRho (liftRho rho)

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.classPred_double_lift (rho : SemanticCore.Var → ℕ) (A : SemanticCore.Class) : lowerClassPred (liftRho (liftRho rho)) 0 A = ClassHandlersDev011.classPred rho A ↑f' 1 # 1

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.classPred_bind_eq_lift_of_not_mem_fv (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (A : SemanticCore.Class) (hx : x ∉ A.fv) : lowerClassPred (liftRho (bindRho rho x)) 0 A = ClassHandlersDev011.classPred rho A ↑f' 1 # 1

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.classPred_bind_cv_self (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : ClassHandlersDev011.classPred (bindRho rho x) (SemanticCore.Class.cv x) = DirectCertificate.ClassBoundaryNormalizationDev005.cvPred &0

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.lowerClassPred_bind_cv_self (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : lowerClassPred (liftRho (bindRho rho x)) 0 (SemanticCore.Class.cv x) = DirectCertificate.ClassBoundaryNormalizationDev005.cvPred &0

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.lowerWff_classEq (rho : SemanticCore.Var → ℕ) (A B : SemanticCore.Class) : lowerWff rho (SemanticCore.Wff.classEq A B) = DirectCertificate.ClassBoundaryCoreDev006.classEq (ClassHandlersDev011.classPred rho A) (ClassHandlersDev011.classPred rho B)

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.lowerWff_classMem (rho : SemanticCore.Var → ℕ) (A B : SemanticCore.Class) : lowerWff rho (SemanticCore.Wff.classMem A B) = DirectCertificate.ClassBoundaryCoreDev006.classMem (ClassHandlersDev011.classPred rho A) (ClassHandlersDev011.classPred rho B)

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.lowerWff_bind_classMem_cv_of_not_mem_fv (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (A : SemanticCore.Class) (hx : x ∉ A.fv) : lowerWff (bindRho rho x) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) = DirectCertificate.ClassBoundaryRawHandlersDev010.liftedClassMem (ClassHandlersDev011.classPred rho A)

theorem NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.lowerWff_bind_classEq_cv_of_not_mem_fv (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (A : SemanticCore.Class) (hx : x ∉ A.fv) : lowerWff (bindRho rho x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) = DirectCertificate.ClassBoundaryNormalizationDev005.represents (&0) (ClassHandlersDev011.classPred rho A ↑f' 1 # 1)

noncomputable def NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.dfCleqOfDV (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (hAxExt : NPrf ((SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).biimp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv z)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (SemanticCore.Class.cv z)))) (hxA : x ∉ A.fv) (hxB : x ∉ B.fv) : NPrf (ClassHandlersDev011.dfCleqGoal x A B)

Direct adapter for the exact df-cleq source signature.

Equations

• NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.dfCleqOfDV x y z A B hAxExt hxA hxB = NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.dfCleqOfShift x y z A B hAxExt ⋯ ⋯ ⋯

noncomputable def NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.dfClelOfDV (x : SemanticCore.Var) (A B : SemanticCore.Class) (hxA : x ∉ A.fv) (hxB : x ∉ B.fv) : NPrf (ClassHandlersDev011.dfClelGoal x A B)

Direct adapter for the exact df-clel source signature.

Equations

• NFChoice.DirectNominalPrf.Nominal.DefinitionLeafAdapterDev014.dfClelOfDV x A B hxA hxB = NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.dfClelOfShift x A B ⋯ ⋯ ⋯