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-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cgoa 33801 | The Godel-set of conjunction. |
class β§π | ||
Syntax | cgoi 33802 | The Godel-set of implication. |
class βπ | ||
Syntax | cgoo 33803 | The Godel-set of disjunction. |
class β¨π | ||
Syntax | cgob 33804 | The Godel-set of equivalence. |
class βπ | ||
Syntax | cgoq 33805 | The Godel-set of equality. |
class =π | ||
Syntax | cgox 33806 | The Godel-set of existential quantification. (Note that this is not a wff.) |
class βπππ | ||
Definition | df-gonot 33807 | 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 33808* | 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 33809* | 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 33810* | 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 33811* | 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 33812* | 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 2709 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 33813 | 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 33814 | The Axiom of Extensionality. |
class AxExt | ||
Syntax | cgzr 33815 | The Axiom Scheme of Replacement. |
class AxRep | ||
Syntax | cgzp 33816 | The Axiom of Power Sets. |
class AxPow | ||
Syntax | cgzu 33817 | The Axiom of Unions. |
class AxUn | ||
Syntax | cgzg 33818 | The Axiom of Regularity. |
class AxReg | ||
Syntax | cgzi 33819 | The Axiom of Infinity. |
class AxInf | ||
Syntax | cgzf 33820 | The set of models of ZF. |
class ZF | ||
Definition | df-gzext 33821 | 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 33822 | 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 33823 | 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 33824 | 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 33825 | 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 33826 | 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 33827* | 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 33828 | The set of constants. |
class mCN | ||
Syntax | cmvar 33829 | The set of variables. |
class mVR | ||
Syntax | cmty 33830 | The type function. |
class mType | ||
Syntax | cmvt 33831 | The set of variable typecodes. |
class mVT | ||
Syntax | cmtc 33832 | The set of typecodes. |
class mTC | ||
Syntax | cmax 33833 | The set of axioms. |
class mAx | ||
Syntax | cmrex 33834 | The set of raw expressions. |
class mREx | ||
Syntax | cmex 33835 | The set of expressions. |
class mEx | ||
Syntax | cmdv 33836 | The set of distinct variables. |
class mDV | ||
Syntax | cmvrs 33837 | The variables in an expression. |
class mVars | ||
Syntax | cmrsub 33838 | The set of raw substitutions. |
class mRSubst | ||
Syntax | cmsub 33839 | The set of substitutions. |
class mSubst | ||
Syntax | cmvh 33840 | The set of variable hypotheses. |
class mVH | ||
Syntax | cmpst 33841 | The set of pre-statements. |
class mPreSt | ||
Syntax | cmsr 33842 | The reduct of a pre-statement. |
class mStRed | ||
Syntax | cmsta 33843 | The set of statements. |
class mStat | ||
Syntax | cmfs 33844 | The set of formal systems. |
class mFS | ||
Syntax | cmcls 33845 | The closure of a set of statements. |
class mCls | ||
Syntax | cmpps 33846 | The set of provable pre-statements. |
class mPPSt | ||
Syntax | cmthm 33847 | The set of theorems. |
class mThm | ||
Definition | df-mcn 33848 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mCN = Slot 1 | ||
Definition | df-mvar 33849 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVR = Slot 2 | ||
Definition | df-mty 33850 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mType = Slot 3 | ||
Definition | df-mtc 33851 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mTC = Slot 4 | ||
Definition | df-mmax 33852 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mAx = Slot 5 | ||
Definition | df-mvt 33853 | 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 33854 | 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 33855 | 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 33856 | 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 33857* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVars = (π‘ β V β¦ (π β (mExβπ‘) β¦ (ran (2nd βπ) β© (mVRβπ‘)))) | ||
Definition | df-mrsub 33858* | 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 33859* | 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 33860* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVH = (π‘ β V β¦ (π£ β (mVRβπ‘) β¦ β¨((mTypeβπ‘)βπ£), β¨βπ£ββ©β©)) | ||
Definition | df-mpst 33861* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mPreSt = (π‘ β V β¦ (({π β π« (mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ (mExβπ‘))) | ||
Definition | df-msr 33862* | 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 33863 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mStat = (π‘ β V β¦ ran (mStRedβπ‘)) | ||
Definition | df-mfs 33864* | 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 33865* | 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 33866* | Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mPPSt = (π‘ β V β¦ {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))}) | ||
Definition | df-mthm 33867 | Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mThm = (π‘ β V β¦ (β‘(mStRedβπ‘) β ((mStRedβπ‘) β (mPPStβπ‘)))) | ||
Theorem | mvtval 33868 | The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVTβπ) & β’ π = (mTypeβπ) β β’ π = ran π | ||
Theorem | mrexval 33869 | 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 33870 | 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 33871 | 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 33872 | 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 33873 | The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π = (mVarsβπ) β β’ (π β πΈ β (πβπ) = (ran (2nd βπ) β© π)) | ||
Theorem | mvrsfpw 33874 | 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 33875* | 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 33876* | 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 33877* | 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 33878 | The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β (πΆ βͺ π)) β ((πβπΉ)ββ¨βπββ©) = if(π β π΄, (πΉβπ), β¨βπββ©)) | ||
Theorem | mrsubvr 33879 | The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β π΄) β ((πβπΉ)ββ¨βπββ©) = (πΉβπ)) | ||
Theorem | mrsubff 33880 | A substitution is a function from π to π . (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mRSubstβπ) β β’ (π β π β π:(π βpm π)βΆ(π βm π )) | ||
Theorem | mrsubrn 33881 | 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 33882 | 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 33883 | 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 33884 | The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) β β’ (πΉ β ran π β (πΉββ ) = β ) | ||
Theorem | mrsubf 33885 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) β β’ (πΉ β ran π β πΉ:π βΆπ ) | ||
Theorem | mrsubccat 33886 | Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) β β’ ((πΉ β ran π β§ π β π β§ π β π ) β (πΉβ(π ++ π)) = ((πΉβπ) ++ (πΉβπ))) | ||
Theorem | mrsubcn 33887 | A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) & β’ π = (mVRβπ) & β’ πΆ = (mCNβπ) β β’ ((πΉ β ran π β§ π β (πΆ β π)) β (πΉββ¨βπββ©) = β¨βπββ©) | ||
Theorem | elmrsubrn 33888* | 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 33917.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) & β’ π = (mVRβπ) & β’ πΆ = (mCNβπ) β β’ (π β π β (πΉ β ran π β (πΉ:π βΆπ β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§ βπ₯ β π βπ¦ β π (πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))))) | ||
Theorem | mrsubco 33889 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) β β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ) β ran π) | ||
Theorem | mrsubvrs 33890* | 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 33891* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ (π β π β π = (π β (π βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) | ||
Theorem | msubfval 33892* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π) β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©)) | ||
Theorem | msubval 33893 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β πΈ) β ((πβπΉ)βπ) = β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) | ||
Theorem | msubrsub 33894 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β πΈ) β (2nd β((πβπΉ)βπ)) = ((πβπΉ)β(2nd βπ))) | ||
Theorem | msubty 33895 | 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 33896* | 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 33897 | 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 33898 | A substitution is a function from πΈ to πΈ. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (π β π β π:(π βpm π)βΆ(πΈ βm πΈ)) | ||
Theorem | msubco 33899 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mSubstβπ) β β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ) β ran π) | ||
Theorem | msubf 33900 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (πΉ β ran π β πΉ:πΈβΆπΈ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |