P. 348 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34701-34800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	satfun 34701	The satisfaction predicate as function over wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀. (Contributed by AV, 29-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘ω):(Fmla‘ω)⟶𝒫 (𝑀 ↑m ω))
Theorem	satfvel 34702	An element of the value of the satisfaction predicate as function over wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀 at the code 𝑈 for a wff using ∈ , ⊼ , ∀ is a valuation 𝑆:ω⟶𝑀 of the variables (v0 = (𝑆‘∅), v1 = (𝑆‘1o), etc.) so that 𝑈 is true under the assignment 𝑆. (Contributed by AV, 29-Oct-2023.)
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (((𝑀 Sat 𝐸)‘ω)‘𝑈)) → 𝑆:ω⟶𝑀)
Theorem	satfv0fvfmla0 34703*	The value of the satisfaction predicate as function over a wff code at ∅. (Contributed by AV, 2-Nov-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑆‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st ‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd ‘𝑋)))})
Theorem	satefv 34704	The simplified satisfaction predicate as function over wff codes in the model 𝑀 at the code 𝑈. (Contributed by AV, 30-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊) → (𝑀 Sat∈ 𝑈) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑈))
Theorem	sate0 34705	The simplified satisfaction predicate for any wff code over an empty model. (Contributed by AV, 6-Oct-2023.) (Revised by AV, 5-Nov-2023.)
⊢ (𝑈 ∈ 𝑉 → (∅ Sat∈ 𝑈) = (((∅ Sat ∅)‘ω)‘𝑈))
Theorem	satef 34706	The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (𝑀 Sat∈ 𝑈)) → 𝑆:ω⟶𝑀)
Theorem	sate0fv0 34707	A simplified satisfaction predicate as function over wff codes over an empty model is an empty set. (Contributed by AV, 31-Oct-2023.)
⊢ (𝑈 ∈ (Fmla‘ω) → (𝑆 ∈ (∅ Sat∈ 𝑈) → 𝑆 = ∅))
Theorem	satefvfmla0 34708*	The simplified satisfaction predicate for wff codes of height 0. (Contributed by AV, 4-Nov-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → (𝑀 Sat∈ 𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st ‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd ‘𝑋)))})
Theorem	sategoelfvb 34709	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 34710	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 34711*	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 34712*	Instance of sategoelfv 34710 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 34713*	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 34714	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 34715*	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 34716*	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 34717	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 34718	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 34719	The wff (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) encoded as ((𝐴∈𝑔𝐵) ⊼𝑔(𝐵∈𝑔𝐴)) is true in any model 𝑀. This is the model theoretic proof of elnanel 9606. (Contributed by AV, 5-Nov-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝑀⊧((𝐴∈𝑔𝐵)⊼𝑔(𝐵∈𝑔𝐴)))
Theorem	prv0 34720	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 34721	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 34722	The Godel-set of negation. (Note that this is not a wff.)
class ¬𝑔𝑈
Syntax	cgoa 34723	The Godel-set of conjunction.
class ∧𝑔
Syntax	cgoi 34724	The Godel-set of implication.
class →𝑔
Syntax	cgoo 34725	The Godel-set of disjunction.
class ∨𝑔
Syntax	cgob 34726	The Godel-set of equivalence.
class ↔𝑔
Syntax	cgoq 34727	The Godel-set of equality.
class =𝑔
Syntax	cgox 34728	The Godel-set of existential quantification. (Note that this is not a wff.)
class ∃𝑔𝑁𝑈
Definition	df-gonot 34729	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 34730*	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 34731*	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 34732*	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 34733*	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 34734*	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 2702 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 34735	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 34736	The Axiom of Extensionality.
class AxExt
Syntax	cgzr 34737	The Axiom Scheme of Replacement.
class AxRep
Syntax	cgzp 34738	The Axiom of Power Sets.
class AxPow
Syntax	cgzu 34739	The Axiom of Unions.
class AxUn
Syntax	cgzg 34740	The Axiom of Regularity.
class AxReg
Syntax	cgzi 34741	The Axiom of Infinity.
class AxInf
Syntax	cgzf 34742	The set of models of ZF.
class ZF
Definition	df-gzext 34743	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 34744	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 34745	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 34746	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 34747	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 34748	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 34749*	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 34750	The set of constants.
class mCN
Syntax	cmvar 34751	The set of variables.
class mVR
Syntax	cmty 34752	The type function.
class mType
Syntax	cmvt 34753	The set of variable typecodes.
class mVT
Syntax	cmtc 34754	The set of typecodes.
class mTC
Syntax	cmax 34755	The set of axioms.
class mAx
Syntax	cmrex 34756	The set of raw expressions.
class mREx
Syntax	cmex 34757	The set of expressions.
class mEx
Syntax	cmdv 34758	The set of distinct variables.
class mDV
Syntax	cmvrs 34759	The variables in an expression.
class mVars
Syntax	cmrsub 34760	The set of raw substitutions.
class mRSubst
Syntax	cmsub 34761	The set of substitutions.
class mSubst
Syntax	cmvh 34762	The set of variable hypotheses.
class mVH
Syntax	cmpst 34763	The set of pre-statements.
class mPreSt
Syntax	cmsr 34764	The reduct of a pre-statement.
class mStRed
Syntax	cmsta 34765	The set of statements.
class mStat
Syntax	cmfs 34766	The set of formal systems.
class mFS
Syntax	cmcls 34767	The closure of a set of statements.
class mCls
Syntax	cmpps 34768	The set of provable pre-statements.
class mPPSt
Syntax	cmthm 34769	The set of theorems.
class mThm
Definition	df-mcn 34770	Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mCN = Slot 1
Definition	df-mvar 34771	Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVR = Slot 2
Definition	df-mty 34772	Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mType = Slot 3
Definition	df-mtc 34773	Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mTC = Slot 4
Definition	df-mmax 34774	Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mAx = Slot 5
Definition	df-mvt 34775	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 34776	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 34777	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 34778	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 34779*	Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))
Definition	df-mrsub 34780*	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 34781*	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 34782*	Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
Definition	df-mpst 34783*	Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Definition	df-msr 34784*	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 34785	Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡))
Definition	df-mfs 34786*	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 34787*	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 34788*	Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPPSt = (𝑡 ∈ V ↦ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))})
Definition	df-mthm 34789	Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡))))
Theorem	mvtval 34790	The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ 𝑉 = ran 𝑌
Theorem	mrexval 34791	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 34792	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 34793	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 34794	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 34795	The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑊 = (mVars‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉))
Theorem	mvrsfpw 34796	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 34797*	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 34798*	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 34799*	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 34800	The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), ⟨“𝑋”⟩))