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 ⟶ R R

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 = Word mCN ⁡ T ∪ V
13 12 ad2antrr ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R → R = Word mCN ⁡ T ∪ V
14 10 13 eleqtrd ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R → e ∈ Word mCN ⁡ 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 ffvelrnda ⊢ 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 = Word mCN ⁡ T ∪ V
20 18 19 eleqtrd ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R ∧ v ∈ mCN ⁡ T ∪ V ∧ v ∈ dom ⁡ f → f ⁡ v ∈ Word mCN ⁡ 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 ”⟩ ∈ Word mCN ⁡ T ∪ V
23 20 22 ifclda ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R ∧ v ∈ mCN ⁡ T ∪ V → if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∈ Word mCN ⁡ T ∪ V
24 23 fmpttd ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R → v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ : mCN ⁡ T ∪ V ⟶ Word mCN ⁡ T ∪ V
25 wrdco ⊢ e ∈ Word mCN ⁡ T ∪ V ∧ v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ : mCN ⁡ T ∪ V ⟶ Word mCN ⁡ T ∪ V → v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ Word Word mCN ⁡ T ∪ V
26 14 24 25 syl2anc ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R → v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ Word Word mCN ⁡ T ∪ V
27 eqid ⊢ Base freeMnd ⁡ mCN ⁡ T ∪ V = Base freeMnd ⁡ mCN ⁡ T ∪ V
28 7 27 frmdbas ⊢ mCN ⁡ T ∪ V ∈ V → Base freeMnd ⁡ mCN ⁡ T ∪ V = Word mCN ⁡ T ∪ V
29 6 28 ax-mp ⊢ Base freeMnd ⁡ mCN ⁡ T ∪ V = Word mCN ⁡ T ∪ V
30 29 eqcomi ⊢ Word mCN ⁡ T ∪ V = Base freeMnd ⁡ mCN ⁡ T ∪ V
31 30 gsumwcl ⊢ freeMnd ⁡ mCN ⁡ T ∪ V ∈ Mnd ∧ v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ Word Word mCN ⁡ T ∪ V → ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ Word mCN ⁡ T ∪ V
32 9 26 31 syl2anc ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ Word mCN ⁡ T ∪ V
33 32 13 eleqtrrd ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ R
34 33 fmpttd ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V → e ∈ R ⟼ ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e : R ⟶ R
35 2 fvexi ⊢ R ∈ V
36 35 35 elmap ⊢ e ∈ R ⟼ ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ R R ↔ e ∈ R ⟼ ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e : R ⟶ R
37 34 36 sylibr ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V → e ∈ R ⟼ ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ R R
38 37 fmpttd ⊢ T ∈ W → f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e : R ↑ 𝑝𝑚 V ⟶ R R
39 11 1 2 3 7 mrsubffval ⊢ T ∈ W → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
40 39 feq1d ⊢ T ∈ W → S : R ↑ 𝑝𝑚 V ⟶ R R ↔ f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ freeMnd ⁡ mCN ⁡ T ∪ V v ∈ mCN ⁡ T ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e : R ↑ 𝑝𝑚 V ⟶ R R
41 38 40 mpbird ⊢ T ∈ W → S : R ↑ 𝑝𝑚 V ⟶ R R