Metamath Proof Explorer

Theorem mrsubff

Description: A substitution is a function from R to R . (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 mrsubff ⊢T∈W→S:R↑𝑝𝑚V⟶RR

Proof

Step Hyp Ref Expression
1 mrsubvr.v ⊢V=mVR⁡T
2 mrsubvr.r ⊢R=mREx⁡T
3 mrsubvr.s ⊢S=mRSubst⁡T
4 fvex ⊢mCN⁡T∈V
5 1 fvexi ⊢V∈V
6 4 5 unex ⊢mCN⁡T∪V∈V
7 eqid ⊢freeMnd⁡mCN⁡T∪V=freeMnd⁡mCN⁡T∪V
8 7 frmdmnd ⊢mCN⁡T∪V∈V→freeMnd⁡mCN⁡T∪V∈Mnd
9 6 8 mp1i ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→freeMnd⁡mCN⁡T∪V∈Mnd
10 simpr ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→e∈R
11 eqid ⊢mCN⁡T=mCN⁡T
12 11 1 2 mrexval ⊢T∈W→R=WordmCN⁡T∪V
13 12 ad2antrr ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→R=WordmCN⁡T∪V
14 10 13 eleqtrd ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→e∈WordmCN⁡T∪V
15 elpmi ⊢f∈R↑𝑝𝑚V→f:dom⁡f⟶R∧dom⁡f⊆V
16 15 simpld ⊢f∈R↑𝑝𝑚V→f:dom⁡f⟶R
17 16 ad3antlr ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R∧v∈mCN⁡T∪V→f:dom⁡f⟶R
18 17 ffvelcdmda ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R∧v∈mCN⁡T∪V∧v∈dom⁡f→f⁡v∈R
19 13 ad2antrr ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R∧v∈mCN⁡T∪V∧v∈dom⁡f→R=WordmCN⁡T∪V
20 18 19 eleqtrd ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R∧v∈mCN⁡T∪V∧v∈dom⁡f→f⁡v∈WordmCN⁡T∪V
21 simplr ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R∧v∈mCN⁡T∪V∧¬v∈dom⁡f→v∈mCN⁡T∪V
22 21 s1cld ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R∧v∈mCN⁡T∪V∧¬v∈dom⁡f→⟨“v”⟩∈WordmCN⁡T∪V
23 20 22 ifclda ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R∧v∈mCN⁡T∪V→ifv∈dom⁡ff⁡v⟨“v”⟩∈WordmCN⁡T∪V
24 23 fmpttd ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→v∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩:mCN⁡T∪V⟶WordmCN⁡T∪V
25 wrdco ⊢e∈WordmCN⁡T∪V∧v∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩:mCN⁡T∪V⟶WordmCN⁡T∪V→v∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈WordWordmCN⁡T∪V
26 14 24 25 syl2anc ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→v∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈WordWordmCN⁡T∪V
27 eqid ⊢BasefreeMnd⁡mCN⁡T∪V=BasefreeMnd⁡mCN⁡T∪V
28 7 27 frmdbas ⊢mCN⁡T∪V∈V→BasefreeMnd⁡mCN⁡T∪V=WordmCN⁡T∪V
29 6 28 ax-mp ⊢BasefreeMnd⁡mCN⁡T∪V=WordmCN⁡T∪V
30 29 eqcomi ⊢WordmCN⁡T∪V=BasefreeMnd⁡mCN⁡T∪V
31 30 gsumwcl ⊢freeMnd⁡mCN⁡T∪V∈Mnd∧v∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈WordWordmCN⁡T∪V→∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈WordmCN⁡T∪V
32 9 26 31 syl2anc ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈WordmCN⁡T∪V
33 32 13 eleqtrrd ⊢T∈W∧f∈R↑𝑝𝑚V∧e∈R→∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈R
34 33 fmpttd ⊢T∈W∧f∈R↑𝑝𝑚V→e∈R⟼∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e:R⟶R
35 2 fvexi ⊢R∈V
36 35 35 elmap ⊢e∈R⟼∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈RR↔e∈R⟼∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e:R⟶R
37 34 36 sylibr ⊢T∈W∧f∈R↑𝑝𝑚V→e∈R⟼∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈RR
38 37 fmpttd ⊢T∈W→f∈R↑𝑝𝑚V⟼e∈R⟼∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e:R↑𝑝𝑚V⟶RR
39 11 1 2 3 7 mrsubffval ⊢T∈W→S=f∈R↑𝑝𝑚V⟼e∈R⟼∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
40 39 feq1d ⊢T∈W→S:R↑𝑝𝑚V⟶RR↔f∈R↑𝑝𝑚V⟼e∈R⟼∑freeMnd⁡mCN⁡T∪Vv∈mCN⁡T∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e:R↑𝑝𝑚V⟶RR
41 38 40 mpbird ⊢T∈W→S:R↑𝑝𝑚V⟶RR