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 ran O e E 1 st e f 2 nd 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 V S = g mREx T 𝑝𝑚 mVR T e E 1 st e O g 2 nd e
7 4 5 2 mrsubff T V O : mREx T 𝑝𝑚 mVR T mREx T mREx T
8 7 ffnd T V O Fn mREx T 𝑝𝑚 mVR T
9 fnfvelrn O Fn mREx T 𝑝𝑚 mVR T g mREx T 𝑝𝑚 mVR T O g ran O
10 8 9 sylan T V g mREx T 𝑝𝑚 mVR T O g ran O
11 7 feqmptd T V O = g mREx T 𝑝𝑚 mVR T O g
12 eqidd T V f ran O e E 1 st e f 2 nd e = f ran O e E 1 st e f 2 nd e
13 fveq1 f = O g f 2 nd e = O g 2 nd e
14 13 opeq2d f = O g 1 st e f 2 nd e = 1 st e O g 2 nd e
15 14 mpteq2dv f = O g e E 1 st e f 2 nd e = e E 1 st e O g 2 nd e
16 10 11 12 15 fmptco T V f ran O e E 1 st e f 2 nd e O = g mREx T 𝑝𝑚 mVR T e E 1 st e O g 2 nd e
17 6 16 eqtr4d T V S = f ran O e E 1 st e f 2 nd e O
18 17 rneqd T V ran S = ran f ran O e E 1 st e f 2 nd e O
19 rnco ran f ran O e E 1 st e f 2 nd e O = ran f ran O e E 1 st e f 2 nd e ran O
20 ssid ran O ran O
21 resmpt ran O ran O f ran O e E 1 st e f 2 nd e ran O = f ran O e E 1 st e f 2 nd e
22 20 21 ax-mp f ran O e E 1 st e f 2 nd e ran O = f ran O e E 1 st e f 2 nd e
23 22 rneqi ran f ran O e E 1 st e f 2 nd e ran O = ran f ran O e E 1 st e f 2 nd e
24 19 23 eqtri ran f ran O e E 1 st e f 2 nd e O = ran f ran O e E 1 st e f 2 nd e
25 18 24 eqtrdi T V ran S = ran f ran O e E 1 st e f 2 nd e
26 mpt0 f e E 1 st e f 2 nd e =
27 26 eqcomi = f e E 1 st e f 2 nd e
28 fvprc ¬ T V mSubst T =
29 3 28 syl5eq ¬ T V S =
30 2 rnfvprc ¬ T V ran O =
31 30 mpteq1d ¬ T V f ran O e E 1 st e f 2 nd e = f e E 1 st e f 2 nd e
32 27 29 31 3eqtr4a ¬ T V S = f ran O e E 1 st e f 2 nd e
33 32 rneqd ¬ T V ran S = ran f ran O e E 1 st e f 2 nd e
34 25 33 pm2.61i ran S = ran f ran O e E 1 st e f 2 nd e