Home | Metamath
Proof Explorer Theorem List (p. 339 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cgze 33801 | The Axiom of Extensionality. |
class AxExt | ||
Syntax | cgzr 33802 | The Axiom Scheme of Replacement. |
class AxRep | ||
Syntax | cgzp 33803 | The Axiom of Power Sets. |
class AxPow | ||
Syntax | cgzu 33804 | The Axiom of Unions. |
class AxUn | ||
Syntax | cgzg 33805 | The Axiom of Regularity. |
class AxReg | ||
Syntax | cgzi 33806 | The Axiom of Infinity. |
class AxInf | ||
Syntax | cgzf 33807 | The set of models of ZF. |
class ZF | ||
Definition | df-gzext 33808 | 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 33809 | 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 33810 | 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 33811 | 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 33812 | 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 33813 | 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 33814* | 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 33815 | The set of constants. |
class mCN | ||
Syntax | cmvar 33816 | The set of variables. |
class mVR | ||
Syntax | cmty 33817 | The type function. |
class mType | ||
Syntax | cmvt 33818 | The set of variable typecodes. |
class mVT | ||
Syntax | cmtc 33819 | The set of typecodes. |
class mTC | ||
Syntax | cmax 33820 | The set of axioms. |
class mAx | ||
Syntax | cmrex 33821 | The set of raw expressions. |
class mREx | ||
Syntax | cmex 33822 | The set of expressions. |
class mEx | ||
Syntax | cmdv 33823 | The set of distinct variables. |
class mDV | ||
Syntax | cmvrs 33824 | The variables in an expression. |
class mVars | ||
Syntax | cmrsub 33825 | The set of raw substitutions. |
class mRSubst | ||
Syntax | cmsub 33826 | The set of substitutions. |
class mSubst | ||
Syntax | cmvh 33827 | The set of variable hypotheses. |
class mVH | ||
Syntax | cmpst 33828 | The set of pre-statements. |
class mPreSt | ||
Syntax | cmsr 33829 | The reduct of a pre-statement. |
class mStRed | ||
Syntax | cmsta 33830 | The set of statements. |
class mStat | ||
Syntax | cmfs 33831 | The set of formal systems. |
class mFS | ||
Syntax | cmcls 33832 | The closure of a set of statements. |
class mCls | ||
Syntax | cmpps 33833 | The set of provable pre-statements. |
class mPPSt | ||
Syntax | cmthm 33834 | The set of theorems. |
class mThm | ||
Definition | df-mcn 33835 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mCN = Slot 1 | ||
Definition | df-mvar 33836 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVR = Slot 2 | ||
Definition | df-mty 33837 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mType = Slot 3 | ||
Definition | df-mtc 33838 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mTC = Slot 4 | ||
Definition | df-mmax 33839 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mAx = Slot 5 | ||
Definition | df-mvt 33840 | 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 33841 | 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 33842 | 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 33843 | 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 33844* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVars = (π‘ β V β¦ (π β (mExβπ‘) β¦ (ran (2nd βπ) β© (mVRβπ‘)))) | ||
Definition | df-mrsub 33845* | 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 33846* | 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 33847* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVH = (π‘ β V β¦ (π£ β (mVRβπ‘) β¦ β¨((mTypeβπ‘)βπ£), β¨βπ£ββ©β©)) | ||
Definition | df-mpst 33848* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mPreSt = (π‘ β V β¦ (({π β π« (mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ (mExβπ‘))) | ||
Definition | df-msr 33849* | 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 33850 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mStat = (π‘ β V β¦ ran (mStRedβπ‘)) | ||
Definition | df-mfs 33851* | 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 33852* | 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 33853* | Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mPPSt = (π‘ β V β¦ {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))}) | ||
Definition | df-mthm 33854 | Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mThm = (π‘ β V β¦ (β‘(mStRedβπ‘) β ((mStRedβπ‘) β (mPPStβπ‘)))) | ||
Theorem | mvtval 33855 | The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVTβπ) & β’ π = (mTypeβπ) β β’ π = ran π | ||
Theorem | mrexval 33856 | 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 33857 | 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 33858 | 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 33859 | 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 33860 | The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π = (mVarsβπ) β β’ (π β πΈ β (πβπ) = (ran (2nd βπ) β© π)) | ||
Theorem | mvrsfpw 33861 | 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 33862* | 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 33863* | 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 33864* | 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 | mrsubcv 33865 | The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β (πΆ βͺ π)) β ((πβπΉ)ββ¨βπββ©) = if(π β π΄, (πΉβπ), β¨βπββ©)) | ||
Theorem | mrsubvr 33866 | The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β π΄) β ((πβπΉ)ββ¨βπββ©) = (πΉβπ)) | ||
Theorem | mrsubff 33867 | A substitution is a function from π to π . (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ (π β π β π:(π βpm π)βΆ(π βm π )) | ||
Theorem | mrsubrn 33868 | Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ ran π = (π β (π βm π)) | ||
Theorem | mrsubff1 33869 | When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ (π β π β (π βΎ (π βm π)):(π βm π)β1-1β(π βm π )) | ||
Theorem | mrsubff1o 33870 | When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ (π β π β (π βΎ (π βm π)):(π βm π)β1-1-ontoβran π) | ||
Theorem | mrsub0 33871 | The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) β β’ (πΉ β ran π β (πΉββ ) = β ) | ||
Theorem | mrsubf 33872 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) β β’ (πΉ β ran π β πΉ:π βΆπ ) | ||
Theorem | mrsubccat 33873 | Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) β β’ ((πΉ β ran π β§ π β π β§ π β π ) β (πΉβ(π ++ π)) = ((πΉβπ) ++ (πΉβπ))) | ||
Theorem | mrsubcn 33874 | A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) & β’ π = (mVRβπ) & β’ πΆ = (mCNβπ) β β’ ((πΉ β ran π β§ π β (πΆ β π)) β (πΉββ¨βπββ©) = β¨βπββ©) | ||
Theorem | elmrsubrn 33875* | Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses (πΆ β π) because we don't know that πΆ and π are disjoint until we get to ismfs 33904.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) & β’ π = (mVRβπ) & β’ πΆ = (mCNβπ) β β’ (π β π β (πΉ β ran π β (πΉ:π βΆπ β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§ βπ₯ β π βπ¦ β π (πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))))) | ||
Theorem | mrsubco 33876 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) β β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ) β ran π) | ||
Theorem | mrsubvrs 33877* | The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mVRβπ) & β’ π = (mRExβπ) β β’ ((πΉ β ran π β§ π β π ) β (ran (πΉβπ) β© π) = βͺ π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) | ||
Theorem | msubffval 33878* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ (π β π β π = (π β (π βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) | ||
Theorem | msubfval 33879* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π) β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©)) | ||
Theorem | msubval 33880 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β πΈ) β ((πβπΉ)βπ) = β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) | ||
Theorem | msubrsub 33881 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β πΈ) β (2nd β((πβπΉ)βπ)) = ((πβπΉ)β(2nd βπ))) | ||
Theorem | msubty 33882 | The type of a substituted expression is the same as the original type. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β πΈ) β (1st β((πβπΉ)βπ)) = (1st βπ)) | ||
Theorem | elmsubrn 33883* | Characterization of substitution in terms of raw substitution, without reference to the generating functions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) & β’ π = (mSubstβπ) β β’ ran π = ran (π β ran π β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) | ||
Theorem | msubrn 33884 | Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) β β’ ran π = (π β (π βm π)) | ||
Theorem | msubff 33885 | A substitution is a function from πΈ to πΈ. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (π β π β π:(π βpm π)βΆ(πΈ βm πΈ)) | ||
Theorem | msubco 33886 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mSubstβπ) β β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ) β ran π) | ||
Theorem | msubf 33887 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (πΉ β ran π β πΉ:πΈβΆπΈ) | ||
Theorem | mvhfval 33888* | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mTypeβπ) & β’ π» = (mVHβπ) β β’ π» = (π£ β π β¦ β¨(πβπ£), β¨βπ£ββ©β©) | ||
Theorem | mvhval 33889 | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mTypeβπ) & β’ π» = (mVHβπ) β β’ (π β π β (π»βπ) = β¨(πβπ), β¨βπββ©β©) | ||
Theorem | mpstval 33890* | A pre-statement is an ordered triple, whose first member is a symmetric set of disjoint variable conditions, whose second member is a finite set of expressions, and whose third member is an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mDVβπ) & β’ πΈ = (mExβπ) & β’ π = (mPreStβπ) β β’ π = (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) | ||
Theorem | elmpst 33891 | Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mDVβπ) & β’ πΈ = (mExβπ) & β’ π = (mPreStβπ) β β’ (β¨π·, π», π΄β© β π β ((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin) β§ π΄ β πΈ)) | ||
Theorem | msrfval 33892* | Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVarsβπ) & β’ π = (mPreStβπ) & β’ π = (mStRedβπ) β β’ π = (π β π β¦ β¦(2nd β(1st βπ )) / ββ¦β¦(2nd βπ ) / πβ¦β¨((1st β(1st βπ )) β© β¦βͺ (π β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) | ||
Theorem | msrval 33893 | Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVarsβπ) & β’ π = (mPreStβπ) & β’ π = (mStRedβπ) & β’ π = βͺ (π β (π» βͺ {π΄})) β β’ (β¨π·, π», π΄β© β π β (π ββ¨π·, π», π΄β©) = β¨(π· β© (π Γ π)), π», π΄β©) | ||
Theorem | mpstssv 33894 | A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) β β’ π β ((V Γ V) Γ V) | ||
Theorem | mpst123 33895 | Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) β β’ (π β π β π = β¨(1st β(1st βπ)), (2nd β(1st βπ)), (2nd βπ)β©) | ||
Theorem | mpstrcl 33896 | The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) β β’ (β¨π·, π», π΄β© β π β (π· β V β§ π» β V β§ π΄ β V)) | ||
Theorem | msrf 33897 | The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π = (mStRedβπ) β β’ π :πβΆπ | ||
Theorem | msrrcl 33898 | If π and π have the same reduct, then one is a pre-statement iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π = (mStRedβπ) β β’ ((π βπ) = (π βπ) β (π β π β π β π)) | ||
Theorem | mstaval 33899 | Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mStatβπ) β β’ π = ran π | ||
Theorem | msrid 33900 | The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mStatβπ) β β’ (π β π β (π βπ) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |