![]() |
Metamath
Proof Explorer Theorem List (p. 345 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | satff 34401 | The satisfaction predicate as function over wff codes in the model π and the binary relation πΈ on π. (Contributed by AV, 28-Oct-2023.) |
β’ ((π β π β§ πΈ β π β§ π β Ο) β ((π Sat πΈ)βπ):(Fmlaβπ)βΆπ« (π βm Ο)) | ||
Theorem | satfun 34402 | The satisfaction predicate as function over wff codes in the model π and the binary relation πΈ on π. (Contributed by AV, 29-Oct-2023.) |
β’ ((π β π β§ πΈ β π) β ((π Sat πΈ)βΟ):(FmlaβΟ)βΆπ« (π βm Ο)) | ||
Theorem | satfvel 34403 | An element of the value of the satisfaction predicate as function over wff codes in the model π and the binary relation πΈ on π at the code π for a wff using β , βΌ , β is a valuation π:ΟβΆπ of the variables (v0 = (πββ ), v1 = (πβ1o), etc.) so that π is true under the assignment π. (Contributed by AV, 29-Oct-2023.) |
β’ (((π β π β§ πΈ β π) β§ π β (FmlaβΟ) β§ π β (((π Sat πΈ)βΟ)βπ)) β π:ΟβΆπ) | ||
Theorem | satfv0fvfmla0 34404* | The value of the satisfaction predicate as function over a wff code at β . (Contributed by AV, 2-Nov-2023.) |
β’ π = (π Sat πΈ) β β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ )) β ((πββ )βπ) = {π β (π βm Ο) β£ (πβ(1st β(2nd βπ)))πΈ(πβ(2nd β(2nd βπ)))}) | ||
Theorem | satefv 34405 | The simplified satisfaction predicate as function over wff codes in the model π at the code π. (Contributed by AV, 30-Oct-2023.) |
β’ ((π β π β§ π β π) β (π Satβ π) = (((π Sat ( E β© (π Γ π)))βΟ)βπ)) | ||
Theorem | sate0 34406 | The simplified satisfaction predicate for any wff code over an empty model. (Contributed by AV, 6-Oct-2023.) (Revised by AV, 5-Nov-2023.) |
β’ (π β π β (β Satβ π) = (((β Sat β )βΟ)βπ)) | ||
Theorem | satef 34407 | The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023.) |
β’ ((π β π β§ π β (FmlaβΟ) β§ π β (π Satβ π)) β π:ΟβΆπ) | ||
Theorem | sate0fv0 34408 | A simplified satisfaction predicate as function over wff codes over an empty model is an empty set. (Contributed by AV, 31-Oct-2023.) |
β’ (π β (FmlaβΟ) β (π β (β Satβ π) β π = β )) | ||
Theorem | satefvfmla0 34409* | The simplified satisfaction predicate for wff codes of height 0. (Contributed by AV, 4-Nov-2023.) |
β’ ((π β π β§ π β (Fmlaββ )) β (π Satβ π) = {π β (π βm Ο) β£ (πβ(1st β(2nd βπ))) β (πβ(2nd β(2nd βπ)))}) | ||
Theorem | sategoelfvb 34410 | Characterization of a valuation π of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
β’ πΈ = (π Satβ (π΄βππ΅)) β β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β (π β πΈ β (π β (π βm Ο) β§ (πβπ΄) β (πβπ΅)))) | ||
Theorem | sategoelfv 34411 | Condition of a valuation π of a simplified satisfaction predicate for a Godel-set of membership: The sets in model π corresponding to the variables π΄ and π΅ under the assignment of π are in a membership relation in π. (Contributed by AV, 5-Nov-2023.) |
β’ πΈ = (π Satβ (π΄βππ΅)) β β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο) β§ π β πΈ) β (πβπ΄) β (πβπ΅)) | ||
Theorem | ex-sategoelel 34412* | Example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
β’ πΈ = (π Satβ (π΄βππ΅)) & β’ π = (π₯ β Ο β¦ if(π₯ = π΄, π, if(π₯ = π΅, π« π, β ))) β β’ (((π β WUni β§ π β π) β§ (π΄ β Ο β§ π΅ β Ο β§ π΄ β π΅)) β π β πΈ) | ||
Theorem | ex-sategoel 34413* | Instance of sategoelfv 34411 for the example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
β’ πΈ = (π Satβ (π΄βππ΅)) & β’ π = (π₯ β Ο β¦ if(π₯ = π΄, π, if(π₯ = π΅, π« π, β ))) β β’ (((π β WUni β§ π β π) β§ (π΄ β Ο β§ π΅ β Ο β§ π΄ β π΅)) β (πβπ΄) β (πβπ΅)) | ||
Theorem | satfv1fvfmla1 34414* | The value of the satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.) |
β’ π = ((πΌβππ½)βΌπ(πΎβππΏ)) β β’ (((π β π β§ πΈ β π) β§ (πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β (((π Sat πΈ)β1o)βπ) = {π β (π βm Ο) β£ (Β¬ (πβπΌ)πΈ(πβπ½) β¨ Β¬ (πβπΎ)πΈ(πβπΏ))}) | ||
Theorem | 2goelgoanfmla1 34415 | Two Godel-sets of membership combined with a Godel-set for NAND is a Godel formula of height 1. (Contributed by AV, 17-Nov-2023.) |
β’ π = ((πΌβππ½)βΌπ(πΎβππΏ)) β β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β π β (Fmlaβ1o)) | ||
Theorem | satefvfmla1 34416* | The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.) |
β’ π = ((πΌβππ½)βΌπ(πΎβππΏ)) β β’ ((π β π β§ (πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β (π Satβ π) = {π β (π βm Ο) β£ (Β¬ (πβπΌ) β (πβπ½) β¨ Β¬ (πβπΎ) β (πβπΏ))}) | ||
Theorem | ex-sategoelelomsuc 34417* | Example of a valuation of a simplified satisfaction predicate over the ordinal numbers as model for a Godel-set of membership using the properties of a successor: (πβ2o) = π β suc π = (πβ2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2oβπ1o) should not be confused with 2o β 1o, which is false. (Contributed by AV, 19-Nov-2023.) |
β’ π = (π₯ β Ο β¦ if(π₯ = 2o, π, suc π)) β β’ (π β Ο β π β (Ο Satβ (2oβπ1o))) | ||
Theorem | ex-sategoelel12 34418 | Example of a valuation of a simplified satisfaction predicate over a proper pair (of ordinal numbers) as model for a Godel-set of membership using the properties of a successor: (πβ2o) = 1o β 2o = (πβ2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2oβπ1o) should not be confused with 2o β 1o, which is false. (Contributed by AV, 19-Nov-2023.) |
β’ π = (π₯ β Ο β¦ if(π₯ = 2o, 1o, 2o)) β β’ π β ({1o, 2o} Satβ (2oβπ1o)) | ||
Theorem | prv 34419 | The "proves" relation on a set. A wff encoded as π is true in a model π iff for every valuation π β (π βm Ο), the interpretation of the wff using the membership relation on π is true. (Contributed by AV, 5-Nov-2023.) |
β’ ((π β π β§ π β π) β (πβ§π β (π Satβ π) = (π βm Ο))) | ||
Theorem | elnanelprv 34420 | The wff (π΄ β π΅ βΌ π΅ β π΄) encoded as ((π΄βππ΅) βΌπ(π΅βππ΄)) is true in any model π. This is the model theoretic proof of elnanel 9602. (Contributed by AV, 5-Nov-2023.) |
β’ ((π β π β§ π΄ β Ο β§ π΅ β Ο) β πβ§((π΄βππ΅)βΌπ(π΅βππ΄))) | ||
Theorem | prv0 34421 | Every wff encoded as π is true in an "empty model" (π = β ). Since β§ is defined in terms of the interpretations making the given formula true, it is not defined on the "empty model", since there are no interpretations. In particular, the empty set on the LHS of β§ should not be interpreted as the empty model, because βπ₯π₯ = π₯ is not satisfied on the empty model. (Contributed by AV, 19-Nov-2023.) |
β’ (π β (FmlaβΟ) β β β§π) | ||
Theorem | prv1n 34422 | No wff encoded as a Godel-set of membership is true in a model with only one element. (Contributed by AV, 19-Nov-2023.) |
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β Β¬ {π}β§(πΌβππ½)) | ||
Syntax | cgon 34423 | The Godel-set of negation. (Note that this is not a wff.) |
class Β¬ππ | ||
Syntax | cgoa 34424 | The Godel-set of conjunction. |
class β§π | ||
Syntax | cgoi 34425 | The Godel-set of implication. |
class βπ | ||
Syntax | cgoo 34426 | The Godel-set of disjunction. |
class β¨π | ||
Syntax | cgob 34427 | The Godel-set of equivalence. |
class βπ | ||
Syntax | cgoq 34428 | The Godel-set of equality. |
class =π | ||
Syntax | cgox 34429 | The Godel-set of existential quantification. (Note that this is not a wff.) |
class βπππ | ||
Definition | df-gonot 34430 | Define the Godel-set of negation. Here the argument π is also a Godel-set corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ Β¬ππ = (πβΌππ) | ||
Definition | df-goan 34431* | Define the Godel-set of conjunction. Here the arguments π and π are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ β§π = (π’ β V, π£ β V β¦ Β¬π(π’βΌππ£)) | ||
Definition | df-goim 34432* | Define the Godel-set of implication. Here the arguments π and π are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ βπ = (π’ β V, π£ β V β¦ (π’βΌπΒ¬ππ£)) | ||
Definition | df-goor 34433* | Define the Godel-set of disjunction. Here the arguments π and π are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ β¨π = (π’ β V, π£ β V β¦ (Β¬ππ’ βπ π£)) | ||
Definition | df-gobi 34434* | Define the Godel-set of equivalence. Here the arguments π and π are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ βπ = (π’ β V, π£ β V β¦ ((π’ βπ π£)β§π(π£ βπ π’))) | ||
Definition | df-goeq 34435* | Define the Godel-set of equality. Here the arguments π₯ = β¨π, πβ© correspond to vN and vP , so (β =π1o) actually means v0 = v1 , not 0 = 1. Here we use the trick mentioned in ax-ext 2704 to introduce equality as a defined notion in terms of βπ. The expression suc (π’ βͺ π£) = max (π’, π£) + 1 here is a convenient way of getting a dummy variable distinct from π’ and π£. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ =π = (π’ β Ο, π£ β Ο β¦ β¦suc (π’ βͺ π£) / π€β¦βππ€((π€βππ’) βπ (π€βππ£))) | ||
Definition | df-goex 34436 | Define the Godel-set of existential quantification. Here π β Ο corresponds to vN , and π represents another formula, and this expression is [βπ₯π] = βπππ where π₯ is the π-th variable, π = [π] is the code for π. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ βπππ = Β¬πβππΒ¬ππ | ||
Syntax | cgze 34437 | The Axiom of Extensionality. |
class AxExt | ||
Syntax | cgzr 34438 | The Axiom Scheme of Replacement. |
class AxRep | ||
Syntax | cgzp 34439 | The Axiom of Power Sets. |
class AxPow | ||
Syntax | cgzu 34440 | The Axiom of Unions. |
class AxUn | ||
Syntax | cgzg 34441 | The Axiom of Regularity. |
class AxReg | ||
Syntax | cgzi 34442 | The Axiom of Infinity. |
class AxInf | ||
Syntax | cgzf 34443 | The set of models of ZF. |
class ZF | ||
Definition | df-gzext 34444 | The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ AxExt = (βπ2o((2oβπβ ) βπ (2oβπ1o)) βπ (β =π1o)) | ||
Definition | df-gzrep 34445 | The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ AxRep = (π’ β (FmlaβΟ) β¦ (βπ3oβπ1oβπ2o(βπ1oπ’ βπ (2o=π1o)) βπ βπ1oβπ2o((2oβπ1o) βπ βπ3o((3oβπβ )β§πβπ1oπ’)))) | ||
Definition | df-gzpow 34446 | The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ AxPow = βπ1oβπ2o(βπ1o((1oβπ2o) βπ (1oβπβ )) βπ (2oβπ1o)) | ||
Definition | df-gzun 34447 | The Godel-set version of the Axiom of Unions. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ AxUn = βπ1oβπ2o(βπ1o((2oβπ1o)β§π(1oβπβ )) βπ (2oβπ1o)) | ||
Definition | df-gzreg 34448 | The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ AxReg = (βπ1o(1oβπβ ) βπ βπ1o((1oβπβ )β§πβπ2o((2oβπ1o) βπ Β¬π(2oβπβ )))) | ||
Definition | df-gzinf 34449 | The Godel-set version of the Axiom of Infinity. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ AxInf = βπ1o((β βπ1o)β§πβπ2o((2oβπ1o) βπ βπβ ((2oβπβ )β§π(β βπ1o)))) | ||
Definition | df-gzf 34450* | Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ ZF = {π β£ ((Tr π β§ πβ§AxExt β§ πβ§AxPow) β§ (πβ§AxUn β§ πβ§AxReg β§ πβ§AxInf) β§ βπ’ β (FmlaβΟ)πβ§(AxRepβπ’))} | ||
This is a formalization of Appendix C of the Metamath book, which describes the mathematical representation of a formal system, of which set.mm (this file) is one. | ||
Syntax | cmcn 34451 | The set of constants. |
class mCN | ||
Syntax | cmvar 34452 | The set of variables. |
class mVR | ||
Syntax | cmty 34453 | The type function. |
class mType | ||
Syntax | cmvt 34454 | The set of variable typecodes. |
class mVT | ||
Syntax | cmtc 34455 | The set of typecodes. |
class mTC | ||
Syntax | cmax 34456 | The set of axioms. |
class mAx | ||
Syntax | cmrex 34457 | The set of raw expressions. |
class mREx | ||
Syntax | cmex 34458 | The set of expressions. |
class mEx | ||
Syntax | cmdv 34459 | The set of distinct variables. |
class mDV | ||
Syntax | cmvrs 34460 | The variables in an expression. |
class mVars | ||
Syntax | cmrsub 34461 | The set of raw substitutions. |
class mRSubst | ||
Syntax | cmsub 34462 | The set of substitutions. |
class mSubst | ||
Syntax | cmvh 34463 | The set of variable hypotheses. |
class mVH | ||
Syntax | cmpst 34464 | The set of pre-statements. |
class mPreSt | ||
Syntax | cmsr 34465 | The reduct of a pre-statement. |
class mStRed | ||
Syntax | cmsta 34466 | The set of statements. |
class mStat | ||
Syntax | cmfs 34467 | The set of formal systems. |
class mFS | ||
Syntax | cmcls 34468 | The closure of a set of statements. |
class mCls | ||
Syntax | cmpps 34469 | The set of provable pre-statements. |
class mPPSt | ||
Syntax | cmthm 34470 | The set of theorems. |
class mThm | ||
Definition | df-mcn 34471 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mCN = Slot 1 | ||
Definition | df-mvar 34472 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVR = Slot 2 | ||
Definition | df-mty 34473 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mType = Slot 3 | ||
Definition | df-mtc 34474 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mTC = Slot 4 | ||
Definition | df-mmax 34475 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mAx = Slot 5 | ||
Definition | df-mvt 34476 | Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVT = (π‘ β V β¦ ran (mTypeβπ‘)) | ||
Definition | df-mrex 34477 | Define the set of "raw expressions", which are expressions without a typecode attached. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mREx = (π‘ β V β¦ Word ((mCNβπ‘) βͺ (mVRβπ‘))) | ||
Definition | df-mex 34478 | Define the set of expressions, which are strings of constants and variables headed by a typecode constant. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mEx = (π‘ β V β¦ ((mTCβπ‘) Γ (mRExβπ‘))) | ||
Definition | df-mdv 34479 | Define the set of distinct variable conditions, which are pairs of distinct variables. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mDV = (π‘ β V β¦ (((mVRβπ‘) Γ (mVRβπ‘)) β I )) | ||
Definition | df-mvrs 34480* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVars = (π‘ β V β¦ (π β (mExβπ‘) β¦ (ran (2nd βπ) β© (mVRβπ‘)))) | ||
Definition | df-mrsub 34481* | Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mRSubst = (π‘ β V β¦ (π β ((mRExβπ‘) βpm (mVRβπ‘)) β¦ (π β (mRExβπ‘) β¦ ((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) | ||
Definition | df-msub 34482* | Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mSubst = (π‘ β V β¦ (π β ((mRExβπ‘) βpm (mVRβπ‘)) β¦ (π β (mExβπ‘) β¦ β¨(1st βπ), (((mRSubstβπ‘)βπ)β(2nd βπ))β©))) | ||
Definition | df-mvh 34483* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVH = (π‘ β V β¦ (π£ β (mVRβπ‘) β¦ β¨((mTypeβπ‘)βπ£), β¨βπ£ββ©β©)) | ||
Definition | df-mpst 34484* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mPreSt = (π‘ β V β¦ (({π β π« (mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ (mExβπ‘))) | ||
Definition | df-msr 34485* | Define the reduct of a pre-statement. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mStRed = (π‘ β V β¦ (π β (mPreStβπ‘) β¦ β¦(2nd β(1st βπ )) / ββ¦β¦(2nd βπ ) / πβ¦β¨((1st β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) | ||
Definition | df-msta 34486 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mStat = (π‘ β V β¦ ran (mStRedβπ‘)) | ||
Definition | df-mfs 34487* | Define the set of all formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFS = {π‘ β£ ((((mCNβπ‘) β© (mVRβπ‘)) = β β§ (mTypeβπ‘):(mVRβπ‘)βΆ(mTCβπ‘)) β§ ((mAxβπ‘) β (mStatβπ‘) β§ βπ£ β (mVTβπ‘) Β¬ (β‘(mTypeβπ‘) β {π£}) β Fin))} | ||
Definition | df-mcls 34488* | Define the closure of a set of statements relative to a set of disjointness constraints. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mCls = (π‘ β V β¦ (π β π« (mDVβπ‘), β β π« (mExβπ‘) β¦ β© {π β£ ((β βͺ ran (mVHβπ‘)) β π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))})) | ||
Definition | df-mpps 34489* | Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mPPSt = (π‘ β V β¦ {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))}) | ||
Definition | df-mthm 34490 | Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mThm = (π‘ β V β¦ (β‘(mStRedβπ‘) β ((mStRedβπ‘) β (mPPStβπ‘)))) | ||
Theorem | mvtval 34491 | The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVTβπ) & β’ π = (mTypeβπ) β β’ π = ran π | ||
Theorem | mrexval 34492 | The set of "raw expressions", which are expressions without a typecode, that is, just sequences of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) & β’ π = (mRExβπ) β β’ (π β π β π = Word (πΆ βͺ π)) | ||
Theorem | mexval 34493 | The set of expressions, which are pairs whose first element is a typecode, and whose second element is a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΎ = (mTCβπ) & β’ πΈ = (mExβπ) & β’ π = (mRExβπ) β β’ πΈ = (πΎ Γ π ) | ||
Theorem | mexval2 34494 | The set of expressions, which are pairs whose first element is a typecode, and whose second element is a list of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΎ = (mTCβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) β β’ πΈ = (πΎ Γ Word (πΆ βͺ π)) | ||
Theorem | mdvval 34495 | The set of disjoint variable conditions, which are pairs of distinct variables. (This definition differs from appendix C, which uses unordered pairs instead. We use ordered pairs, but all sets of disjoint variable conditions of interest will be symmetric, so it does not matter.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π· = (mDVβπ) β β’ π· = ((π Γ π) β I ) | ||
Theorem | mvrsval 34496 | The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π = (mVarsβπ) β β’ (π β πΈ β (πβπ) = (ran (2nd βπ) β© π)) | ||
Theorem | mvrsfpw 34497 | The set of variables in an expression is a finite subset of π. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π = (mVarsβπ) β β’ (π β πΈ β (πβπ) β (π« π β© Fin)) | ||
Theorem | mrsubffval 34498* | The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) & β’ πΊ = (freeMndβ(πΆ βͺ π)) β β’ (π β π β π = (π β (π βpm π) β¦ (π β π β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) | ||
Theorem | mrsubfval 34499* | The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) & β’ πΊ = (freeMndβ(πΆ βͺ π)) β β’ ((πΉ:π΄βΆπ β§ π΄ β π) β (πβπΉ) = (π β π β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π)))) | ||
Theorem | mrsubval 34500* | The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) & β’ πΊ = (freeMndβ(πΆ βͺ π)) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β π ) β ((πβπΉ)βπ) = (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |