P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-gonot 33301	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 33302*	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 33303*	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 33304*	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 33305*	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 33306*	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 33307	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.)
⊢ ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈
20.6.12  Models of ZF
Syntax	cgze 33308	The Axiom of Extensionality.
class AxExt
Syntax	cgzr 33309	The Axiom Scheme of Replacement.
class AxRep
Syntax	cgzp 33310	The Axiom of Power Sets.
class AxPow
Syntax	cgzu 33311	The Axiom of Unions.
class AxUn
Syntax	cgzg 33312	The Axiom of Regularity.
class AxReg
Syntax	cgzi 33313	The Axiom of Infinity.
class AxInf
Syntax	cgzf 33314	The set of models of ZF.
class ZF
Definition	df-gzext 33315	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 33316	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 33317	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 33318	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 33319	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 33320	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 33321*	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‘𝑢))}
20.6.13  Metamath formal systems 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 33322	The set of constants.
class mCN
Syntax	cmvar 33323	The set of variables.
class mVR
Syntax	cmty 33324	The type function.
class mType
Syntax	cmvt 33325	The set of variable typecodes.
class mVT
Syntax	cmtc 33326	The set of typecodes.
class mTC
Syntax	cmax 33327	The set of axioms.
class mAx
Syntax	cmrex 33328	The set of raw expressions.
class mREx
Syntax	cmex 33329	The set of expressions.
class mEx
Syntax	cmdv 33330	The set of distinct variables.
class mDV
Syntax	cmvrs 33331	The variables in an expression.
class mVars
Syntax	cmrsub 33332	The set of raw substitutions.
class mRSubst
Syntax	cmsub 33333	The set of substitutions.
class mSubst
Syntax	cmvh 33334	The set of variable hypotheses.
class mVH
Syntax	cmpst 33335	The set of pre-statements.
class mPreSt
Syntax	cmsr 33336	The reduct of a pre-statement.
class mStRed
Syntax	cmsta 33337	The set of statements.
class mStat
Syntax	cmfs 33338	The set of formal systems.
class mFS
Syntax	cmcls 33339	The closure of a set of statements.
class mCls
Syntax	cmpps 33340	The set of provable pre-statements.
class mPPSt
Syntax	cmthm 33341	The set of theorems.
class mThm
Definition	df-mcn 33342	Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mCN = Slot 1
Definition	df-mvar 33343	Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVR = Slot 2
Definition	df-mty 33344	Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mType = Slot 3
Definition	df-mtc 33345	Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mTC = Slot 4
Definition	df-mmax 33346	Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mAx = Slot 5
Definition	df-mvt 33347	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 33348	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 33349	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 33350	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 33351*	Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))
Definition	df-mrsub 33352*	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 33353*	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 33354*	Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
Definition	df-mpst 33355*	Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Definition	df-msr 33356*	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 33357	Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡))
Definition	df-mfs 33358*	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 33359*	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 33360*	Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPPSt = (𝑡 ∈ V ↦ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))})
Definition	df-mthm 33361	Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡))))
Theorem	mvtval 33362	The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ 𝑉 = ran 𝑌
Theorem	mrexval 33363	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 33364	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 33365	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 33366	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 33367	The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑊 = (mVars‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉))
Theorem	mvrsfpw 33368	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 33369*	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 33370*	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 33371*	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 33372	The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), ⟨“𝑋”⟩))
Theorem	mrsubvr 33373	The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = (𝐹‘𝑋))
Theorem	mrsubff 33374	A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅))
Theorem	mrsubrn 33375	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 33376	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 33377	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 33378	The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
Theorem	mrsubf 33379	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
Theorem	mrsubccat 33380	Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))
Theorem	mrsubcn 33381	A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑋”⟩) = ⟨“𝑋”⟩)
Theorem	elmrsubrn 33382*	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 33411.) (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))))
Theorem	mrsubco 33383	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	mrsubvrs 33384*	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 33385*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))⟩)))
Theorem	msubfval 33386*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))⟩))
Theorem	msubval 33387	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → ((𝑆‘𝐹)‘𝑋) = ⟨(1st ‘𝑋), ((𝑂‘𝐹)‘(2nd ‘𝑋))⟩)
Theorem	msubrsub 33388	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (2nd ‘((𝑆‘𝐹)‘𝑋)) = ((𝑂‘𝐹)‘(2nd ‘𝑋)))
Theorem	msubty 33389	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 33390*	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 33391	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 33392	A substitution is a function from 𝐸 to 𝐸. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑m 𝐸))
Theorem	msubco 33393	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	msubf 33394	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝐸⟶𝐸)
Theorem	mvhfval 33395*	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)
Theorem	mvhval 33396	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝐻‘𝑋) = ⟨(𝑌‘𝑋), ⟨“𝑋”⟩⟩)
Theorem	mpstval 33397*	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 33398	Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸))
Theorem	msrfval 33399*	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 33400	Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 → (𝑅‘⟨𝐷, 𝐻, 𝐴⟩) = ⟨(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)