Definition df-mrsub 29114

Description: Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-mrsub	|- mRSubst = ( t e. _V |-> ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mREx ` t ) |-> ( (freeMnd ` ( (mCN ` t ) u. (mVR ` t ) ) ) gsumg ( ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )

Distinct variable group:   e, f, t, v

Detailed syntax breakdown of Definition df-mrsub

Step	Hyp	Ref	Expression
1		cmrsub 29094	. 2 class mRSubst
2		vt	. . 3 setvar t
3		cvv 3106	. . 3 class _V
4		vf	. . . 4 setvar f
5	2	cv 1397	. . . . . 6 class t
6		cmrex 29090	. . . . . 6 class mREx
7	5, 6	cfv 5570	. . . . 5 class (mREx ` t )
8		cmvar 29085	. . . . . 6 class mVR
9	5, 8	cfv 5570	. . . . 5 class (mVR ` t )
10		cpm 7413	. . . . 5 class ^pm
11	7, 9, 10	co 6270	. . . 4 class ( (mREx ` t ) ^pm (mVR ` t ) )
12		ve	. . . . 5 setvar e
13		cmcn 29084	. . . . . . . . 9 class mCN
14	5, 13	cfv 5570	. . . . . . . 8 class (mCN ` t )
15	14, 9	cun 3459	. . . . . . 7 class ( (mCN ` t ) u. (mVR ` t ) )
16		cfrmd 16214	. . . . . . 7 class freeMnd
17	15, 16	cfv 5570	. . . . . 6 class (freeMnd ` ( (mCN ` t ) u. (mVR ` t ) ) )
18		vv	. . . . . . . 8 setvar v
19	18	cv 1397	. . . . . . . . . 10 class v
20	4	cv 1397	. . . . . . . . . . 11 class f
21	20	cdm 4988	. . . . . . . . . 10 class dom f
22	19, 21	wcel 1823	. . . . . . . . 9 wff v e. dom f
23	19, 20	cfv 5570	. . . . . . . . 9 class ( f ` v )
24	19	cs1 12521	. . . . . . . . 9 class <" v ">
25	22, 23, 24	cif 3929	. . . . . . . 8 class if ( v e. dom f , ( f ` v ) , <" v "> )
26	18, 15, 25	cmpt 4497	. . . . . . 7 class ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) )
27	12	cv 1397	. . . . . . 7 class e
28	26, 27	ccom 4992	. . . . . 6 class ( ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e )
29		cgsu 14930	. . . . . 6 class gsumg
30	17, 28, 29	co 6270	. . . . 5 class ( (freeMnd ` ( (mCN ` t ) u. (mVR ` t ) ) ) gsumg ( ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) )
31	12, 7, 30	cmpt 4497	. . . 4 class ( e e. (mREx ` t ) |-> ( (freeMnd ` ( (mCN ` t ) u. (mVR ` t ) ) ) gsumg ( ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) )
32	4, 11, 31	cmpt 4497	. . 3 class ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mREx ` t ) |-> ( (freeMnd ` ( (mCN ` t ) u. (mVR ` t ) ) ) gsumg ( ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) )
33	2, 3, 32	cmpt 4497	. 2 class ( t e. _V |-> ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mREx ` t ) |-> ( (freeMnd ` ( (mCN ` t ) u. (mVR ` t ) ) ) gsumg ( ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
34	1, 33	wceq 1398	1 wff mRSubst = ( t e. _V |-> ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mREx ` t ) |-> ( (freeMnd ` ( (mCN ` t ) u. (mVR ` t ) ) ) gsumg ( ( v e. ( (mCN ` t ) u. (mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )

This definition is referenced by:  mrsubffval  29131