![]() |
Metamath
Proof Explorer Theorem List (p. 321 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mvrsval 32001 | The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑊 = (mVars‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉)) | ||
Theorem | mvrsfpw 32002 | 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 32003* | 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 32004* | 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 32005* | 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 32006 | The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘〈“𝑋”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) | ||
Theorem | mrsubvr 32007 | The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘〈“𝑋”〉) = (𝐹‘𝑋)) | ||
Theorem | mrsubff 32008 | A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) | ||
Theorem | mrsubrn 32009 | 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 32010 | 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 32011 | 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 32012 | The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅) | ||
Theorem | mrsubf 32013 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) | ||
Theorem | mrsubccat 32014 | Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) | ||
Theorem | mrsubcn 32015 | A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐶 = (mCN‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑋”〉) = 〈“𝑋”〉) | ||
Theorem | elmrsubrn 32016* | 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 32045.) (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐶 = (mCN‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))) | ||
Theorem | mrsubco 32017 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) | ||
Theorem | mrsubvrs 32018* | 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 32019* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) | ||
Theorem | msubfval 32020* | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) | ||
Theorem | msubval 32021 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → ((𝑆‘𝐹)‘𝑋) = 〈(1st ‘𝑋), ((𝑂‘𝐹)‘(2nd ‘𝑋))〉) | ||
Theorem | msubrsub 32022 | A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑂 = (mRSubst‘𝑇) ⇒ ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (2nd ‘((𝑆‘𝐹)‘𝑋)) = ((𝑂‘𝐹)‘(2nd ‘𝑋))) | ||
Theorem | msubty 32023 | 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 32024* | 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 32025 | 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 32026 | A substitution is a function from 𝐸 to 𝐸. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑅 = (mREx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) ⇒ ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑𝑚 𝐸)) | ||
Theorem | msubco 32027 | The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mSubst‘𝑇) ⇒ ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) | ||
Theorem | msubf 32028 | A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) ⇒ ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝐸⟶𝐸) | ||
Theorem | mvhfval 32029* | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ 〈(𝑌‘𝑣), 〈“𝑣”〉〉) | ||
Theorem | mvhval 32030 | Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝐻‘𝑋) = 〈(𝑌‘𝑋), 〈“𝑋”〉〉) | ||
Theorem | mpstval 32031* | 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 32032 | Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸)) | ||
Theorem | msrfval 32033* | 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 32034 | Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVars‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴})) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝑅‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | ||
Theorem | mpstssv 32035 | A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ 𝑃 ⊆ ((V × V) × V) | ||
Theorem | mpst123 32036 | Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑃 → 𝑋 = 〈(1st ‘(1st ‘𝑋)), (2nd ‘(1st ‘𝑋)), (2nd ‘𝑋)〉) | ||
Theorem | mpstrcl 32037 | The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V)) | ||
Theorem | msrf 32038 | The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑅 = (mStRed‘𝑇) ⇒ ⊢ 𝑅:𝑃⟶𝑃 | ||
Theorem | msrrcl 32039 | 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 32040 | Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ 𝑆 = ran 𝑅 | ||
Theorem | msrid 32041 | The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑋 ∈ 𝑆 → (𝑅‘𝑋) = 𝑋) | ||
Theorem | msrfo 32042 | The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) & ⊢ 𝑃 = (mPreSt‘𝑇) ⇒ ⊢ 𝑅:𝑃–onto→𝑆 | ||
Theorem | mstapst 32043 | A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ 𝑆 ⊆ 𝑃 | ||
Theorem | elmsta 32044 | Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) & ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴})) ⇒ ⊢ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑆 ↔ (〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍))) | ||
Theorem | ismfs 32045* | 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 32046 | The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐶 = (mCN‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → (𝐶 ∩ 𝑉) = ∅) | ||
Theorem | mtyf2 32047 | The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐾) | ||
Theorem | mtyf 32048 | The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐹) | ||
Theorem | mvtss 32049 | The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝐾 = (mTC‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐹 ⊆ 𝐾) | ||
Theorem | maxsta 32050 | An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mStat‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ 𝑆) | ||
Theorem | mvtinf 32051 | Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐹 = (mVT‘𝑇) & ⊢ 𝑌 = (mType‘𝑇) ⇒ ⊢ ((𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹) → ¬ (◡𝑌 “ {𝑋}) ∈ Fin) | ||
Theorem | msubff1 32052 | 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 32053 | 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 32054 | The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑉 = (mVR‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) | ||
Theorem | mvhf1 32055 | 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 32056* | 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 32057 | Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸)) | ||
Theorem | mclsssvlem 32058* | Lemma for mclsssv 32060. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝐴 = (mAx‘𝑇) & ⊢ 𝑆 = (mSubst‘𝑇) & ⊢ 𝑉 = (mVars‘𝑇) ⇒ ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸) | ||
Theorem | mclsval 32059* | 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 32060 | 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 32061 | Lemma for ssmcls 32063. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) ⇒ ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵)) | ||
Theorem | vhmcls 32062 | All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) & ⊢ 𝐻 = (mVH‘𝑇) & ⊢ 𝑉 = (mVR‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵)) | ||
Theorem | ssmcls 32063 | The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐷 = (mDV‘𝑇) & ⊢ 𝐸 = (mEx‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ mFS) & ⊢ (𝜑 → 𝐾 ⊆ 𝐷) & ⊢ (𝜑 → 𝐵 ⊆ 𝐸) ⇒ ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵)) | ||
Theorem | ss2mcls 32064 | 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 32065* | 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 32066* | 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 32067* | Lemma for mppspst 32070. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝐶 = (mCls‘𝑇) ⇒ ⊢ {〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ 𝑃 ∧ 𝑎 ∈ (𝑑𝐶ℎ))} ⊆ 𝑃 | ||
Theorem | mppsval 32068* | 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 32069 | 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 32070 | A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑃 = (mPreSt‘𝑇) & ⊢ 𝐽 = (mPPSt‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑃 | ||
Theorem | mthmval 32071 | 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 32072* | 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 32073 | 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 32074 | A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑈 = (mThm‘𝑇) & ⊢ 𝑆 = (mPreSt‘𝑇) ⇒ ⊢ 𝑈 ⊆ 𝑆 | ||
Theorem | mppsthm 32075 | A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝐽 = (mPPSt‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ 𝐽 ⊆ 𝑈 | ||
Theorem | mthmblem 32076 | Lemma for mthmb 32077. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑅 = (mStRed‘𝑇) & ⊢ 𝑈 = (mThm‘𝑇) ⇒ ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈)) | ||
Theorem | mthmb 32077 | 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 32078 | 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 32079* | The closure is closed under application of provable pre-statements. (Compare mclsax 32065.) 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 32080* | The closure is closed under application of provable pre-statements. (Compare mclsax 32065.) 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 𝐿) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)) & ⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏) ⇒ ⊢ (𝜑 → (𝑆‘𝑃) ∈ (𝐾𝐶𝐵)) | ||
Syntax | cm0s 32081 | Mapping expressions to statements. |
class m0St | ||
Syntax | cmsa 32082 | The set of syntax axioms. |
class mSA | ||
Syntax | cmwgfs 32083 | The set of weakly grammatical formal systems. |
class mWGFS | ||
Syntax | cmsy 32084 | The syntax typecode function. |
class mSyn | ||
Syntax | cmesy 32085 | The syntax typecode function for expressions. |
class mESyn | ||
Syntax | cmgfs 32086 | The set of grammatical formal systems. |
class mGFS | ||
Syntax | cmtree 32087 | The set of proof trees. |
class mTree | ||
Syntax | cmst 32088 | The set of syntax trees. |
class mST | ||
Syntax | cmsax 32089 | The indexing set for a syntax axiom. |
class mSAX | ||
Syntax | cmufs 32090 | The set of unambiguous formal sytems. |
class mUFS | ||
Definition | df-m0s 32091 | Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ m0St = (𝑎 ∈ V ↦ 〈∅, ∅, 𝑎〉) | ||
Definition | df-msa 32092* | 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 32093* | 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 32094 | Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mSyn = Slot 6 | ||
Definition | df-mtree 32095* | 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 32096 | Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) | ||
Definition | df-msax 32097* | 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‘𝑡)‘𝑝)))) | ||
Definition | df-mufs 32098 | Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)} | ||
Syntax | cmuv 32099 | The universe of a model. |
class mUV | ||
Syntax | cmvl 32100 | The set of valuations. |
class mVL |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |