![]() |
Metamath
Proof Explorer Theorem List (p. 355 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sate0fv0 35401 | 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 35402* | 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 35403 | 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 35404 | 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 35405* | 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 35406* | Instance of sategoelfv 35404 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 35407* | 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 35408 | 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 35409* | 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 35410* | 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 35411 | 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 35412 | 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 35413 | The wff (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) encoded as ((𝐴∈𝑔𝐵) ⊼𝑔(𝐵∈𝑔𝐴)) is true in any model 𝑀. This is the model theoretic proof of elnanel 9644. (Contributed by AV, 5-Nov-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝑀⊧((𝐴∈𝑔𝐵)⊼𝑔(𝐵∈𝑔𝐴))) | ||
Theorem | prv0 35414 | 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 35415 | No wff encoded as a Godel-set of membership is true in a model with only one element. (Contributed by AV, 19-Nov-2023.) |
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ {𝑋}⊧(𝐼∈𝑔𝐽)) | ||
Syntax | cgon 35416 | The Godel-set of negation. (Note that this is not a wff.) |
class ¬𝑔𝑈 | ||
Syntax | cgoa 35417 | The Godel-set of conjunction. |
class ∧𝑔 | ||
Syntax | cgoi 35418 | The Godel-set of implication. |
class →𝑔 | ||
Syntax | cgoo 35419 | The Godel-set of disjunction. |
class ∨𝑔 | ||
Syntax | cgob 35420 | The Godel-set of equivalence. |
class ↔𝑔 | ||
Syntax | cgoq 35421 | The Godel-set of equality. |
class =𝑔 | ||
Syntax | cgox 35422 | The Godel-set of existential quantification. (Note that this is not a wff.) |
class ∃𝑔𝑁𝑈 | ||
Definition | df-gonot 35423 | 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 35424* | 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 35425* | 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 35426* | 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 35427* | 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 35428* | 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 2705 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 35429 | 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.) |
⊢ ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈 | ||
Syntax | cgze 35430 | The Axiom of Extensionality. |
class AxExt | ||
Syntax | cgzr 35431 | The Axiom Scheme of Replacement. |
class AxRep | ||
Syntax | cgzp 35432 | The Axiom of Power Sets. |
class AxPow | ||
Syntax | cgzu 35433 | The Axiom of Unions. |
class AxUn | ||
Syntax | cgzg 35434 | The Axiom of Regularity. |
class AxReg | ||
Syntax | cgzi 35435 | The Axiom of Infinity. |
class AxInf | ||
Syntax | cgzf 35436 | The set of models of ZF. |
class ZF | ||
Definition | df-gzext 35437 | 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 35438 | 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 35439 | 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 35440 | 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 35441 | 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 35442 | 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 35443* | 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‘𝑢))} | ||
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 35444 | The set of constants. |
class mCN | ||
Syntax | cmvar 35445 | The set of variables. |
class mVR | ||
Syntax | cmty 35446 | The type function. |
class mType | ||
Syntax | cmvt 35447 | The set of variable typecodes. |
class mVT | ||
Syntax | cmtc 35448 | The set of typecodes. |
class mTC | ||
Syntax | cmax 35449 | The set of axioms. |
class mAx | ||
Syntax | cmrex 35450 | The set of raw expressions. |
class mREx | ||
Syntax | cmex 35451 | The set of expressions. |
class mEx | ||
Syntax | cmdv 35452 | The set of distinct variables. |
class mDV | ||
Syntax | cmvrs 35453 | The variables in an expression. |
class mVars | ||
Syntax | cmrsub 35454 | The set of raw substitutions. |
class mRSubst | ||
Syntax | cmsub 35455 | The set of substitutions. |
class mSubst | ||
Syntax | cmvh 35456 | The set of variable hypotheses. |
class mVH | ||
Syntax | cmpst 35457 | The set of pre-statements. |
class mPreSt | ||
Syntax | cmsr 35458 | The reduct of a pre-statement. |
class mStRed | ||
Syntax | cmsta 35459 | The set of statements. |
class mStat | ||
Syntax | cmfs 35460 | The set of formal systems. |
class mFS | ||
Syntax | cmcls 35461 | The closure of a set of statements. |
class mCls | ||
Syntax | cmpps 35462 | The set of provable pre-statements. |
class mPPSt | ||
Syntax | cmthm 35463 | The set of theorems. |
class mThm | ||
Definition | df-mcn 35464 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mCN = Slot 1 | ||
Definition | df-mvar 35465 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVR = Slot 2 | ||
Definition | df-mty 35466 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mType = Slot 3 | ||
Definition | df-mtc 35467 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mTC = Slot 4 | ||
Definition | df-mmax 35468 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mAx = Slot 5 | ||
Definition | df-mvt 35469 | 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 35470 | 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 35471 | 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 35472 | 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 35473* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡)))) | ||
Definition | df-mrsub 35474* | 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 35475* | 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 35476* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ 〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉)) | ||
Definition | df-mpst 35477* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))) | ||
Definition | df-msr 35478* | 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 35479 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡)) | ||
Definition | df-mfs 35480* | 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 35481* | 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 35482* | Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mPPSt = (𝑡 ∈ V ↦ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) | ||
Definition | df-mthm 35483 | Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡)))) | ||
Theorem | mvtval 35484 | The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ 𝑉 = ran 𝑌 | ||
Theorem | mrexval 35485 | 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 35486 | 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 35487 | 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 35488 | 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 35489 | The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑊 = (mVars‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉)) | ||
Theorem | mvrsfpw 35490 | 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 35491* | 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 35492* | 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 35493* | 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 35494 | The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘〈“𝑋”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) | ||
Theorem | mrsubvr 35495 | The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘〈“𝑋”〉) = (𝐹‘𝑋)) | ||
Theorem | mrsubff 35496 | A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) | ||
Theorem | mrsubrn 35497 | 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 35498 | 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 35499 | 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 35500 | The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |