# Metamath Proof Explorer

## Theorem mrsub0

Description: The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis mrsubccat.s ${⊢}{S}=\mathrm{mRSubst}\left({T}\right)$
Assertion mrsub0 ${⊢}{F}\in \mathrm{ran}{S}\to {F}\left(\varnothing \right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 mrsubccat.s ${⊢}{S}=\mathrm{mRSubst}\left({T}\right)$
2 n0i ${⊢}{F}\in \mathrm{ran}{S}\to ¬\mathrm{ran}{S}=\varnothing$
3 1 rnfvprc ${⊢}¬{T}\in \mathrm{V}\to \mathrm{ran}{S}=\varnothing$
4 2 3 nsyl2 ${⊢}{F}\in \mathrm{ran}{S}\to {T}\in \mathrm{V}$
5 eqid ${⊢}\mathrm{mVR}\left({T}\right)=\mathrm{mVR}\left({T}\right)$
6 eqid ${⊢}\mathrm{mREx}\left({T}\right)=\mathrm{mREx}\left({T}\right)$
7 5 6 1 mrsubff ${⊢}{T}\in \mathrm{V}\to {S}:\mathrm{mREx}\left({T}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({T}\right)⟶{\mathrm{mREx}\left({T}\right)}^{\mathrm{mREx}\left({T}\right)}$
8 ffun ${⊢}{S}:\mathrm{mREx}\left({T}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({T}\right)⟶{\mathrm{mREx}\left({T}\right)}^{\mathrm{mREx}\left({T}\right)}\to \mathrm{Fun}{S}$
9 4 7 8 3syl ${⊢}{F}\in \mathrm{ran}{S}\to \mathrm{Fun}{S}$
10 5 6 1 mrsubrn ${⊢}\mathrm{ran}{S}={S}\left[{\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right]$
11 10 eleq2i ${⊢}{F}\in \mathrm{ran}{S}↔{F}\in {S}\left[{\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right]$
12 11 biimpi ${⊢}{F}\in \mathrm{ran}{S}\to {F}\in {S}\left[{\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right]$
13 fvelima ${⊢}\left(\mathrm{Fun}{S}\wedge {F}\in {S}\left[{\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right]\right)\to \exists {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\phantom{\rule{.4em}{0ex}}{S}\left({f}\right)={F}$
14 9 12 13 syl2anc ${⊢}{F}\in \mathrm{ran}{S}\to \exists {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\phantom{\rule{.4em}{0ex}}{S}\left({f}\right)={F}$
15 elmapi ${⊢}{f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\to {f}:\mathrm{mVR}\left({T}\right)⟶\mathrm{mREx}\left({T}\right)$
16 15 adantl ${⊢}\left({T}\in \mathrm{V}\wedge {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\right)\to {f}:\mathrm{mVR}\left({T}\right)⟶\mathrm{mREx}\left({T}\right)$
17 ssidd ${⊢}\left({T}\in \mathrm{V}\wedge {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\right)\to \mathrm{mVR}\left({T}\right)\subseteq \mathrm{mVR}\left({T}\right)$
18 wrd0 ${⊢}\varnothing \in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)$
19 eqid ${⊢}\mathrm{mCN}\left({T}\right)=\mathrm{mCN}\left({T}\right)$
20 19 5 6 mrexval ${⊢}{T}\in \mathrm{V}\to \mathrm{mREx}\left({T}\right)=\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)$
21 20 adantr ${⊢}\left({T}\in \mathrm{V}\wedge {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\right)\to \mathrm{mREx}\left({T}\right)=\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)$
22 18 21 eleqtrrid ${⊢}\left({T}\in \mathrm{V}\wedge {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\right)\to \varnothing \in \mathrm{mREx}\left({T}\right)$
23 eqid ${⊢}\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)=\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)$
24 19 5 6 1 23 mrsubval ${⊢}\left({f}:\mathrm{mVR}\left({T}\right)⟶\mathrm{mREx}\left({T}\right)\wedge \mathrm{mVR}\left({T}\right)\subseteq \mathrm{mVR}\left({T}\right)\wedge \varnothing \in \mathrm{mREx}\left({T}\right)\right)\to {S}\left({f}\right)\left(\varnothing \right)={\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)⟼if\left({v}\in \mathrm{mVR}\left({T}\right),{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ \varnothing \right)$
25 16 17 22 24 syl3anc ${⊢}\left({T}\in \mathrm{V}\wedge {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\right)\to {S}\left({f}\right)\left(\varnothing \right)={\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)⟼if\left({v}\in \mathrm{mVR}\left({T}\right),{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ \varnothing \right)$
26 co02 ${⊢}\left({v}\in \left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)⟼if\left({v}\in \mathrm{mVR}\left({T}\right),{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ \varnothing =\varnothing$
27 26 oveq2i ${⊢}{\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)⟼if\left({v}\in \mathrm{mVR}\left({T}\right),{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ \varnothing \right)={\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)}\varnothing$
28 23 frmd0 ${⊢}\varnothing ={0}_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)}$
29 28 gsum0 ${⊢}{\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)}\varnothing =\varnothing$
30 27 29 eqtri ${⊢}{\sum }_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)}\left(\left({v}\in \left(\mathrm{mCN}\left({T}\right)\cup \mathrm{mVR}\left({T}\right)\right)⟼if\left({v}\in \mathrm{mVR}\left({T}\right),{f}\left({v}\right),⟨“{v}”⟩\right)\right)\circ \varnothing \right)=\varnothing$
31 25 30 syl6eq ${⊢}\left({T}\in \mathrm{V}\wedge {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\right)\to {S}\left({f}\right)\left(\varnothing \right)=\varnothing$
32 fveq1 ${⊢}{S}\left({f}\right)={F}\to {S}\left({f}\right)\left(\varnothing \right)={F}\left(\varnothing \right)$
33 32 eqeq1d ${⊢}{S}\left({f}\right)={F}\to \left({S}\left({f}\right)\left(\varnothing \right)=\varnothing ↔{F}\left(\varnothing \right)=\varnothing \right)$
34 31 33 syl5ibcom ${⊢}\left({T}\in \mathrm{V}\wedge {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\right)\to \left({S}\left({f}\right)={F}\to {F}\left(\varnothing \right)=\varnothing \right)$
35 34 rexlimdva ${⊢}{T}\in \mathrm{V}\to \left(\exists {f}\in \left({\mathrm{mREx}\left({T}\right)}^{\mathrm{mVR}\left({T}\right)}\right)\phantom{\rule{.4em}{0ex}}{S}\left({f}\right)={F}\to {F}\left(\varnothing \right)=\varnothing \right)$
36 4 14 35 sylc ${⊢}{F}\in \mathrm{ran}{S}\to {F}\left(\varnothing \right)=\varnothing$