P. 315 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31401-31500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mdvval 31401	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 dv conditions of interest will be symmetric, so it does not matter.) (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- D = (mDV ` T )   =>    |- D = ( ( V X. V ) \ _I )
Theorem	mvrsval 31402	The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- E = (mEx ` T )   &    |- W = (mVars ` T )   =>    |- ( X e. E -> ( W ` X ) = ( ran ( 2nd ` X ) i^i V ) )
Theorem	mvrsfpw 31403	The set of variables in an expression is a finite subset of V. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- E = (mEx ` T )   &    |- W = (mVars ` T )   =>    |- ( X e. E -> ( W ` X ) e. ( ~P V i^i Fin ) )
Theorem	mrsubffval 31404*	The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- C = (mCN ` T )   &    |- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   &    |- G = (freeMnd ` ( C u. V ) )   =>    |- ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. R |-> ( G gsumg ( ( v e. ( C u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
Theorem	mrsubfval 31405*	The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- C = (mCN ` T )   &    |- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   &    |- G = (freeMnd ` ( C u. V ) )   =>    |- ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. R |-> ( G gsumg ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. e ) ) ) )
Theorem	mrsubval 31406*	The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- C = (mCN ` T )   &    |- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   &    |- G = (freeMnd ` ( C u. V ) )   =>    |- ( ( F : A --> R /\ A C_ V /\ X e. R ) -> ( ( S ` F ) ` X ) = ( G gsumg ( ( v e. ( C u. V ) |-> if ( v e. A , ( F ` v ) , <" v "> ) ) o. X ) ) )
Theorem	mrsubcv 31407	The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- C = (mCN ` T )   &    |- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   =>    |- ( ( F : A --> R /\ A C_ V /\ X e. ( C u. V ) ) -> ( ( S ` F ) ` <" X "> ) = if ( X e. A , ( F ` X ) , <" X "> ) )
Theorem	mrsubvr 31408	The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   =>    |- ( ( F : A --> R /\ A C_ V /\ X e. A ) -> ( ( S ` F ) ` <" X "> ) = ( F ` X ) )
Theorem	mrsubff 31409	A substitution is a function from R to R. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   =>    |- ( T e. W -> S : ( R ^pm V ) --> ( R ^m R ) )
Theorem	mrsubrn 31410	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.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   =>    |- ran S = ( S " ( R ^m V ) )
Theorem	mrsubff1 31411	When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   =>    |- ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) )
Theorem	mrsubff1o 31412	When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mRSubst ` T )   =>    |- ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S )
Theorem	mrsub0 31413	The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mRSubst ` T )   =>    |- ( F e. ran S -> ( F ` (/) ) = (/) )
Theorem	mrsubf 31414	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mRSubst ` T )   &    |- R = (mREx ` T )   =>    |- ( F e. ran S -> F : R --> R )
Theorem	mrsubccat 31415	Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mRSubst ` T )   &    |- R = (mREx ` T )   =>    |- ( ( F e. ran S /\ X e. R /\ Y e. R ) -> ( F ` ( X ++ Y ) ) = ( ( F ` X ) ++ ( F ` Y ) ) )
Theorem	mrsubcn 31416	A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mRSubst ` T )   &    |- R = (mREx ` T )   &    |- V = (mVR ` T )   &    |- C = (mCN ` T )   =>    |- ( ( F e. ran S /\ X e. ( C \ V ) ) -> ( F ` <" X "> ) = <" X "> )
Theorem	elmrsubrn 31417*	Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses ( C \ V ) because we don't know that C and V are disjoint until we get to ismfs 31446.) (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mRSubst ` T )   &    |- R = (mREx ` T )   &    |- V = (mVR ` T )   &    |- C = (mCN ` T )   =>    |- ( T e. W -> ( F e. ran S <-> ( F : R --> R /\ A. c e. ( C \ V ) ( F ` <" c "> ) = <" c "> /\ A. x e. R A. y e. R ( F ` ( x ++ y ) ) = ( ( F ` x ) ++ ( F ` y ) ) ) ) )
Theorem	mrsubco 31418	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mRSubst ` T )   =>    |- ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )
Theorem	mrsubvrs 31419*	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.)
|- S = (mRSubst ` T )   &    |- V = (mVR ` T )   &    |- R = (mREx ` T )   =>    |- ( ( F e. ran S /\ X e. R ) -> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) )
Theorem	msubffval 31420*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   &    |- O = (mRSubst ` T )   =>    |- ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )
Theorem	msubfval 31421*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   &    |- O = (mRSubst ` T )   =>    |- ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )
Theorem	msubval 31422	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   &    |- O = (mRSubst ` T )   =>    |- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( ( S ` F ) ` X ) = <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` X ) ) >. )
Theorem	msubrsub 31423	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   &    |- O = (mRSubst ` T )   =>    |- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( 2nd ` ( ( S ` F ) ` X ) ) = ( ( O ` F ) ` ( 2nd ` X ) ) )
Theorem	msubty 31424	The type of a substituted expression is the same as the original type. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   =>    |- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( 1st ` ( ( S ` F ) ` X ) ) = ( 1st ` X ) )
Theorem	elmsubrn 31425*	Characterization of substitution in terms of raw substitution, without reference to the generating functions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- E = (mEx ` T )   &    |- O = (mRSubst ` T )   &    |- S = (mSubst ` T )   =>    |- ran S = ran ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
Theorem	msubrn 31426	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.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   =>    |- ran S = ( S " ( R ^m V ) )
Theorem	msubff 31427	A substitution is a function from E to E. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   =>    |- ( T e. W -> S : ( R ^pm V ) --> ( E ^m E ) )
Theorem	msubco 31428	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mSubst ` T )   =>    |- ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )
Theorem	msubf 31429	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- S = (mSubst ` T )   &    |- E = (mEx ` T )   =>    |- ( F e. ran S -> F : E --> E )
Theorem	mvhfval 31430*	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- Y = (mType ` T )   &    |- H = (mVH ` T )   =>    |- H = ( v e. V |-> <. ( Y ` v ) , <" v "> >. )
Theorem	mvhval 31431	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- Y = (mType ` T )   &    |- H = (mVH ` T )   =>    |- ( X e. V -> ( H ` X ) = <. ( Y ` X ) , <" X "> >. )
Theorem	mpstval 31432*	A pre-statement is an ordered triple, whose first member is a symmetric set of dv conditions, whose second member is a finite set of expressions, and whose third member is an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mDV ` T )   &    |- E = (mEx ` T )   &    |- P = (mPreSt ` T )   =>    |- P = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E )
Theorem	elmpst 31433	Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mDV ` T )   &    |- E = (mEx ` T )   &    |- P = (mPreSt ` T )   =>    |- ( <. D , H , A >. e. P <-> ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) /\ A e. E ) )
Theorem	msrfval 31434*	Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVars ` T )   &    |- P = (mPreSt ` T )   &    |- R = (mStRed ` T )   =>    |- R = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
Theorem	msrval 31435	Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVars ` T )   &    |- P = (mPreSt ` T )   &    |- R = (mStRed ` T )   &    |- Z = U. ( V " ( H u. { A } ) )   =>    |- ( <. D , H , A >. e. P -> ( R ` <. D , H , A >. ) = <. ( D i^i ( Z X. Z ) ) , H , A >. )
Theorem	mpstssv 31436	A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   =>    |- P C_ ( ( _V X. _V ) X. _V )
Theorem	mpst123 31437	Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   =>    |- ( X e. P -> X = <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) , ( 2nd ` X ) >. )
Theorem	mpstrcl 31438	The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   =>    |- ( <. D , H , A >. e. P -> ( D e. _V /\ H e. _V /\ A e. _V ) )
Theorem	msrf 31439	The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- R = (mStRed ` T )   =>    |- R : P --> P
Theorem	msrrcl 31440	If X and Y have the same reduct, then one is a pre-statement iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- R = (mStRed ` T )   =>    |- ( ( R ` X ) = ( R ` Y ) -> ( X e. P <-> Y e. P ) )
Theorem	mstaval 31441	Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- S = (mStat ` T )   =>    |- S = ran R
Theorem	msrid 31442	The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- S = (mStat ` T )   =>    |- ( X e. S -> ( R ` X ) = X )
Theorem	msrfo 31443	The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- S = (mStat ` T )   &    |- P = (mPreSt ` T )   =>    |- R : P -onto-> S
Theorem	mstapst 31444	A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- S = (mStat ` T )   =>    |- S C_ P
Theorem	elmsta 31445	Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- S = (mStat ` T )   &    |- V = (mVars ` T )   &    |- Z = U. ( V " ( H u. { A } ) )   =>    |- ( <. D , H , A >. e. S <-> ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) )
Theorem	ismfs 31446*	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.)
|- C = (mCN ` T )   &    |- V = (mVR ` T )   &    |- Y = (mType ` T )   &    |- F = (mVT ` T )   &    |- K = (mTC ` T )   &    |- A = (mAx ` T )   &    |- S = (mStat ` T )   =>    |- ( T e. W -> ( T e. mFS <-> ( ( ( C i^i V ) = (/) /\ Y : V --> K ) /\ ( A C_ S /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) ) )
Theorem	mfsdisj 31447	The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- C = (mCN ` T )   &    |- V = (mVR ` T )   =>    |- ( T e. mFS -> ( C i^i V ) = (/) )
Theorem	mtyf2 31448	The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- K = (mTC ` T )   &    |- Y = (mType ` T )   =>    |- ( T e. mFS -> Y : V --> K )
Theorem	mtyf 31449	The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- F = (mVT ` T )   &    |- Y = (mType ` T )   =>    |- ( T e. mFS -> Y : V --> F )
Theorem	mvtss 31450	The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- F = (mVT ` T )   &    |- K = (mTC ` T )   =>    |- ( T e. mFS -> F C_ K )
Theorem	maxsta 31451	An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- A = (mAx ` T )   &    |- S = (mStat ` T )   =>    |- ( T e. mFS -> A C_ S )
Theorem	mvtinf 31452	Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- F = (mVT ` T )   &    |- Y = (mType ` T )   =>    |- ( ( T e. mFS /\ X e. F ) -> -. ( `' Y " { X } ) e. Fin )
Theorem	msubff1 31453	When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   &    |- E = (mEx ` T )   =>    |- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( E ^m E ) )
Theorem	msubff1o 31454	When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- R = (mREx ` T )   &    |- S = (mSubst ` T )   =>    |- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S )
Theorem	mvhf 31455	The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- E = (mEx ` T )   &    |- H = (mVH ` T )   =>    |- ( T e. mFS -> H : V --> E )
Theorem	mvhf1 31456	The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- V = (mVR ` T )   &    |- E = (mEx ` T )   &    |- H = (mVH ` T )   =>    |- ( T e. mFS -> H : V -1-1-> E )
Theorem	msubvrs 31457*	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.)
|- S = (mSubst ` T )   &    |- E = (mEx ` T )   &    |- V = (mVars ` T )   &    |- H = (mVH ` T )   =>    |- ( ( T e. mFS /\ F e. ran S /\ X e. E ) -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) )
Theorem	mclsrcl 31458	Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   =>    |- ( A e. ( K C B ) -> ( T e. _V /\ K C_ D /\ B C_ E ) )
Theorem	mclsssvlem 31459*	Lemma for mclsssv 31461. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   &    |- A = (mAx ` T )   &    |- S = (mSubst ` T )   &    |- V = (mVars ` T )   =>    |- ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E )
Theorem	mclsval 31460*	The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   &    |- A = (mAx ` T )   &    |- S = (mSubst ` T )   &    |- V = (mVars ` T )   =>    |- ( ph -> ( K C B ) = |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
Theorem	mclsssv 31461	The closure of a set of expressions is a set of expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   =>    |- ( ph -> ( K C B ) C_ E )
Theorem	ssmclslem 31462	Lemma for ssmcls 31464. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   =>    |- ( ph -> ( B u. ran H ) C_ ( K C B ) )
Theorem	vhmcls 31463	All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- H = (mVH ` T )   &    |- V = (mVR ` T )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( H ` X ) e. ( K C B ) )
Theorem	ssmcls 31464	The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   =>    |- ( ph -> B C_ ( K C B ) )
Theorem	ss2mcls 31465	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.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- ( ph -> X C_ K )   &    |- ( ph -> Y C_ B )   =>    |- ( ph -> ( X C Y ) C_ ( K C B ) )
Theorem	mclsax 31466*	The closure is closed under axiom application. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- A = (mAx ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> <. M , O , P >. e. A )   &    |- ( ph -> S e. ran L )   &    |- ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )   &    |- ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )   &    |- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )   =>    |- ( ph -> ( S ` P ) e. ( K C B ) )
Theorem	mclsind 31467*	Induction theorem for closure: any other set Q closed under the axioms and the hypotheses contains all the elements of the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- A = (mAx ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> B C_ Q )   &    |- ( ( ph /\ v e. V ) -> ( H ` v ) e. Q )   &    |- ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. Q )   =>    |- ( ph -> ( K C B ) C_ Q )
Theorem	mppspstlem 31468*	Lemma for mppspst 31471. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   &    |- C = (mCls ` T )   =>    |- { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } C_ P
Theorem	mppsval 31469*	Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   &    |- C = (mCls ` T )   =>    |- J = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) }
Theorem	elmpps 31470	Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   &    |- C = (mCls ` T )   =>    |- ( <. D , H , A >. e. J <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) )
Theorem	mppspst 31471	A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- P = (mPreSt ` T )   &    |- J = (mPPSt ` T )   =>    |- J C_ P
Theorem	mthmval 31472	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.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- U = ( `' R " ( R " J ) )
Theorem	elmthm 31473*	A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- ( X e. U <-> E. x e. J ( R ` x ) = ( R ` X ) )
Theorem	mthmi 31474	A statement whose reduct is the reduct of a provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- ( ( X e. J /\ ( R ` X ) = ( R ` Y ) ) -> Y e. U )
Theorem	mthmsta 31475	A theorem is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- U = (mThm ` T )   &    |- S = (mPreSt ` T )   =>    |- U C_ S
Theorem	mppsthm 31476	A provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- J = (mPPSt ` T )   &    |- U = (mThm ` T )   =>    |- J C_ U
Theorem	mthmblem 31477	Lemma for mthmb 31478. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- U = (mThm ` T )   =>    |- ( ( R ` X ) = ( R ` Y ) -> ( X e. U -> Y e. U ) )
Theorem	mthmb 31478	If two statements have the same reduct then one is a theorem iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- U = (mThm ` T )   =>    |- ( ( R ` X ) = ( R ` Y ) -> ( X e. U <-> Y e. U ) )
Theorem	mthmpps 31479	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 dv conditions, which is sometimes inconvenient.) (Contributed by Mario Carneiro, 18-Jul-2016.)
|- R = (mStRed ` T )   &    |- J = (mPPSt ` T )   &    |- U = (mThm ` T )   &    |- D = (mDV ` T )   &    |- V = (mVars ` T )   &    |- Z = U. ( V " ( H u. { A } ) )   &    |- M = ( C u. ( D \ ( Z X. Z ) ) )   =>    |- ( T e. mFS -> ( <. C , H , A >. e. U <-> ( <. M , H , A >. e. J /\ ( R ` <. M , H , A >. ) = ( R ` <. C , H , A >. ) ) ) )
Theorem	mclsppslem 31480*	The closure is closed under application of provable pre-statements. (Compare mclsax 31466.) 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.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- J = (mPPSt ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> <. M , O , P >. e. J )   &    |- ( ph -> S e. ran L )   &    |- ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )   &    |- ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )   &    |- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )   &    |- ( ph -> <. m , o , p >. e. (mAx ` T ) )   &    |- ( ph -> s e. ran L )   &    |- ( ph -> ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) )   &    |- ( ph -> A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) )   =>    |- ( ph -> ( s ` p ) e. ( `' S " ( K C B ) ) )
Theorem	mclspps 31481*	The closure is closed under application of provable pre-statements. (Compare mclsax 31466.) 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.)
|- D = (mDV ` T )   &    |- E = (mEx ` T )   &    |- C = (mCls ` T )   &    |- ( ph -> T e. mFS )   &    |- ( ph -> K C_ D )   &    |- ( ph -> B C_ E )   &    |- J = (mPPSt ` T )   &    |- L = (mSubst ` T )   &    |- V = (mVR ` T )   &    |- H = (mVH ` T )   &    |- W = (mVars ` T )   &    |- ( ph -> <. M , O , P >. e. J )   &    |- ( ph -> S e. ran L )   &    |- ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )   &    |- ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )   &    |- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )   =>    |- ( ph -> ( S ` P ) e. ( K C B ) )
20.5.13  Grammatical formal systems
Syntax	cm0s 31482	Mapping expressions to statements.
class m0St
Syntax	cmsa 31483	The set of syntax axioms.
class mSA
Syntax	cmwgfs 31484	The set of weakly grammatical formal systems.
class mWGFS
Syntax	cmsy 31485	The syntax typecode function.
class mSyn
Syntax	cmesy 31486	The syntax typecode function for expressions.
class mESyn
Syntax	cmgfs 31487	The set of grammatical formal systems.
class mGFS
Syntax	cmtree 31488	The set of proof trees.
class mTree
Syntax	cmst 31489	The set of syntax trees.
class mST
Syntax	cmsax 31490	The indexing set for a syntax axiom.
class mSAX
Syntax	cmufs 31491	The set of unambiguous formal sytems.
class mUFS
Definition	df-m0s 31492	Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- m0St = ( a e. _V |-> <. (/) , (/) , a >. )
Definition	df-msa 31493*	Define the set of syntax axioms. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mSA = ( t e. _V |-> { a e. (mEx ` t ) | ( (m0St ` a ) e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` (mVR ` t ) ) ) } )
Definition	df-mwgfs 31494*	Define the set of weakly grammatical formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mWGFS = { t e. mFS | A. d A. h A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) ) }
Definition	df-msyn 31495	Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mSyn = Slot 6
Definition	df-mtree 31496*	Define the set of proof trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mTree = ( t e. _V |-> ( d e. ~P (mDV ` t ) , h e. ~P (mEx ` t ) |-> |^| { r | ( A. e e. ran (mVH ` t ) e r <. (m0St ` e ) , (/) >. /\ A. e e. h e r <. ( (mStRed ` t ) ` <. d , h , e >. ) , (/) >. /\ A. m A. o A. p ( <. m , o , p >. e. (mAx ` t ) -> A. s e. ran (mSubst ` t ) ( A. x A. y ( x m y -> ( ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) ) X. ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) ) ) C_ d ) -> ( { ( s ` p ) } X. X_ e e. ( o u. ( (mVH ` t ) " U. ( (mVars ` t ) " ( o u. { p } ) ) ) ) ( r " { ( s ` e ) } ) ) C_ r ) ) ) } ) )
Definition	df-mst 31497	Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mST = ( t e. _V |-> ( ( (/) (mTree ` t ) (/) ) |` ( (mEx ` t ) |` (mVT ` t ) ) ) )
Definition	df-msax 31498*	Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mSAX = ( t e. _V |-> ( p e. (mSA ` t ) |-> ( (mVH ` t ) " ( (mVars ` t ) ` p ) ) ) )
Definition	df-mufs 31499	Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mUFS = { t e. mGFS | Fun (mST ` t ) }
20.5.14  Models of formal systems
Syntax	cmuv 31500	The universe of a model.
class mUV