Metamath Proof Explorer

Definition df-msub

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

Ref Expression
Assertion df-msub 
|- mSubst = ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsub 
 |-  mSubst
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vf 
 |-  f
4 cmrex 
 |-  mREx
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mREx ` t )
7 cpm 
 |-  ^pm
8 cmvar 
 |-  mVR
9 5 8 cfv 
 |-  ( mVR ` t )
10 6 9 7 co 
 |-  ( ( mREx ` t ) ^pm ( mVR ` t ) )
11 ve 
 |-  e
12 cmex 
 |-  mEx
13 5 12 cfv 
 |-  ( mEx ` t )
14 c1st 
 |-  1st
15 11 cv 
 |-  e
16 15 14 cfv 
 |-  ( 1st ` e )
17 cmrsub 
 |-  mRSubst
18 5 17 cfv 
 |-  ( mRSubst ` t )
19 3 cv 
 |-  f
20 19 18 cfv 
 |-  ( ( mRSubst ` t ) ` f )
21 c2nd 
 |-  2nd
22 15 21 cfv 
 |-  ( 2nd ` e )
23 22 20 cfv 
 |-  ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) )
24 16 23 cop 
 |-  <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >.
25 11 13 24 cmpt 
 |-  ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. )
26 3 10 25 cmpt 
 |-  ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) )
27 1 2 26 cmpt 
 |-  ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) )
28 0 27 wceq 
 |-  mSubst = ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) )