Home | Metamath
Proof Explorer Theorem List (p. 328 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-gzf 32701* | 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 32702 | The set of constants. |
class mCN | ||
Syntax | cmvar 32703 | The set of variables. |
class mVR | ||
Syntax | cmty 32704 | The type function. |
class mType | ||
Syntax | cmvt 32705 | The set of variable typecodes. |
class mVT | ||
Syntax | cmtc 32706 | The set of typecodes. |
class mTC | ||
Syntax | cmax 32707 | The set of axioms. |
class mAx | ||
Syntax | cmrex 32708 | The set of raw expressions. |
class mREx | ||
Syntax | cmex 32709 | The set of expressions. |
class mEx | ||
Syntax | cmdv 32710 | The set of distinct variables. |
class mDV | ||
Syntax | cmvrs 32711 | The variables in an expression. |
class mVars | ||
Syntax | cmrsub 32712 | The set of raw substitutions. |
class mRSubst | ||
Syntax | cmsub 32713 | The set of substitutions. |
class mSubst | ||
Syntax | cmvh 32714 | The set of variable hypotheses. |
class mVH | ||
Syntax | cmpst 32715 | The set of pre-statements. |
class mPreSt | ||
Syntax | cmsr 32716 | The reduct of a pre-statement. |
class mStRed | ||
Syntax | cmsta 32717 | The set of statements. |
class mStat | ||
Syntax | cmfs 32718 | The set of formal systems. |
class mFS | ||
Syntax | cmcls 32719 | The closure of a set of statements. |
class mCls | ||
Syntax | cmpps 32720 | The set of provable pre-statements. |
class mPPSt | ||
Syntax | cmthm 32721 | The set of theorems. |
class mThm | ||
Definition | df-mcn 32722 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mCN = Slot 1 | ||
Definition | df-mvar 32723 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVR = Slot 2 | ||
Definition | df-mty 32724 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mType = Slot 3 | ||
Definition | df-mtc 32725 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mTC = Slot 4 | ||
Definition | df-mmax 32726 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mAx = Slot 5 | ||
Definition | df-mvt 32727 | 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 32728 | 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 32729 | 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 32730 | 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 32731* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡)))) | ||
Definition | df-mrsub 32732* | 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 32733* | 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 32734* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ 〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉)) | ||
Definition | df-mpst 32735* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))) | ||
Definition | df-msr 32736* | 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 32737 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡)) | ||
Definition | df-mfs 32738* | 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 32739* | 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 32740* | Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mPPSt = (𝑡 ∈ V ↦ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) | ||
Definition | df-mthm 32741 | Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡)))) | ||
Theorem | mvtval 32742 | The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ 𝑉 = ran 𝑌 | ||
Theorem | mrexval 32743 | 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 32744 | 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 32745 | 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 32746 | 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 32747 | The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑊 = (mVars‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉)) | ||
Theorem | mvrsfpw 32748 | 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 32749* | 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 32750* | 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 32751* | 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 32752 | The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘〈“𝑋”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) | ||
Theorem | mrsubvr 32753 | The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘〈“𝑋”〉) = (𝐹‘𝑋)) | ||
Theorem | mrsubff 32754 | A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) | ||
Theorem | mrsubrn 32755 | 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 32756 | 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 32757 | 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 32758 | The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅) | ||
Theorem | mrsubf 32759 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) | ||
Theorem | mrsubccat 32760 | Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) | ||
Theorem | mrsubcn 32761 | A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐶 = (mCN‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑋”〉) = 〈“𝑋”〉) | ||
Theorem | elmrsubrn 32762* | 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 32791.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐶 = (mCN‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))) | ||
Theorem | mrsubco 32763 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) | ||
Theorem | mrsubvrs 32764* | 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 32765* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) | ||
Theorem | msubfval 32766* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) | ||
Theorem | msubval 32767 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → ((𝑆‘𝐹)‘𝑋) = 〈(1st ‘𝑋), ((𝑂‘𝐹)‘(2nd ‘𝑋))〉) | ||
Theorem | msubrsub 32768 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (2nd ‘((𝑆‘𝐹)‘𝑋)) = ((𝑂‘𝐹)‘(2nd ‘𝑋))) | ||
Theorem | msubty 32769 | 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 32770* | 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 32771 | 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 32772 | A substitution is a function from 𝐸 to 𝐸. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑m 𝐸)) | ||
Theorem | msubco 32773 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mSubst‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) | ||
Theorem | msubf 32774 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝐸⟶𝐸) | ||
Theorem | mvhfval 32775* | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ 〈(𝑌‘𝑣), 〈“𝑣”〉〉) | ||
Theorem | mvhval 32776 | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝐻‘𝑋) = 〈(𝑌‘𝑋), 〈“𝑋”〉〉) | ||
Theorem | mpstval 32777* | 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 32778 | Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸)) | ||
Theorem | msrfval 32779* | 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 32780 | Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVars‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴})) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝑅‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | ||
Theorem | mpstssv 32781 | A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ 𝑃 ⊆ ((V × V) × V) | ||
Theorem | mpst123 32782 | Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑃 → 𝑋 = 〈(1st ‘(1st ‘𝑋)), (2nd ‘(1st ‘𝑋)), (2nd ‘𝑋)〉) | ||
Theorem | mpstrcl 32783 | The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V)) | ||
Theorem | msrf 32784 | The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑅 = (mStRed‘𝑇) ⇒ ⊢ 𝑅:𝑃⟶𝑃 | ||
Theorem | msrrcl 32785 | 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 32786 | Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ 𝑆 = ran 𝑅 | ||
Theorem | msrid 32787 | The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑆 → (𝑅‘𝑋) = 𝑋) | ||
Theorem | msrfo 32788 | The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ 𝑅:𝑃–onto→𝑆 | ||
Theorem | mstapst 32789 | A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ 𝑆 ⊆ 𝑃 | ||
Theorem | elmsta 32790 | Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) & ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴})) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 ↔ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍))) | ||
Theorem | ismfs 32791* | 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 32792 | The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → (𝐶 ∩ 𝑉) = ∅) | ||
Theorem | mtyf2 32793 | The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐾) | ||
Theorem | mtyf 32794 | The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐹) | ||
Theorem | mvtss 32795 | The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐹 ⊆ 𝐾) | ||
Theorem | maxsta 32796 | An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ 𝑆) | ||
Theorem | mvtinf 32797 | Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ ((𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹) → ¬ (◡𝑌 “ {𝑋}) ∈ Fin) | ||
Theorem | msubff1 32798 | 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 32799 | 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 32800 | The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |