P. 316 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31501-31600   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cmpps 31501	The set of provable pre-statements.
class mPPSt
Syntax	cmthm 31502	The set of theorems.
class mThm
Definition	df-mcn 31503	Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mCN = Slot 1
Definition	df-mvar 31504	Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVR = Slot 2
Definition	df-mty 31505	Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mType = Slot 3
Definition	df-mtc 31506	Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mTC = Slot 4
Definition	df-mmax 31507	Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mAx = Slot 5
Definition	df-mvt 31508	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 31509	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 31510	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 31511	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 31512*	Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))
Definition	df-mrsub 31513*	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 31514*	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 31515*	Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
Definition	df-mpst 31516*	Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Definition	df-msr 31517*	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 31518	Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡))
Definition	df-mfs 31519*	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 31520*	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 31521*	Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPPSt = (𝑡 ∈ V ↦ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))})
Definition	df-mthm 31522	Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡))))
Theorem	mvtval 31523	The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ 𝑉 = ran 𝑌
Theorem	mrexval 31524	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 31525	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 31526	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 31527	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 dv conditions of interest will be symmetric, so it does not matter.) (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐷 = (mDV‘𝑇)    ⇒   ⊢ 𝐷 = ((𝑉 × 𝑉) ∖ I )
Theorem	mvrsval 31528	The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑊 = (mVars‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉))
Theorem	mvrsfpw 31529	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 31530*	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 31531*	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 31532*	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 31533	The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), ⟨“𝑋”⟩))
Theorem	mrsubvr 31534	The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = (𝐹‘𝑋))
Theorem	mrsubff 31535	A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅))
Theorem	mrsubrn 31536	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 𝑆 = (𝑆 “ (𝑅 ↑𝑚 𝑉))
Theorem	mrsubff1 31537	When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝑅 ↑𝑚 𝑅))
Theorem	mrsubff1o 31538	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‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1-onto→ran 𝑆)
Theorem	mrsub0 31539	The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
Theorem	mrsubf 31540	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
Theorem	mrsubccat 31541	Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))
Theorem	mrsubcn 31542	A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑋”⟩) = ⟨“𝑋”⟩)
Theorem	elmrsubrn 31543*	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 31572.) (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))))
Theorem	mrsubco 31544	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	mrsubvrs 31545*	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 31546*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))⟩)))
Theorem	msubfval 31547*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))⟩))
Theorem	msubval 31548	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → ((𝑆‘𝐹)‘𝑋) = ⟨(1st ‘𝑋), ((𝑂‘𝐹)‘(2nd ‘𝑋))⟩)
Theorem	msubrsub 31549	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (2nd ‘((𝑆‘𝐹)‘𝑋)) = ((𝑂‘𝐹)‘(2nd ‘𝑋)))
Theorem	msubty 31550	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 31551*	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 31552	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 𝑆 = (𝑆 “ (𝑅 ↑𝑚 𝑉))
Theorem	msubff 31553	A substitution is a function from 𝐸 to 𝐸. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑𝑚 𝐸))
Theorem	msubco 31554	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	msubf 31555	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝐸⟶𝐸)
Theorem	mvhfval 31556*	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)
Theorem	mvhval 31557	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝐻‘𝑋) = ⟨(𝑌‘𝑋), ⟨“𝑋”⟩⟩)
Theorem	mpstval 31558*	A pre-statement is an ordered triple, whose first member is a symmetric set of dv 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 31559	Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸))
Theorem	msrfval 31560*	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 31561	Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 → (𝑅‘⟨𝐷, 𝐻, 𝐴⟩) = ⟨(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
Theorem	mpstssv 31562	A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑃 ⊆ ((V × V) × V)
Theorem	mpst123 31563	Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑃 → 𝑋 = ⟨(1st ‘(1st ‘𝑋)), (2nd ‘(1st ‘𝑋)), (2nd ‘𝑋)⟩)
Theorem	mpstrcl 31564	The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V))
Theorem	msrf 31565	The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    ⇒   ⊢ 𝑅:𝑃⟶𝑃
Theorem	msrrcl 31566	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 31567	Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ 𝑆 = ran 𝑅
Theorem	msrid 31568	The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑆 → (𝑅‘𝑋) = 𝑋)
Theorem	msrfo 31569	The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑅:𝑃–onto→𝑆
Theorem	mstapst 31570	A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ 𝑆 ⊆ 𝑃
Theorem	elmsta 31571	Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑆 ↔ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)))
Theorem	ismfs 31572*	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 31573	The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → (𝐶 ∩ 𝑉) = ∅)
Theorem	mtyf2 31574	The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐾 = (mTC‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐾)
Theorem	mtyf 31575	The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐹)
Theorem	mvtss 31576	The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝐾 = (mTC‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐹 ⊆ 𝐾)
Theorem	maxsta 31577	An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ 𝑆)
Theorem	mvtinf 31578	Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ ((𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹) → ¬ (◡𝑌 “ {𝑋}) ∈ Fin)
Theorem	msubff1 31579	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 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝐸 ↑𝑚 𝐸))
Theorem	msubff1o 31580	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 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1-onto→ran 𝑆)
Theorem	mvhf 31581	The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸)
Theorem	mvhf1 31582	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 31583*	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 31584	Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    ⇒   ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸))
Theorem	mclsssvlem 31585*	Lemma for mclsssv 31587. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    &   ⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    ⇒   ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸)
Theorem	mclsval 31586*	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 31587	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 31588	Lemma for ssmcls 31590. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵))
Theorem	vhmcls 31589	All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵))
Theorem	ssmcls 31590	The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵))
Theorem	ss2mcls 31591	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 31592*	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 31593*	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 31594*	Lemma for mppspst 31597. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝐽 = (mPPSt‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    ⇒   ⊢ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃
Theorem	mppsval 31595*	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 31596	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 31597	A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝐽 = (mPPSt‘𝑇)    ⇒   ⊢ 𝐽 ⊆ 𝑃
Theorem	mthmval 31598	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 31599*	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 31600	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‘𝑇)    ⇒   ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑅‘𝑋) = (𝑅‘𝑌)) → 𝑌 ∈ 𝑈)