# 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}=\mathrm{mVR}\left({T}\right)$
mrsubvr.r ${⊢}{R}=\mathrm{mREx}\left({T}\right)$
mrsubvr.s ${⊢}{S}=\mathrm{mRSubst}\left({T}\right)$
Assertion mrsubrn ${⊢}\mathrm{ran}{S}={S}\left[{{R}}^{{V}}\right]$

### Proof

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