Metamath Proof Explorer

Theorem msubrn

Description: Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (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 )
Assertion msubrn 
|- ran S = ( S " ( R ^m V ) )

Proof

Step Hyp Ref Expression
1 msubff.v 
 |-  V = ( mVR ` T )
2 msubff.r 
 |-  R = ( mREx ` T )
3 msubff.s 
 |-  S = ( mSubst ` T )
4 eqid 
 |-  ( mEx ` T ) = ( mEx ` T )
5 eqid 
 |-  ( mRSubst ` T ) = ( mRSubst ` T )
6 1 2 3 4 5 msubffval 
 |-  ( T e. _V -> S = ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) )
7 6 rneqd 
 |-  ( T e. _V -> ran S = ran ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) )
8 1 2 5 mrsubff 
 |-  ( T e. _V -> ( mRSubst ` T ) : ( R ^pm V ) --> ( R ^m R ) )
9 8 adantr 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( mRSubst ` T ) : ( R ^pm V ) --> ( R ^m R ) )
10 9 ffund 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> Fun ( mRSubst ` T ) )
11 8 ffnd 
 |-  ( T e. _V -> ( mRSubst ` T ) Fn ( R ^pm V ) )
12 fnfvelrn 
 |-  ( ( ( mRSubst ` T ) Fn ( R ^pm V ) /\ f e. ( R ^pm V ) ) -> ( ( mRSubst ` T ) ` f ) e. ran ( mRSubst ` T ) )
13 11 12 sylan 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( ( mRSubst ` T ) ` f ) e. ran ( mRSubst ` T ) )
14 1 2 5 mrsubrn 
 |-  ran ( mRSubst ` T ) = ( ( mRSubst ` T ) " ( R ^m V ) )
15 13 14 eleqtrdi 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( ( mRSubst ` T ) ` f ) e. ( ( mRSubst ` T ) " ( R ^m V ) ) )
16 fvelima 
 |-  ( ( Fun ( mRSubst ` T ) /\ ( ( mRSubst ` T ) ` f ) e. ( ( mRSubst ` T ) " ( R ^m V ) ) ) -> E. g e. ( R ^m V ) ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) )
17 10 15 16 syl2anc 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> E. g e. ( R ^m V ) ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) )
18 elmapi 
 |-  ( g e. ( R ^m V ) -> g : V --> R )
19 18 adantl 
 |-  ( ( T e. _V /\ g e. ( R ^m V ) ) -> g : V --> R )
20 ssid 
 |-  V C_ V
21 1 2 3 4 5 msubfval 
 |-  ( ( g : V --> R /\ V C_ V ) -> ( S ` g ) = ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) >. ) )
22 19 20 21 sylancl 
 |-  ( ( T e. _V /\ g e. ( R ^m V ) ) -> ( S ` g ) = ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) >. ) )
23 fvex 
 |-  ( mEx ` T ) e. _V
24 23 mptex 
 |-  ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) e. _V
25 eqid 
 |-  ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) = ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) )
26 24 25 fnmpti 
 |-  ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) Fn ( R ^pm V )
27 6 fneq1d 
 |-  ( T e. _V -> ( S Fn ( R ^pm V ) <-> ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) Fn ( R ^pm V ) ) )
28 26 27 mpbiri 
 |-  ( T e. _V -> S Fn ( R ^pm V ) )
29 28 adantr 
 |-  ( ( T e. _V /\ g e. ( R ^m V ) ) -> S Fn ( R ^pm V ) )
30 mapsspm 
 |-  ( R ^m V ) C_ ( R ^pm V )
31 30 a1i 
 |-  ( ( T e. _V /\ g e. ( R ^m V ) ) -> ( R ^m V ) C_ ( R ^pm V ) )
32 simpr 
 |-  ( ( T e. _V /\ g e. ( R ^m V ) ) -> g e. ( R ^m V ) )
33 fnfvima 
 |-  ( ( S Fn ( R ^pm V ) /\ ( R ^m V ) C_ ( R ^pm V ) /\ g e. ( R ^m V ) ) -> ( S ` g ) e. ( S " ( R ^m V ) ) )
34 29 31 32 33 syl3anc 
 |-  ( ( T e. _V /\ g e. ( R ^m V ) ) -> ( S ` g ) e. ( S " ( R ^m V ) ) )
35 22 34 eqeltrrd 
 |-  ( ( T e. _V /\ g e. ( R ^m V ) ) -> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) >. ) e. ( S " ( R ^m V ) ) )
36 35 adantlr 
 |-  ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ g e. ( R ^m V ) ) -> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) >. ) e. ( S " ( R ^m V ) ) )
37 fveq1 
 |-  ( ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) -> ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) = ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) )
38 37 opeq2d 
 |-  ( ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) -> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) >. = <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. )
39 38 mpteq2dv 
 |-  ( ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) -> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) >. ) = ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) )
40 39 eleq1d 
 |-  ( ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) -> ( ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` e ) ) >. ) e. ( S " ( R ^m V ) ) <-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) e. ( S " ( R ^m V ) ) ) )
41 36 40 syl5ibcom 
 |-  ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ g e. ( R ^m V ) ) -> ( ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) -> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) e. ( S " ( R ^m V ) ) ) )
42 41 rexlimdva 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( E. g e. ( R ^m V ) ( ( mRSubst ` T ) ` g ) = ( ( mRSubst ` T ) ` f ) -> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) e. ( S " ( R ^m V ) ) ) )
43 17 42 mpd 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) e. ( S " ( R ^m V ) ) )
44 43 fmpttd 
 |-  ( T e. _V -> ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) : ( R ^pm V ) --> ( S " ( R ^m V ) ) )
45 44 frnd 
 |-  ( T e. _V -> ran ( f e. ( R ^pm V ) |-> ( e e. ( mEx ` T ) |-> <. ( 1st ` e ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` e ) ) >. ) ) C_ ( S " ( R ^m V ) ) )
46 7 45 eqsstrd 
 |-  ( T e. _V -> ran S C_ ( S " ( R ^m V ) ) )
47 3 rnfvprc 
 |-  ( -. T e. _V -> ran S = (/) )
48 0ss 
 |-  (/) C_ ( S " ( R ^m V ) )
49 47 48 eqsstrdi 
 |-  ( -. T e. _V -> ran S C_ ( S " ( R ^m V ) ) )
50 46 49 pm2.61i 
 |-  ran S C_ ( S " ( R ^m V ) )
51 imassrn 
 |-  ( S " ( R ^m V ) ) C_ ran S
52 50 51 eqssi 
 |-  ran S = ( S " ( R ^m V ) )