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 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 V S = f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e
7 6 rneqd T V ran S = ran f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e
8 1 2 5 mrsubff T V mRSubst T : R 𝑝𝑚 V R R
9 8 adantr T V f R 𝑝𝑚 V mRSubst T : R 𝑝𝑚 V R R
10 9 ffund T V f R 𝑝𝑚 V Fun mRSubst T
11 8 ffnd T V mRSubst T Fn R 𝑝𝑚 V
12 fnfvelrn mRSubst T Fn R 𝑝𝑚 V f R 𝑝𝑚 V mRSubst T f ran mRSubst T
13 11 12 sylan T V f R 𝑝𝑚 V mRSubst T f ran mRSubst T
14 1 2 5 mrsubrn ran mRSubst T = mRSubst T R V
15 13 14 eleqtrdi T V f R 𝑝𝑚 V mRSubst T f mRSubst T R V
16 fvelima Fun mRSubst T mRSubst T f mRSubst T R V g R V mRSubst T g = mRSubst T f
17 10 15 16 syl2anc T V f R 𝑝𝑚 V g R V mRSubst T g = mRSubst T f
18 elmapi g R V g : V R
19 18 adantl T V g R V g : V R
20 ssid V V
21 1 2 3 4 5 msubfval g : V R V V S g = e mEx T 1 st e mRSubst T g 2 nd e
22 19 20 21 sylancl T V g R V S g = e mEx T 1 st e mRSubst T g 2 nd e
23 fvex mEx T V
24 23 mptex e mEx T 1 st e mRSubst T f 2 nd e V
25 eqid f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e = f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e
26 24 25 fnmpti f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e Fn R 𝑝𝑚 V
27 6 fneq1d T V S Fn R 𝑝𝑚 V f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e Fn R 𝑝𝑚 V
28 26 27 mpbiri T V S Fn R 𝑝𝑚 V
29 28 adantr T V g R V S Fn R 𝑝𝑚 V
30 mapsspm R V R 𝑝𝑚 V
31 30 a1i T V g R V R V R 𝑝𝑚 V
32 simpr T V g R V g R V
33 fnfvima S Fn R 𝑝𝑚 V R V R 𝑝𝑚 V g R V S g S R V
34 29 31 32 33 syl3anc T V g R V S g S R V
35 22 34 eqeltrrd T V g R V e mEx T 1 st e mRSubst T g 2 nd e S R V
36 35 adantlr T V f R 𝑝𝑚 V g R V e mEx T 1 st e mRSubst T g 2 nd e S R V
37 fveq1 mRSubst T g = mRSubst T f mRSubst T g 2 nd e = mRSubst T f 2 nd e
38 37 opeq2d mRSubst T g = mRSubst T f 1 st e mRSubst T g 2 nd e = 1 st e mRSubst T f 2 nd e
39 38 mpteq2dv mRSubst T g = mRSubst T f e mEx T 1 st e mRSubst T g 2 nd e = e mEx T 1 st e mRSubst T f 2 nd e
40 39 eleq1d mRSubst T g = mRSubst T f e mEx T 1 st e mRSubst T g 2 nd e S R V e mEx T 1 st e mRSubst T f 2 nd e S R V
41 36 40 syl5ibcom T V f R 𝑝𝑚 V g R V mRSubst T g = mRSubst T f e mEx T 1 st e mRSubst T f 2 nd e S R V
42 41 rexlimdva T V f R 𝑝𝑚 V g R V mRSubst T g = mRSubst T f e mEx T 1 st e mRSubst T f 2 nd e S R V
43 17 42 mpd T V f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e S R V
44 43 fmpttd T V f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e : R 𝑝𝑚 V S R V
45 44 frnd T V ran f R 𝑝𝑚 V e mEx T 1 st e mRSubst T f 2 nd e S R V
46 7 45 eqsstrd T V ran S S R V
47 3 rnfvprc ¬ T V ran S =
48 0ss S R V
49 47 48 eqsstrdi ¬ T V ran S S R V
50 46 49 pm2.61i ran S S R V
51 imassrn S R V ran S
52 50 51 eqssi ran S = S R V