Metamath Proof Explorer

Theorem elmsubrn

Description: Characterization of substitution in terms of raw substitution, without reference to the generating functions. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses elmsubrn.e 
|- E = ( mEx ` T )
elmsubrn.o 
|- O = ( mRSubst ` T )
elmsubrn.s 
|- S = ( mSubst ` T )
Assertion elmsubrn 
|- ran S = ran ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )

Proof

Step Hyp Ref Expression
1 elmsubrn.e 
 |-  E = ( mEx ` T )
2 elmsubrn.o 
 |-  O = ( mRSubst ` T )
3 elmsubrn.s 
 |-  S = ( mSubst ` T )
4 eqid 
 |-  ( mVR ` T ) = ( mVR ` T )
5 eqid 
 |-  ( mREx ` T ) = ( mREx ` T )
6 4 5 3 1 2 msubffval 
 |-  ( T e. _V -> S = ( g e. ( ( mREx ` T ) ^pm ( mVR ` T ) ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` g ) ` ( 2nd ` e ) ) >. ) ) )
7 4 5 2 mrsubff 
 |-  ( T e. _V -> O : ( ( mREx ` T ) ^pm ( mVR ` T ) ) --> ( ( mREx ` T ) ^m ( mREx ` T ) ) )
8 7 ffnd 
 |-  ( T e. _V -> O Fn ( ( mREx ` T ) ^pm ( mVR ` T ) ) )
9 fnfvelrn 
 |-  ( ( O Fn ( ( mREx ` T ) ^pm ( mVR ` T ) ) /\ g e. ( ( mREx ` T ) ^pm ( mVR ` T ) ) ) -> ( O ` g ) e. ran O )
10 8 9 sylan 
 |-  ( ( T e. _V /\ g e. ( ( mREx ` T ) ^pm ( mVR ` T ) ) ) -> ( O ` g ) e. ran O )
11 7 feqmptd 
 |-  ( T e. _V -> O = ( g e. ( ( mREx ` T ) ^pm ( mVR ` T ) ) |-> ( O ` g ) ) )
12 eqidd 
 |-  ( T e. _V -> ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) = ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) )
13 fveq1 
 |-  ( f = ( O ` g ) -> ( f ` ( 2nd ` e ) ) = ( ( O ` g ) ` ( 2nd ` e ) ) )
14 13 opeq2d 
 |-  ( f = ( O ` g ) -> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. = <. ( 1st ` e ) , ( ( O ` g ) ` ( 2nd ` e ) ) >. )
15 14 mpteq2dv 
 |-  ( f = ( O ` g ) -> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` g ) ` ( 2nd ` e ) ) >. ) )
16 10 11 12 15 fmptco 
 |-  ( T e. _V -> ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) o. O ) = ( g e. ( ( mREx ` T ) ^pm ( mVR ` T ) ) |-> ( e e. E |-> <. ( 1st ` e ) , ( ( O ` g ) ` ( 2nd ` e ) ) >. ) ) )
17 6 16 eqtr4d 
 |-  ( T e. _V -> S = ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) o. O ) )
18 17 rneqd 
 |-  ( T e. _V -> ran S = ran ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) o. O ) )
19 rnco 
 |-  ran ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) o. O ) = ran ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) |` ran O )
20 ssid 
 |-  ran O C_ ran O
21 resmpt 
 |-  ( ran O C_ ran O -> ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) |` ran O ) = ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) )
22 20 21 ax-mp 
 |-  ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) |` ran O ) = ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
23 22 rneqi 
 |-  ran ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) |` ran O ) = ran ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
24 19 23 eqtri 
 |-  ran ( ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) o. O ) = ran ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
25 18 24 eqtrdi 
 |-  ( T e. _V -> ran S = ran ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) )
26 mpt0 
 |-  ( f e. (/) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) = (/)
27 26 eqcomi 
 |-  (/) = ( f e. (/) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
28 fvprc 
 |-  ( -. T e. _V -> ( mSubst ` T ) = (/) )
29 3 28 syl5eq 
 |-  ( -. T e. _V -> S = (/) )
30 2 rnfvprc 
 |-  ( -. T e. _V -> ran O = (/) )
31 30 mpteq1d 
 |-  ( -. T e. _V -> ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) = ( f e. (/) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) )
32 27 29 31 3eqtr4a 
 |-  ( -. T e. _V -> S = ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) )
33 32 rneqd 
 |-  ( -. T e. _V -> ran S = ran ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) )
34 25 33 pm2.61i 
 |-  ran S = ran ( f e. ran O |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )