Metamath Proof Explorer


Theorem mrsubrn

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 mrsubvr.v V = mVR T
mrsubvr.r R = mREx T
mrsubvr.s S = mRSubst T
Assertion mrsubrn ran S = S R V

Proof

Step Hyp Ref Expression
1 mrsubvr.v V = mVR T
2 mrsubvr.r R = mREx T
3 mrsubvr.s S = mRSubst T
4 1 2 3 mrsubff T V S : R 𝑝𝑚 V R R
5 4 ffnd T V S Fn R 𝑝𝑚 V
6 eleq1w x = v x dom f v dom f
7 fveq2 x = v f x = f v
8 s1eq x = v ⟨“ x ”⟩ = ⟨“ v ”⟩
9 6 7 8 ifbieq12d x = v if x dom f f x ⟨“ x ”⟩ = if v dom f f v ⟨“ v ”⟩
10 eqid x V if x dom f f x ⟨“ x ”⟩ = x V if x dom f f x ⟨“ x ”⟩
11 fvex f v V
12 s1cli ⟨“ v ”⟩ Word V
13 12 elexi ⟨“ v ”⟩ V
14 11 13 ifex if v dom f f v ⟨“ v ”⟩ V
15 9 10 14 fvmpt v V x V if x dom f f x ⟨“ x ”⟩ v = if v dom f f v ⟨“ v ”⟩
16 15 adantl T V f R 𝑝𝑚 V v V x V if x dom f f x ⟨“ x ”⟩ v = if v dom f f v ⟨“ v ”⟩
17 16 ifeq1da T V f R 𝑝𝑚 V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩ = if v V if v dom f f v ⟨“ v ”⟩ ⟨“ v ”⟩
18 ifan if v V v dom f f v ⟨“ v ”⟩ = if v V if v dom f f v ⟨“ v ”⟩ ⟨“ v ”⟩
19 17 18 eqtr4di T V f R 𝑝𝑚 V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩ = if v V v dom f f v ⟨“ v ”⟩
20 elpmi f R 𝑝𝑚 V f : dom f R dom f V
21 20 adantl T V f R 𝑝𝑚 V f : dom f R dom f V
22 21 simprd T V f R 𝑝𝑚 V dom f V
23 22 sseld T V f R 𝑝𝑚 V v dom f v V
24 23 pm4.71rd T V f R 𝑝𝑚 V v dom f v V v dom f
25 24 bicomd T V f R 𝑝𝑚 V v V v dom f v dom f
26 25 ifbid T V f R 𝑝𝑚 V if v V v dom f f v ⟨“ v ”⟩ = if v dom f f v ⟨“ v ”⟩
27 19 26 eqtr2d T V f R 𝑝𝑚 V if v dom f f v ⟨“ v ”⟩ = if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩
28 27 mpteq2dv T V f R 𝑝𝑚 V v mCN T V if v dom f f v ⟨“ v ”⟩ = v mCN T V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩
29 28 coeq1d T V f R 𝑝𝑚 V v mCN T V if v dom f f v ⟨“ v ”⟩ e = v mCN T V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩ e
30 29 oveq2d T V f R 𝑝𝑚 V freeMnd mCN T V v mCN T V if v dom f f v ⟨“ v ”⟩ e = freeMnd mCN T V v mCN T V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩ e
31 30 mpteq2dv T V f R 𝑝𝑚 V e R freeMnd mCN T V v mCN T V if v dom f f v ⟨“ v ”⟩ e = e R freeMnd mCN T V v mCN T V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩ e
32 eqid mCN T = mCN T
33 eqid freeMnd mCN T V = freeMnd mCN T V
34 32 1 2 3 33 mrsubfval f : dom f R dom f V S f = e R freeMnd mCN T V v mCN T V if v dom f f v ⟨“ v ”⟩ e
35 21 34 syl T V f R 𝑝𝑚 V S f = e R freeMnd mCN T V v mCN T V if v dom f f v ⟨“ v ”⟩ e
36 21 simpld T V f R 𝑝𝑚 V f : dom f R
37 36 adantr T V f R 𝑝𝑚 V x V f : dom f R
38 37 ffvelrnda T V f R 𝑝𝑚 V x V x dom f f x R
39 elun2 x V x mCN T V
40 39 ad2antlr T V f R 𝑝𝑚 V x V ¬ x dom f x mCN T V
41 40 s1cld T V f R 𝑝𝑚 V x V ¬ x dom f ⟨“ x ”⟩ Word mCN T V
42 32 1 2 mrexval T V R = Word mCN T V
43 42 ad3antrrr T V f R 𝑝𝑚 V x V ¬ x dom f R = Word mCN T V
44 41 43 eleqtrrd T V f R 𝑝𝑚 V x V ¬ x dom f ⟨“ x ”⟩ R
45 38 44 ifclda T V f R 𝑝𝑚 V x V if x dom f f x ⟨“ x ”⟩ R
46 45 fmpttd T V f R 𝑝𝑚 V x V if x dom f f x ⟨“ x ”⟩ : V R
47 ssid V V
48 32 1 2 3 33 mrsubfval x V if x dom f f x ⟨“ x ”⟩ : V R V V S x V if x dom f f x ⟨“ x ”⟩ = e R freeMnd mCN T V v mCN T V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩ e
49 46 47 48 sylancl T V f R 𝑝𝑚 V S x V if x dom f f x ⟨“ x ”⟩ = e R freeMnd mCN T V v mCN T V if v V x V if x dom f f x ⟨“ x ”⟩ v ⟨“ v ”⟩ e
50 31 35 49 3eqtr4d T V f R 𝑝𝑚 V S f = S x V if x dom f f x ⟨“ x ”⟩
51 5 adantr T V f R 𝑝𝑚 V S Fn R 𝑝𝑚 V
52 mapsspm R V R 𝑝𝑚 V
53 52 a1i T V f R 𝑝𝑚 V R V R 𝑝𝑚 V
54 2 fvexi R V
55 1 fvexi V V
56 54 55 elmap x V if x dom f f x ⟨“ x ”⟩ R V x V if x dom f f x ⟨“ x ”⟩ : V R
57 46 56 sylibr T V f R 𝑝𝑚 V x V if x dom f f x ⟨“ x ”⟩ R V
58 fnfvima S Fn R 𝑝𝑚 V R V R 𝑝𝑚 V x V if x dom f f x ⟨“ x ”⟩ R V S x V if x dom f f x ⟨“ x ”⟩ S R V
59 51 53 57 58 syl3anc T V f R 𝑝𝑚 V S x V if x dom f f x ⟨“ x ”⟩ S R V
60 50 59 eqeltrd T V f R 𝑝𝑚 V S f S R V
61 60 ralrimiva T V f R 𝑝𝑚 V S f S R V
62 ffnfv S : R 𝑝𝑚 V S R V S Fn R 𝑝𝑚 V f R 𝑝𝑚 V S f S R V
63 5 61 62 sylanbrc T V S : R 𝑝𝑚 V S R V
64 63 frnd T V ran S S R V
65 3 rnfvprc ¬ T V ran S =
66 0ss S R V
67 65 66 eqsstrdi ¬ T V ran S S R V
68 64 67 pm2.61i ran S S R V
69 imassrn S R V ran S
70 68 69 eqssi ran S = S R V