Metamath Proof Explorer

Theorem msubffval

Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msubffval.v 
|- V = ( mVR ` T )
msubffval.r 
|- R = ( mREx ` T )
msubffval.s 
|- S = ( mSubst ` T )
msubffval.e 
|- E = ( mEx ` T )
msubffval.o 
|- O = ( mRSubst ` T )
Assertion msubffval 
|- ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )

Proof

Step Hyp Ref Expression
1 msubffval.v 
 |-  V = ( mVR ` T )
2 msubffval.r 
 |-  R = ( mREx ` T )
3 msubffval.s 
 |-  S = ( mSubst ` T )
4 msubffval.e 
 |-  E = ( mEx ` T )
5 msubffval.o 
 |-  O = ( mRSubst ` T )
6 elex 
 |-  ( T e. W -> T e. _V )
7 fveq2 
 |-  ( t = T -> ( mREx ` t ) = ( mREx ` T ) )
8 7 2 eqtr4di 
 |-  ( t = T -> ( mREx ` t ) = R )
9 fveq2 
 |-  ( t = T -> ( mVR ` t ) = ( mVR ` T ) )
10 9 1 eqtr4di 
 |-  ( t = T -> ( mVR ` t ) = V )
11 8 10 oveq12d 
 |-  ( t = T -> ( ( mREx ` t ) ^pm ( mVR ` t ) ) = ( R ^pm V ) )
12 fveq2 
 |-  ( t = T -> ( mEx ` t ) = ( mEx ` T ) )
13 12 4 eqtr4di 
 |-  ( t = T -> ( mEx ` t ) = E )
14 fveq2 
 |-  ( t = T -> ( mRSubst ` t ) = ( mRSubst ` T ) )
15 14 5 eqtr4di 
 |-  ( t = T -> ( mRSubst ` t ) = O )
16 15 fveq1d 
 |-  ( t = T -> ( ( mRSubst ` t ) ` f ) = ( O ` f ) )
17 16 fveq1d 
 |-  ( t = T -> ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) = ( ( O ` f ) ` ( 2nd ` e ) ) )
18 17 opeq2d 
 |-  ( t = T -> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. = <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. )
19 13 18 mpteq12dv 
 |-  ( t = T -> ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) )
20 11 19 mpteq12dv 
 |-  ( t = T -> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )
21 df-msub 
 |-  mSubst = ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mEx ` t ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) )
22 ovex 
 |-  ( R ^pm V ) e. _V
23 22 mptex 
 |-  ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) e. _V
24 20 21 23 fvmpt 
 |-  ( T e. _V -> ( mSubst ` T ) = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )
25 3 24 syl5eq 
 |-  ( T e. _V -> S = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )
26 6 25 syl 
 |-  ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )