P. 336 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33501-33600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mdvval 33501	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 33502	The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑊 = (mVars‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉))
Theorem	mvrsfpw 33503	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 33504*	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 33505*	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 33506*	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 33507	The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), ⟨“𝑋”⟩))
Theorem	mrsubvr 33508	The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = (𝐹‘𝑋))
Theorem	mrsubff 33509	A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅))
Theorem	mrsubrn 33510	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 33511	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 33512	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 33513	The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
Theorem	mrsubf 33514	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
Theorem	mrsubccat 33515	Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))
Theorem	mrsubcn 33516	A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑋”⟩) = ⟨“𝑋”⟩)
Theorem	elmrsubrn 33517*	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 33546.) (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))))
Theorem	mrsubco 33518	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	mrsubvrs 33519*	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 33520*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))⟩)))
Theorem	msubfval 33521*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))⟩))
Theorem	msubval 33522	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → ((𝑆‘𝐹)‘𝑋) = ⟨(1st ‘𝑋), ((𝑂‘𝐹)‘(2nd ‘𝑋))⟩)
Theorem	msubrsub 33523	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (2nd ‘((𝑆‘𝐹)‘𝑋)) = ((𝑂‘𝐹)‘(2nd ‘𝑋)))
Theorem	msubty 33524	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 33525*	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 33526	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 33527	A substitution is a function from 𝐸 to 𝐸. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑m 𝐸))
Theorem	msubco 33528	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	msubf 33529	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝐸⟶𝐸)
Theorem	mvhfval 33530*	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)
Theorem	mvhval 33531	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝐻‘𝑋) = ⟨(𝑌‘𝑋), ⟨“𝑋”⟩⟩)
Theorem	mpstval 33532*	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 33533	Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸))
Theorem	msrfval 33534*	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 33535	Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 → (𝑅‘⟨𝐷, 𝐻, 𝐴⟩) = ⟨(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
Theorem	mpstssv 33536	A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑃 ⊆ ((V × V) × V)
Theorem	mpst123 33537	Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑃 → 𝑋 = ⟨(1st ‘(1st ‘𝑋)), (2nd ‘(1st ‘𝑋)), (2nd ‘𝑋)⟩)
Theorem	mpstrcl 33538	The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V))
Theorem	msrf 33539	The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    ⇒   ⊢ 𝑅:𝑃⟶𝑃
Theorem	msrrcl 33540	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 33541	Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ 𝑆 = ran 𝑅
Theorem	msrid 33542	The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑆 → (𝑅‘𝑋) = 𝑋)
Theorem	msrfo 33543	The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑅:𝑃–onto→𝑆
Theorem	mstapst 33544	A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ 𝑆 ⊆ 𝑃
Theorem	elmsta 33545	Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑆 ↔ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)))
Theorem	ismfs 33546*	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 33547	The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → (𝐶 ∩ 𝑉) = ∅)
Theorem	mtyf2 33548	The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐾 = (mTC‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐾)
Theorem	mtyf 33549	The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐹)
Theorem	mvtss 33550	The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝐾 = (mTC‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐹 ⊆ 𝐾)
Theorem	maxsta 33551	An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ 𝑆)
Theorem	mvtinf 33552	Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ ((𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹) → ¬ (◡𝑌 “ {𝑋}) ∈ Fin)
Theorem	msubff1 33553	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 33554	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 33555	The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸)
Theorem	mvhf1 33556	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 33557*	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 33558	Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    ⇒   ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸))
Theorem	mclsssvlem 33559*	Lemma for mclsssv 33561. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    &   ⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    ⇒   ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸)
Theorem	mclsval 33560*	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 33561	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 33562	Lemma for ssmcls 33564. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵))
Theorem	vhmcls 33563	All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵))
Theorem	ssmcls 33564	The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵))
Theorem	ss2mcls 33565	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 33566*	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 33567*	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 33568*	Lemma for mppspst 33571. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝐽 = (mPPSt‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    ⇒   ⊢ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃
Theorem	mppsval 33569*	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 33570	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 33571	A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝐽 = (mPPSt‘𝑇)    ⇒   ⊢ 𝐽 ⊆ 𝑃
Theorem	mthmval 33572	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 33573*	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 33574	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 33575	A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑈 = (mThm‘𝑇)    &   ⊢ 𝑆 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑈 ⊆ 𝑆
Theorem	mppsthm 33576	A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐽 = (mPPSt‘𝑇)    &   ⊢ 𝑈 = (mThm‘𝑇)    ⇒   ⊢ 𝐽 ⊆ 𝑈
Theorem	mthmblem 33577	Lemma for mthmb 33578. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑈 = (mThm‘𝑇)    ⇒   ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈))
Theorem	mthmb 33578	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 33579	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 33580*	The closure is closed under application of provable pre-statements. (Compare mclsax 33566.) 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 33581*	The closure is closed under application of provable pre-statements. (Compare mclsax 33566.) 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 𝐿)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵))    &   ⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏)    ⇒   ⊢ (𝜑 → (𝑆‘𝑃) ∈ (𝐾𝐶𝐵))
20.6.14  Grammatical formal systems
Syntax	cm0s 33582	Mapping expressions to statements.
class m0St
Syntax	cmsa 33583	The set of syntax axioms.
class mSA
Syntax	cmwgfs 33584	The set of weakly grammatical formal systems.
class mWGFS
Syntax	cmsy 33585	The syntax typecode function.
class mSyn
Syntax	cmesy 33586	The syntax typecode function for expressions.
class mESyn
Syntax	cmgfs 33587	The set of grammatical formal systems.
class mGFS
Syntax	cmtree 33588	The set of proof trees.
class mTree
Syntax	cmst 33589	The set of syntax trees.
class mST
Syntax	cmsax 33590	The indexing set for a syntax axiom.
class mSAX
Syntax	cmufs 33591	The set of unambiguous formal sytems.
class mUFS
Definition	df-m0s 33592	Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ m0St = (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)
Definition	df-msa 33593*	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 33594*	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 33595	Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mSyn = Slot 6
Definition	df-mesyn 33596*	Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.)
⊢ mESyn = (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒)))
Definition	df-mgfs 33597*	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 33598*	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 33599	Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡))))
Definition	df-msax 33600*	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‘𝑡)‘𝑝))))