Metamath Proof Explorer

Theorem msubff

Description: A substitution is a function from E to E . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msubff.v 
|- V = ( mVR ` T )
msubff.r 
|- R = ( mREx ` T )
msubff.s 
|- S = ( mSubst ` T )
msubff.e 
|- E = ( mEx ` T )
Assertion msubff 
|- ( T e. W -> S : ( R ^pm V ) --> ( E ^m E ) )

Proof

Step Hyp Ref Expression
1 msubff.v 
 |-  V = ( mVR ` T )
2 msubff.r 
 |-  R = ( mREx ` T )
3 msubff.s 
 |-  S = ( mSubst ` T )
4 msubff.e 
 |-  E = ( mEx ` T )
5 xp1st 
 |-  ( e e. ( ( mTC ` T ) X. R ) -> ( 1st ` e ) e. ( mTC ` T ) )
6 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
7 6 4 2 mexval 
 |-  E = ( ( mTC ` T ) X. R )
8 5 7 eleq2s 
 |-  ( e e. E -> ( 1st ` e ) e. ( mTC ` T ) )
9 8 adantl 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. E ) -> ( 1st ` e ) e. ( mTC ` T ) )
10 eqid 
 |-  ( mRSubst ` T ) = ( mRSubst ` T )
11 1 2 10 mrsubff 
 |-  ( T e. W -> ( mRSubst ` T ) : ( R ^pm V ) --> ( R ^m R ) )
12 11 ffvelrnda 
 |-  ( ( T e. W /\ f e. ( R ^pm V ) ) -> ( ( mRSubst ` T ) ` f ) e. ( R ^m R ) )
13 elmapi 
 |-  ( ( ( mRSubst ` T ) ` f ) e. ( R ^m R ) -> ( ( mRSubst ` T ) ` f ) : R --> R )
14 12 13 syl 
 |-  ( ( T e. W /\ f e. ( R ^pm V ) ) -> ( ( mRSubst ` T ) ` f ) : R --> R )
15 xp2nd 
 |-  ( e e. ( ( mTC ` T ) X. R ) -> ( 2nd ` e ) e. R )
16 15 7 eleq2s 
 |-  ( e e. E -> ( 2nd ` e ) e. R )
17 ffvelrn 
 |-  ( ( ( ( mRSubst ` T ) ` f ) : R --> R /\ ( 2nd ` e ) e. R ) -> ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) e. R )
18 14 16 17 syl2an 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. E ) -> ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) e. R )
19 opelxp 
 |-  ( <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. e. ( ( mTC ` T ) X. R ) <-> ( ( 1st ` e ) e. ( mTC ` T ) /\ ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) e. R ) )
20 9 18 19 sylanbrc 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. E ) -> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. e. ( ( mTC ` T ) X. R ) )
21 20 7 eleqtrrdi 
 |-  ( ( ( T e. W /\ f e. ( R ^pm V ) ) /\ e e. E ) -> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. e. E )
22 21 fmpttd 
 |-  ( ( T e. W /\ f e. ( R ^pm V ) ) -> ( e e. E |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) : E --> E )
23 4 fvexi 
 |-  E e. _V
24 23 23 elmap 
 |-  ( ( e e. E |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) e. ( E ^m E ) <-> ( e e. E |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) : E --> E )
25 22 24 sylibr 
 |-  ( ( T e. W /\ f e. ( R ^pm V ) ) -> ( e e. E |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) e. ( E ^m E ) )
26 25 fmpttd 
 |-  ( T e. W -> ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) : ( R ^pm V ) --> ( E ^m E ) )
27 1 2 3 4 10 msubffval 
 |-  ( T e. W -> S = ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) )
28 27 feq1d 
 |-  ( T e. W -> ( S : ( R ^pm V ) --> ( E ^m E ) <-> ( f e. ( R ^pm V ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) : ( R ^pm V ) --> ( E ^m E ) ) )
29 26 28 mpbird 
 |-  ( T e. W -> S : ( R ^pm V ) --> ( E ^m E ) )