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=mRSubst⁡T
Assertion mrsub0 ⊢F∈ran⁡S→F⁡∅=∅

Proof

Step Hyp Ref Expression
1 mrsubccat.s ⊢S=mRSubst⁡T
2 n0i ⊢F∈ran⁡S→¬ran⁡S=∅
3 1 rnfvprc ⊢¬T∈V→ran⁡S=∅
4 2 3 nsyl2 ⊢F∈ran⁡S→T∈V
5 eqid ⊢mVR⁡T=mVR⁡T
6 eqid ⊢mREx⁡T=mREx⁡T
7 5 6 1 mrsubff ⊢T∈V→S:mREx⁡T↑𝑝𝑚mVR⁡T⟶mREx⁡TmREx⁡T
8 ffun ⊢S:mREx⁡T↑𝑝𝑚mVR⁡T⟶mREx⁡TmREx⁡T→Fun⁡S
9 4 7 8 3syl ⊢F∈ran⁡S→Fun⁡S
10 5 6 1 mrsubrn ⊢ran⁡S=SmREx⁡TmVR⁡T
11 10 eleq2i ⊢F∈ran⁡S↔F∈SmREx⁡TmVR⁡T
12 11 biimpi ⊢F∈ran⁡S→F∈SmREx⁡TmVR⁡T
13 fvelima ⊢Fun⁡S∧F∈SmREx⁡TmVR⁡T→∃f∈mREx⁡TmVR⁡TS⁡f=F
14 9 12 13 syl2anc ⊢F∈ran⁡S→∃f∈mREx⁡TmVR⁡TS⁡f=F
15 elmapi ⊢f∈mREx⁡TmVR⁡T→f:mVR⁡T⟶mREx⁡T
16 15 adantl ⊢T∈V∧f∈mREx⁡TmVR⁡T→f:mVR⁡T⟶mREx⁡T
17 ssidd ⊢T∈V∧f∈mREx⁡TmVR⁡T→mVR⁡T⊆mVR⁡T
18 wrd0 ⊢∅∈WordmCN⁡T∪mVR⁡T
19 eqid ⊢mCN⁡T=mCN⁡T
20 19 5 6 mrexval ⊢T∈V→mREx⁡T=WordmCN⁡T∪mVR⁡T
21 20 adantr ⊢T∈V∧f∈mREx⁡TmVR⁡T→mREx⁡T=WordmCN⁡T∪mVR⁡T
22 18 21 eleqtrrid ⊢T∈V∧f∈mREx⁡TmVR⁡T→∅∈mREx⁡T
23 eqid ⊢freeMnd⁡mCN⁡T∪mVR⁡T=freeMnd⁡mCN⁡T∪mVR⁡T
24 19 5 6 1 23 mrsubval ⊢f:mVR⁡T⟶mREx⁡T∧mVR⁡T⊆mVR⁡T∧∅∈mREx⁡T→S⁡f⁡∅=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘∅
25 16 17 22 24 syl3anc ⊢T∈V∧f∈mREx⁡TmVR⁡T→S⁡f⁡∅=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘∅
26 co02 ⊢v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘∅=∅
27 26 oveq2i ⊢∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘∅=∑freeMnd⁡mCN⁡T∪mVR⁡T∅
28 23 frmd0 ⊢∅=0freeMnd⁡mCN⁡T∪mVR⁡T
29 28 gsum0 ⊢∑freeMnd⁡mCN⁡T∪mVR⁡T∅=∅
30 27 29 eqtri ⊢∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘∅=∅
31 25 30 eqtrdi ⊢T∈V∧f∈mREx⁡TmVR⁡T→S⁡f⁡∅=∅
32 fveq1 ⊢S⁡f=F→S⁡f⁡∅=F⁡∅
33 32 eqeq1d ⊢S⁡f=F→S⁡f⁡∅=∅↔F⁡∅=∅
34 31 33 syl5ibcom ⊢T∈V∧f∈mREx⁡TmVR⁡T→S⁡f=F→F⁡∅=∅
35 34 rexlimdva ⊢T∈V→∃f∈mREx⁡TmVR⁡TS⁡f=F→F⁡∅=∅
36 4 14 35 sylc ⊢F∈ran⁡S→F⁡∅=∅