Metamath Proof Explorer

Theorem msubfval

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 msubfval 
|- ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( 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 1 2 3 4 5 msubffval 
 |-  ( T e. _V -> S = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )
7 6 adantr 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> S = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) ) )
8 simplr 
 |-  ( ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) /\ e e. E ) -> f = F )
9 8 fveq2d 
 |-  ( ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) /\ e e. E ) -> ( O ` f ) = ( O ` F ) )
10 9 fveq1d 
 |-  ( ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) /\ e e. E ) -> ( ( O ` f ) ` ( 2nd ` e ) ) = ( ( O ` F ) ` ( 2nd ` e ) ) )
11 10 opeq2d 
 |-  ( ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) /\ e e. E ) -> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. = <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. )
12 11 mpteq2dva 
 |-  ( ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) /\ f = F ) -> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` f ) ` ( 2nd ` e ) ) >. ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )
13 2 fvexi 
 |-  R e. _V
14 1 fvexi 
 |-  V e. _V
15 13 14 pm3.2i 
 |-  ( R e. _V /\ V e. _V )
16 15 a1i 
 |-  ( T e. _V -> ( R e. _V /\ V e. _V ) )
17 elpm2r 
 |-  ( ( ( R e. _V /\ V e. _V ) /\ ( F : A --> R /\ A C_ V ) ) -> F e. ( R ^pm V ) )
18 16 17 sylan 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> F e. ( R ^pm V ) )
19 4 fvexi 
 |-  E e. _V
20 19 mptex 
 |-  ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) e. _V
21 20 a1i 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) e. _V )
22 7 12 18 21 fvmptd 
 |-  ( ( T e. _V /\ ( F : A --> R /\ A C_ V ) ) -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )
23 22 ex 
 |-  ( T e. _V -> ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) ) )
24 0fv 
 |-  ( (/) ` F ) = (/)
25 mpt0 
 |-  ( e e. (/) |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) = (/)
26 24 25 eqtr4i 
 |-  ( (/) ` F ) = ( e e. (/) |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. )
27 fvprc 
 |-  ( -. T e. _V -> ( mSubst ` T ) = (/) )
28 3 27 syl5eq 
 |-  ( -. T e. _V -> S = (/) )
29 28 fveq1d 
 |-  ( -. T e. _V -> ( S ` F ) = ( (/) ` F ) )
30 fvprc 
 |-  ( -. T e. _V -> ( mEx ` T ) = (/) )
31 4 30 syl5eq 
 |-  ( -. T e. _V -> E = (/) )
32 31 mpteq1d 
 |-  ( -. T e. _V -> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) = ( e e. (/) |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )
33 26 29 32 3eqtr4a 
 |-  ( -. T e. _V -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )
34 33 a1d 
 |-  ( -. T e. _V -> ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) ) )
35 23 34 pm2.61i 
 |-  ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )