![]() |
Metamath
Proof Explorer Theorem List (p. 346 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mrsubff1o 34501 | 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 34502 | The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) β β’ (πΉ β ran π β (πΉββ ) = β ) | ||
Theorem | mrsubf 34503 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) β β’ (πΉ β ran π β πΉ:π βΆπ ) | ||
Theorem | mrsubccat 34504 | Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) β β’ ((πΉ β ran π β§ π β π β§ π β π ) β (πΉβ(π ++ π)) = ((πΉβπ) ++ (πΉβπ))) | ||
Theorem | mrsubcn 34505 | A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) & β’ π = (mVRβπ) & β’ πΆ = (mCNβπ) β β’ ((πΉ β ran π β§ π β (πΆ β π)) β (πΉββ¨βπββ©) = β¨βπββ©) | ||
Theorem | elmrsubrn 34506* | 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 34535.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) & β’ π = (mRExβπ) & β’ π = (mVRβπ) & β’ πΆ = (mCNβπ) β β’ (π β π β (πΉ β ran π β (πΉ:π βΆπ β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§ βπ₯ β π βπ¦ β π (πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))))) | ||
Theorem | mrsubco 34507 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mRSubstβπ) β β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ) β ran π) | ||
Theorem | mrsubvrs 34508* | 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 34509* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ (π β π β π = (π β (π βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) | ||
Theorem | msubfval 34510* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π) β (πβπΉ) = (π β πΈ β¦ β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©)) | ||
Theorem | msubval 34511 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β πΈ) β ((πβπΉ)βπ) = β¨(1st βπ), ((πβπΉ)β(2nd βπ))β©) | ||
Theorem | msubrsub 34512 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mRSubstβπ) β β’ ((πΉ:π΄βΆπ β§ π΄ β π β§ π β πΈ) β (2nd β((πβπΉ)βπ)) = ((πβπΉ)β(2nd βπ))) | ||
Theorem | msubty 34513 | 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 34514* | 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 34515 | 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 34516 | A substitution is a function from πΈ to πΈ. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (π β π β π:(π βpm π)βΆ(πΈ βm πΈ)) | ||
Theorem | msubco 34517 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mSubstβπ) β β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ) β ran π) | ||
Theorem | msubf 34518 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (πΉ β ran π β πΉ:πΈβΆπΈ) | ||
Theorem | mvhfval 34519* | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mTypeβπ) & β’ π» = (mVHβπ) β β’ π» = (π£ β π β¦ β¨(πβπ£), β¨βπ£ββ©β©) | ||
Theorem | mvhval 34520 | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mTypeβπ) & β’ π» = (mVHβπ) β β’ (π β π β (π»βπ) = β¨(πβπ), β¨βπββ©β©) | ||
Theorem | mpstval 34521* | 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 34522 | Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mDVβπ) & β’ πΈ = (mExβπ) & β’ π = (mPreStβπ) β β’ (β¨π·, π», π΄β© β π β ((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin) β§ π΄ β πΈ)) | ||
Theorem | msrfval 34523* | 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 34524 | Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVarsβπ) & β’ π = (mPreStβπ) & β’ π = (mStRedβπ) & β’ π = βͺ (π β (π» βͺ {π΄})) β β’ (β¨π·, π», π΄β© β π β (π ββ¨π·, π», π΄β©) = β¨(π· β© (π Γ π)), π», π΄β©) | ||
Theorem | mpstssv 34525 | A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) β β’ π β ((V Γ V) Γ V) | ||
Theorem | mpst123 34526 | Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) β β’ (π β π β π = β¨(1st β(1st βπ)), (2nd β(1st βπ)), (2nd βπ)β©) | ||
Theorem | mpstrcl 34527 | The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) β β’ (β¨π·, π», π΄β© β π β (π· β V β§ π» β V β§ π΄ β V)) | ||
Theorem | msrf 34528 | The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π = (mStRedβπ) β β’ π :πβΆπ | ||
Theorem | msrrcl 34529 | 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 34530 | Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mStatβπ) β β’ π = ran π | ||
Theorem | msrid 34531 | The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mStatβπ) β β’ (π β π β (π βπ) = π) | ||
Theorem | msrfo 34532 | The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mStatβπ) & β’ π = (mPreStβπ) β β’ π :πβontoβπ | ||
Theorem | mstapst 34533 | A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π = (mStatβπ) β β’ π β π | ||
Theorem | elmsta 34534 | Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π = (mStatβπ) & β’ π = (mVarsβπ) & β’ π = βͺ (π β (π» βͺ {π΄})) β β’ (β¨π·, π», π΄β© β π β (β¨π·, π», π΄β© β π β§ π· β (π Γ π))) | ||
Theorem | ismfs 34535* | A formal system is a tuple β¨mCN, mVR, mType, mVT, mTC, mAxβ© such that: mCN and mVR are disjoint; mType is a function from mVR to mVT; mVT is a subset of mTC; mAx is a set of statements; and for each variable typecode, there are infinitely many variables of that type. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) & β’ π = (mTypeβπ) & β’ πΉ = (mVTβπ) & β’ πΎ = (mTCβπ) & β’ π΄ = (mAxβπ) & β’ π = (mStatβπ) β β’ (π β π β (π β mFS β (((πΆ β© π) = β β§ π:πβΆπΎ) β§ (π΄ β π β§ βπ£ β πΉ Β¬ (β‘π β {π£}) β Fin)))) | ||
Theorem | mfsdisj 34536 | The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΆ = (mCNβπ) & β’ π = (mVRβπ) β β’ (π β mFS β (πΆ β© π) = β ) | ||
Theorem | mtyf2 34537 | The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΎ = (mTCβπ) & β’ π = (mTypeβπ) β β’ (π β mFS β π:πβΆπΎ) | ||
Theorem | mtyf 34538 | The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΉ = (mVTβπ) & β’ π = (mTypeβπ) β β’ (π β mFS β π:πβΆπΉ) | ||
Theorem | mvtss 34539 | The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΉ = (mVTβπ) & β’ πΎ = (mTCβπ) β β’ (π β mFS β πΉ β πΎ) | ||
Theorem | maxsta 34540 | An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π΄ = (mAxβπ) & β’ π = (mStatβπ) β β’ (π β mFS β π΄ β π) | ||
Theorem | mvtinf 34541 | Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ πΉ = (mVTβπ) & β’ π = (mTypeβπ) β β’ ((π β mFS β§ π β πΉ) β Β¬ (β‘π β {π}) β Fin) | ||
Theorem | msubff1 34542 | When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ π = (mRExβπ) & β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) β β’ (π β mFS β (π βΎ (π βm π)):(π βm π)β1-1β(πΈ βm πΈ)) | ||
Theorem | msubff1o 34543 | 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βπ) & β’ π = (mSubstβπ) β β’ (π β mFS β (π βΎ (π βm π)):(π βm π)β1-1-ontoβran π) | ||
Theorem | mvhf 34544 | The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π» = (mVHβπ) β β’ (π β mFS β π»:πβΆπΈ) | ||
Theorem | mvhf1 34545 | The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mVRβπ) & β’ πΈ = (mExβπ) & β’ π» = (mVHβπ) β β’ (π β mFS β π»:πβ1-1βπΈ) | ||
Theorem | msubvrs 34546* | 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.) |
β’ π = (mSubstβπ) & β’ πΈ = (mExβπ) & β’ π = (mVarsβπ) & β’ π» = (mVHβπ) β β’ ((π β mFS β§ πΉ β ran π β§ π β πΈ) β (πβ(πΉβπ)) = βͺ π₯ β (πβπ)(πβ(πΉβ(π»βπ₯)))) | ||
Theorem | mclsrcl 34547 | Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) β β’ (π΄ β (πΎπΆπ΅) β (π β V β§ πΎ β π· β§ π΅ β πΈ)) | ||
Theorem | mclsssvlem 34548* | Lemma for mclsssv 34550. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) & β’ π΄ = (mAxβπ) & β’ π = (mSubstβπ) & β’ π = (mVarsβπ) β β’ (π β β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ) | ||
Theorem | mclsval 34549* | The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) & β’ π΄ = (mAxβπ) & β’ π = (mSubstβπ) & β’ π = (mVarsβπ) β β’ (π β (πΎπΆπ΅) = β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) | ||
Theorem | mclsssv 34550 | The closure of a set of expressions is a set of expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) β β’ (π β (πΎπΆπ΅) β πΈ) | ||
Theorem | ssmclslem 34551 | Lemma for ssmcls 34553. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) β β’ (π β (π΅ βͺ ran π») β (πΎπΆπ΅)) | ||
Theorem | vhmcls 34552 | All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π» = (mVHβπ) & β’ π = (mVRβπ) & β’ (π β π β π) β β’ (π β (π»βπ) β (πΎπΆπ΅)) | ||
Theorem | ssmcls 34553 | The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) β β’ (π β π΅ β (πΎπΆπ΅)) | ||
Theorem | ss2mcls 34554 | The closure is monotonic under subsets of the original set of expressions and the set of disjoint variable conditions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ (π β π β πΎ) & β’ (π β π β π΅) β β’ (π β (ππΆπ) β (πΎπΆπ΅)) | ||
Theorem | mclsax 34555* | The closure is closed under axiom application. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π΄ = (mAxβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β β¨π, π, πβ© β π΄) & β’ (π β π β ran πΏ) & β’ ((π β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) & β’ ((π β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) & β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) β β’ (π β (πβπ) β (πΎπΆπ΅)) | ||
Theorem | mclsind 34556* | Induction theorem for closure: any other set π closed under the axioms and the hypotheses contains all the elements of the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π΄ = (mAxβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β π΅ β π) & β’ ((π β§ π£ β π) β (π»βπ£) β π) & β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β β’ (π β (πΎπΆπ΅) β π) | ||
Theorem | mppspstlem 34557* | Lemma for mppspst 34560. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) & β’ πΆ = (mClsβπ) β β’ {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} β π | ||
Theorem | mppsval 34558* | Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) & β’ πΆ = (mClsβπ) β β’ π½ = {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} | ||
Theorem | elmpps 34559 | Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) & β’ πΆ = (mClsβπ) β β’ (β¨π·, π», π΄β© β π½ β (β¨π·, π», π΄β© β π β§ π΄ β (π·πΆπ»))) | ||
Theorem | mppspst 34560 | A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mPreStβπ) & β’ π½ = (mPPStβπ) β β’ π½ β π | ||
Theorem | mthmval 34561 | A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. Unlike the difference between pre-statement and statement, this application of the reduct is not necessarily trivial: there are theorems that are not themselves provable but are provable once enough "dummy variables" are introduced. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ π = (β‘π β (π β π½)) | ||
Theorem | elmthm 34562* | A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ (π β π β βπ₯ β π½ (π βπ₯) = (π βπ)) | ||
Theorem | mthmi 34563 | A statement whose reduct is the reduct of a provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ ((π β π½ β§ (π βπ) = (π βπ)) β π β π) | ||
Theorem | mthmsta 34564 | A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mThmβπ) & β’ π = (mPreStβπ) β β’ π β π | ||
Theorem | mppsthm 34565 | A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) β β’ π½ β π | ||
Theorem | mthmblem 34566 | Lemma for mthmb 34567. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mThmβπ) β β’ ((π βπ) = (π βπ) β (π β π β π β π)) | ||
Theorem | mthmb 34567 | If two statements have the same reduct then one is a theorem iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π = (mThmβπ) β β’ ((π βπ) = (π βπ) β (π β π β π β π)) | ||
Theorem | mthmpps 34568 | Given a theorem, there is an explicitly definable witnessing provable pre-statement for the provability of the theorem. (However, this pre-statement requires infinitely many disjoint variable conditions, which is sometimes inconvenient.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (mStRedβπ) & β’ π½ = (mPPStβπ) & β’ π = (mThmβπ) & β’ π· = (mDVβπ) & β’ π = (mVarsβπ) & β’ π = βͺ (π β (π» βͺ {π΄})) & β’ π = (πΆ βͺ (π· β (π Γ π))) β β’ (π β mFS β (β¨πΆ, π», π΄β© β π β (β¨π, π», π΄β© β π½ β§ (π ββ¨π, π», π΄β©) = (π ββ¨πΆ, π», π΄β©)))) | ||
Theorem | mclsppslem 34569* | The closure is closed under application of provable pre-statements. (Compare mclsax 34555.) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π½ = (mPPStβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β β¨π, π, πβ© β π½) & β’ (π β π β ran πΏ) & β’ ((π β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) & β’ ((π β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) & β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) & β’ (π β β¨π, π, πβ© β (mAxβπ)) & β’ (π β π β ran πΏ) & β’ (π β (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) & β’ (π β βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β β’ (π β (π βπ) β (β‘π β (πΎπΆπ΅))) | ||
Theorem | mclspps 34570* | The closure is closed under application of provable pre-statements. (Compare mclsax 34555.) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π· = (mDVβπ) & β’ πΈ = (mExβπ) & β’ πΆ = (mClsβπ) & β’ (π β π β mFS) & β’ (π β πΎ β π·) & β’ (π β π΅ β πΈ) & β’ π½ = (mPPStβπ) & β’ πΏ = (mSubstβπ) & β’ π = (mVRβπ) & β’ π» = (mVHβπ) & β’ π = (mVarsβπ) & β’ (π β β¨π, π, πβ© β π½) & β’ (π β π β ran πΏ) & β’ ((π β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) & β’ ((π β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) & β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) β β’ (π β (πβπ) β (πΎπΆπ΅)) | ||
Syntax | cm0s 34571 | Mapping expressions to statements. |
class m0St | ||
Syntax | cmsa 34572 | The set of syntax axioms. |
class mSA | ||
Syntax | cmwgfs 34573 | The set of weakly grammatical formal systems. |
class mWGFS | ||
Syntax | cmsy 34574 | The syntax typecode function. |
class mSyn | ||
Syntax | cmesy 34575 | The syntax typecode function for expressions. |
class mESyn | ||
Syntax | cmgfs 34576 | The set of grammatical formal systems. |
class mGFS | ||
Syntax | cmtree 34577 | The set of proof trees. |
class mTree | ||
Syntax | cmst 34578 | The set of syntax trees. |
class mST | ||
Syntax | cmsax 34579 | The indexing set for a syntax axiom. |
class mSAX | ||
Syntax | cmufs 34580 | The set of unambiguous formal sytems. |
class mUFS | ||
Definition | df-m0s 34581 | Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ m0St = (π β V β¦ β¨β , β , πβ©) | ||
Definition | df-msa 34582* | Define the set of syntax axioms. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mSA = (π‘ β V β¦ {π β (mExβπ‘) β£ ((m0Stβπ) β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘) β§ Fun (β‘(2nd βπ) βΎ (mVRβπ‘)))}) | ||
Definition | df-mwgfs 34583* | Define the set of weakly grammatical formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mWGFS = {π‘ β mFS β£ βπβββπ((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘)))} | ||
Definition | df-msyn 34584 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mSyn = Slot 6 | ||
Definition | df-mesyn 34585* | Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.) |
β’ mESyn = (π‘ β V β¦ (π β (mTCβπ‘), π β (mRExβπ‘) β¦ (((mSynβπ‘)βπ)m0Stπ))) | ||
Definition | df-mgfs 34586* | Define the set of grammatical formal systems. (Contributed by Mario Carneiro, 12-Jun-2023.) |
β’ mGFS = {π‘ β mWGFS β£ ((mSynβπ‘):(mTCβπ‘)βΆ(mVTβπ‘) β§ βπ β (mVTβπ‘)((mSynβπ‘)βπ) = π β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)))} | ||
Definition | df-mtree 34587* | Define the set of proof trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mTree = (π‘ β V β¦ (π β π« (mDVβπ‘), β β π« (mExβπ‘) β¦ β© {π β£ (βπ β ran (mVHβπ‘)ππβ¨(m0Stβπ), β β© β§ βπ β β ππβ¨((mStRedβπ‘)ββ¨π, β, πβ©), β β© β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π) β ({(π βπ)} Γ Xπ β (π βͺ ((mVHβπ‘) β βͺ ((mVarsβπ‘) β (π βͺ {π}))))(π β {(π βπ)})) β π)))})) | ||
Definition | df-mst 34588 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mST = (π‘ β V β¦ ((β (mTreeβπ‘)β ) βΎ ((mExβπ‘) βΎ (mVTβπ‘)))) | ||
Definition | df-msax 34589* | Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mSAX = (π‘ β V β¦ (π β (mSAβπ‘) β¦ ((mVHβπ‘) β ((mVarsβπ‘)βπ)))) | ||
Definition | df-mufs 34590 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUFS = {π‘ β mGFS β£ Fun (mSTβπ‘)} | ||
Syntax | cmuv 34591 | The universe of a model. |
class mUV | ||
Syntax | cmvl 34592 | The set of valuations. |
class mVL | ||
Syntax | cmvsb 34593 | Substitution for a valuation. |
class mVSubst | ||
Syntax | cmfsh 34594 | The freshness relation of a model. |
class mFresh | ||
Syntax | cmfr 34595 | The set of freshness relations. |
class mFRel | ||
Syntax | cmevl 34596 | The evaluation function of a model. |
class mEval | ||
Syntax | cmdl 34597 | The set of models. |
class mMdl | ||
Syntax | cusyn 34598 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 34599 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 34600 | The interpretation function of the model. |
class mItp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |