P. 357 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35601-35700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sategoelfvb 35601	Characterization of a valuation 𝑆 of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.)
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵))    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝑆 ∈ 𝐸 ↔ (𝑆 ∈ (𝑀 ↑m ω) ∧ (𝑆‘𝐴) ∈ (𝑆‘𝐵))))
Theorem	sategoelfv 35602	Condition of a valuation 𝑆 of a simplified satisfaction predicate for a Godel-set of membership: The sets in model 𝑀 corresponding to the variables 𝐴 and 𝐵 under the assignment of 𝑆 are in a membership relation in 𝑀. (Contributed by AV, 5-Nov-2023.)
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵))    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑆 ∈ 𝐸) → (𝑆‘𝐴) ∈ (𝑆‘𝐵))
Theorem	ex-sategoelel 35603*	Example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.)
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵))    &   ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 𝐴, 𝑍, if(𝑥 = 𝐵, 𝒫 𝑍, ∅)))    ⇒   ⊢ (((𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵)) → 𝑆 ∈ 𝐸)
Theorem	ex-sategoel 35604*	Instance of sategoelfv 35602 for the example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.)
⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵))    &   ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 𝐴, 𝑍, if(𝑥 = 𝐵, 𝒫 𝑍, ∅)))    ⇒   ⊢ (((𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵)) → (𝑆‘𝐴) ∈ (𝑆‘𝐵))
Theorem	satfv1fvfmla1 35605*	The value of the satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.)
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿))    ⇒   ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat 𝐸)‘1o)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))})
Theorem	2goelgoanfmla1 35606	Two Godel-sets of membership combined with a Godel-set for NAND is a Godel formula of height 1. (Contributed by AV, 17-Nov-2023.)
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿))    ⇒   ⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ (Fmla‘1o))
Theorem	satefvfmla1 35607*	The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.)
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿))    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀 Sat∈ 𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾) ∈ (𝑎‘𝐿))})
Theorem	ex-sategoelelomsuc 35608*	Example of a valuation of a simplified satisfaction predicate over the ordinal numbers as model for a Godel-set of membership using the properties of a successor: (𝑆‘2o) = 𝑍 ∈ suc 𝑍 = (𝑆‘2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2o∈𝑔1o) should not be confused with 2o ∈ 1o, which is false. (Contributed by AV, 19-Nov-2023.)
⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 2o, 𝑍, suc 𝑍))    ⇒   ⊢ (𝑍 ∈ ω → 𝑆 ∈ (ω Sat∈ (2o∈𝑔1o)))
Theorem	ex-sategoelel12 35609	Example of a valuation of a simplified satisfaction predicate over a proper pair (of ordinal numbers) as model for a Godel-set of membership using the properties of a successor: (𝑆‘2o) = 1o ∈ 2o = (𝑆‘2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2o∈𝑔1o) should not be confused with 2o ∈ 1o, which is false. (Contributed by AV, 19-Nov-2023.)
⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 2o, 1o, 2o))    ⇒   ⊢ 𝑆 ∈ ({1o, 2o} Sat∈ (2o∈𝑔1o))
Theorem	prv 35610	The "proves" relation on a set. A wff encoded as 𝑈 is true in a model 𝑀 iff for every valuation 𝑠 ∈ (𝑀 ↑m ω), the interpretation of the wff using the membership relation on 𝑀 is true. (Contributed by AV, 5-Nov-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊) → (𝑀⊧𝑈 ↔ (𝑀 Sat∈ 𝑈) = (𝑀 ↑m ω)))
Theorem	elnanelprv 35611	The wff (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) encoded as ((𝐴∈𝑔𝐵) ⊼𝑔(𝐵∈𝑔𝐴)) is true in any model 𝑀. This is the model theoretic proof of elnanel 9528. (Contributed by AV, 5-Nov-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝑀⊧((𝐴∈𝑔𝐵)⊼𝑔(𝐵∈𝑔𝐴)))
Theorem	prv0 35612	Every wff encoded as 𝑈 is true in an "empty model" (𝑀 = ∅). Since ⊧ is defined in terms of the interpretations making the given formula true, it is not defined on the "empty model", since there are no interpretations. In particular, the empty set on the LHS of ⊧ should not be interpreted as the empty model, because ∃𝑥𝑥 = 𝑥 is not satisfied on the empty model. (Contributed by AV, 19-Nov-2023.)
⊢ (𝑈 ∈ (Fmla‘ω) → ∅⊧𝑈)
Theorem	prv1n 35613	No wff encoded as a Godel-set of membership is true in a model with only one element. (Contributed by AV, 19-Nov-2023.)
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ {𝑋}⊧(𝐼∈𝑔𝐽))
21.6.11  Godel-sets of formulas - part 2
Syntax	cgon 35614	The Godel-set of negation. (Note that this is not a wff.)
class ¬𝑔𝑈
Syntax	cgoa 35615	The Godel-set of conjunction.
class ∧𝑔
Syntax	cgoi 35616	The Godel-set of implication.
class →𝑔
Syntax	cgoo 35617	The Godel-set of disjunction.
class ∨𝑔
Syntax	cgob 35618	The Godel-set of equivalence.
class ↔𝑔
Syntax	cgoq 35619	The Godel-set of equality.
class =𝑔
Syntax	cgox 35620	The Godel-set of existential quantification. (Note that this is not a wff.)
class ∃𝑔𝑁𝑈
Definition	df-gonot 35621	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 35622*	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 35623*	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 35624*	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 35625*	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 35626*	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 2708 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 35627	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.)
⊢ ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈
21.6.12  Models of ZF
Syntax	cgze 35628	The Axiom of Extensionality.
class AxExt
Syntax	cgzr 35629	The Axiom Scheme of Replacement.
class AxRep
Syntax	cgzp 35630	The Axiom of Power Sets.
class AxPow
Syntax	cgzu 35631	The Axiom of Unions.
class AxUn
Syntax	cgzg 35632	The Axiom of Regularity.
class AxReg
Syntax	cgzi 35633	The Axiom of Infinity.
class AxInf
Syntax	cgzf 35634	The set of models of ZF.
class ZF
Definition	df-gzext 35635	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 35636	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 35637	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 35638	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 35639	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 35640	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 35641*	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‘𝑢))}
21.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 35642	The set of constants.
class mCN
Syntax	cmvar 35643	The set of variables.
class mVR
Syntax	cmty 35644	The type function.
class mType
Syntax	cmvt 35645	The set of variable typecodes.
class mVT
Syntax	cmtc 35646	The set of typecodes.
class mTC
Syntax	cmax 35647	The set of axioms.
class mAx
Syntax	cmrex 35648	The set of raw expressions.
class mREx
Syntax	cmex 35649	The set of expressions.
class mEx
Syntax	cmdv 35650	The set of distinct variables.
class mDV
Syntax	cmvrs 35651	The variables in an expression.
class mVars
Syntax	cmrsub 35652	The set of raw substitutions.
class mRSubst
Syntax	cmsub 35653	The set of substitutions.
class mSubst
Syntax	cmvh 35654	The set of variable hypotheses.
class mVH
Syntax	cmpst 35655	The set of pre-statements.
class mPreSt
Syntax	cmsr 35656	The reduct of a pre-statement.
class mStRed
Syntax	cmsta 35657	The set of statements.
class mStat
Syntax	cmfs 35658	The set of formal systems.
class mFS
Syntax	cmcls 35659	The closure of a set of statements.
class mCls
Syntax	cmpps 35660	The set of provable pre-statements.
class mPPSt
Syntax	cmthm 35661	The set of theorems.
class mThm
Definition	df-mcn 35662	Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mCN = Slot 1
Definition	df-mvar 35663	Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVR = Slot 2
Definition	df-mty 35664	Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mType = Slot 3
Definition	df-mtc 35665	Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mTC = Slot 4
Definition	df-mmax 35666	Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mAx = Slot 5
Definition	df-mvt 35667	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 35668	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 35669	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 35670	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 35671*	Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))
Definition	df-mrsub 35672*	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 35673*	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 35674*	Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
Definition	df-mpst 35675*	Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Definition	df-msr 35676*	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 35677	Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡))
Definition	df-mfs 35678*	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 35679*	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 35680*	Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPPSt = (𝑡 ∈ V ↦ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))})
Definition	df-mthm 35681	Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡))))
Theorem	mvtval 35682	The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ 𝑉 = ran 𝑌
Theorem	mrexval 35683	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 35684	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 35685	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 35686	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 35687	The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑊 = (mVars‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉))
Theorem	mvrsfpw 35688	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 35689*	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 35690*	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 35691*	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 35692	The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), ⟨“𝑋”⟩))
Theorem	mrsubvr 35693	The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = (𝐹‘𝑋))
Theorem	mrsubff 35694	A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅))
Theorem	mrsubrn 35695	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 35696	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 35697	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 35698	The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
Theorem	mrsubf 35699	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
Theorem	mrsubccat 35700	Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))