![]() |
Metamath
Proof Explorer Theorem List (p. 340 of 472) | < 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-29746) |
![]() (29747-31269) |
![]() (31270-47184) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cgox 33901 | The Godel-set of existential quantification. (Note that this is not a wff.) |
class ∃𝑔𝑁𝑈 | ||
Definition | df-gonot 33902 | 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 33903* | 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 33904* | 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 33905* | 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 33906* | 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 33907* | 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 2707 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 33908 | 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 33909 | The Axiom of Extensionality. |
class AxExt | ||
Syntax | cgzr 33910 | The Axiom Scheme of Replacement. |
class AxRep | ||
Syntax | cgzp 33911 | The Axiom of Power Sets. |
class AxPow | ||
Syntax | cgzu 33912 | The Axiom of Unions. |
class AxUn | ||
Syntax | cgzg 33913 | The Axiom of Regularity. |
class AxReg | ||
Syntax | cgzi 33914 | The Axiom of Infinity. |
class AxInf | ||
Syntax | cgzf 33915 | The set of models of ZF. |
class ZF | ||
Definition | df-gzext 33916 | 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 33917 | 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 33918 | 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 33919 | 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 33920 | 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 33921 | 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 33922* | 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 33923 | The set of constants. |
class mCN | ||
Syntax | cmvar 33924 | The set of variables. |
class mVR | ||
Syntax | cmty 33925 | The type function. |
class mType | ||
Syntax | cmvt 33926 | The set of variable typecodes. |
class mVT | ||
Syntax | cmtc 33927 | The set of typecodes. |
class mTC | ||
Syntax | cmax 33928 | The set of axioms. |
class mAx | ||
Syntax | cmrex 33929 | The set of raw expressions. |
class mREx | ||
Syntax | cmex 33930 | The set of expressions. |
class mEx | ||
Syntax | cmdv 33931 | The set of distinct variables. |
class mDV | ||
Syntax | cmvrs 33932 | The variables in an expression. |
class mVars | ||
Syntax | cmrsub 33933 | The set of raw substitutions. |
class mRSubst | ||
Syntax | cmsub 33934 | The set of substitutions. |
class mSubst | ||
Syntax | cmvh 33935 | The set of variable hypotheses. |
class mVH | ||
Syntax | cmpst 33936 | The set of pre-statements. |
class mPreSt | ||
Syntax | cmsr 33937 | The reduct of a pre-statement. |
class mStRed | ||
Syntax | cmsta 33938 | The set of statements. |
class mStat | ||
Syntax | cmfs 33939 | The set of formal systems. |
class mFS | ||
Syntax | cmcls 33940 | The closure of a set of statements. |
class mCls | ||
Syntax | cmpps 33941 | The set of provable pre-statements. |
class mPPSt | ||
Syntax | cmthm 33942 | The set of theorems. |
class mThm | ||
Definition | df-mcn 33943 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mCN = Slot 1 | ||
Definition | df-mvar 33944 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVR = Slot 2 | ||
Definition | df-mty 33945 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mType = Slot 3 | ||
Definition | df-mtc 33946 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mTC = Slot 4 | ||
Definition | df-mmax 33947 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mAx = Slot 5 | ||
Definition | df-mvt 33948 | 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 33949 | 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 33950 | 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 33951 | 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 33952* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡)))) | ||
Definition | df-mrsub 33953* | 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 33954* | 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 33955* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ 〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉)) | ||
Definition | df-mpst 33956* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))) | ||
Definition | df-msr 33957* | 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 33958 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡)) | ||
Definition | df-mfs 33959* | 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 33960* | 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 33961* | Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mPPSt = (𝑡 ∈ V ↦ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) | ||
Definition | df-mthm 33962 | Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡)))) | ||
Theorem | mvtval 33963 | The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ 𝑉 = ran 𝑌 | ||
Theorem | mrexval 33964 | 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 33965 | 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 33966 | 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 33967 | 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 33968 | The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑊 = (mVars‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉)) | ||
Theorem | mvrsfpw 33969 | 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 33970* | 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 33971* | 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 33972* | 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 33973 | The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘〈“𝑋”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) | ||
Theorem | mrsubvr 33974 | The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘〈“𝑋”〉) = (𝐹‘𝑋)) | ||
Theorem | mrsubff 33975 | A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) | ||
Theorem | mrsubrn 33976 | 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 33977 | 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 33978 | 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 33979 | The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅) | ||
Theorem | mrsubf 33980 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) | ||
Theorem | mrsubccat 33981 | Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) | ||
Theorem | mrsubcn 33982 | A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐶 = (mCN‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑋”〉) = 〈“𝑋”〉) | ||
Theorem | elmrsubrn 33983* | 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 34012.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐶 = (mCN‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))) | ||
Theorem | mrsubco 33984 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) | ||
Theorem | mrsubvrs 33985* | 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 33986* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) | ||
Theorem | msubfval 33987* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) | ||
Theorem | msubval 33988 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → ((𝑆‘𝐹)‘𝑋) = 〈(1st ‘𝑋), ((𝑂‘𝐹)‘(2nd ‘𝑋))〉) | ||
Theorem | msubrsub 33989 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (2nd ‘((𝑆‘𝐹)‘𝑋)) = ((𝑂‘𝐹)‘(2nd ‘𝑋))) | ||
Theorem | msubty 33990 | 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 33991* | 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 33992 | 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 33993 | A substitution is a function from 𝐸 to 𝐸. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑m 𝐸)) | ||
Theorem | msubco 33994 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mSubst‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) | ||
Theorem | msubf 33995 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝐸⟶𝐸) | ||
Theorem | mvhfval 33996* | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ 〈(𝑌‘𝑣), 〈“𝑣”〉〉) | ||
Theorem | mvhval 33997 | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝐻‘𝑋) = 〈(𝑌‘𝑋), 〈“𝑋”〉〉) | ||
Theorem | mpstval 33998* | 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 33999 | Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸)) | ||
Theorem | msrfval 34000* | Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVars‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑅 = (mStRed‘𝑇) ⇒ ⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌〈((1st ‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉 “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |