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}=\mathrm{mVR}\left({T}\right)$
mrsubvr.r ${⊢}{R}=\mathrm{mREx}\left({T}\right)$
mrsubvr.s ${⊢}{S}=\mathrm{mRSubst}\left({T}\right)$
Assertion mrsubff ${⊢}{T}\in {W}\to {S}:{R}{↑}_{𝑝𝑚}{V}⟶{{R}}^{{R}}$

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 fvex ${⊢}\mathrm{mCN}\left({T}\right)\in \mathrm{V}$
5 1 fvexi ${⊢}{V}\in \mathrm{V}$
6 4 5 unex ${⊢}\mathrm{mCN}\left({T}\right)\cup {V}\in \mathrm{V}$
7 eqid ${⊢}\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)=\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
8 7 frmdmnd ${⊢}\mathrm{mCN}\left({T}\right)\cup {V}\in \mathrm{V}\to \mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\in \mathrm{Mnd}$
9 6 8 mp1i ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\to \mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\in \mathrm{Mnd}$
10 simpr ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\to {e}\in {R}$
11 eqid ${⊢}\mathrm{mCN}\left({T}\right)=\mathrm{mCN}\left({T}\right)$
12 11 1 2 mrexval ${⊢}{T}\in {W}\to {R}=\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
13 12 ad2antrr ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\to {R}=\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
14 10 13 eleqtrd ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\to {e}\in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
15 elpmi ${⊢}{f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\to \left({f}:\mathrm{dom}{f}⟶{R}\wedge \mathrm{dom}{f}\subseteq {V}\right)$
16 15 simpld ${⊢}{f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\to {f}:\mathrm{dom}{f}⟶{R}$
17 16 ad3antlr ${⊢}\left(\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\wedge {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\right)\to {f}:\mathrm{dom}{f}⟶{R}$
18 17 ffvelrnda ${⊢}\left(\left(\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\wedge {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\right)\wedge {v}\in \mathrm{dom}{f}\right)\to {f}\left({v}\right)\in {R}$
19 13 ad2antrr ${⊢}\left(\left(\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\wedge {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\right)\wedge {v}\in \mathrm{dom}{f}\right)\to {R}=\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
20 18 19 eleqtrd ${⊢}\left(\left(\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\wedge {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\right)\wedge {v}\in \mathrm{dom}{f}\right)\to {f}\left({v}\right)\in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
21 simplr ${⊢}\left(\left(\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\wedge {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\right)\wedge ¬{v}\in \mathrm{dom}{f}\right)\to {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
22 21 s1cld ${⊢}\left(\left(\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\wedge {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\right)\wedge ¬{v}\in \mathrm{dom}{f}\right)\to ⟨“{v}”⟩\in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
23 20 22 ifclda ${⊢}\left(\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\right)\wedge {v}\in \left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\right)\to if\left({v}\in \mathrm{dom}{f},{f}\left({v}\right),⟨“{v}”⟩\right)\in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
24 23 fmpttd ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\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):\mathrm{mCN}\left({T}\right)\cup {V}⟶\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
25 wrdco ${⊢}\left({e}\in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\wedge \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):\mathrm{mCN}\left({T}\right)\cup {V}⟶\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {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}\in \mathrm{Word}\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
26 14 24 25 syl2anc ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\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}\in \mathrm{Word}\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
27 eqid ${⊢}{\mathrm{Base}}_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)}$
28 7 27 frmdbas ${⊢}\mathrm{mCN}\left({T}\right)\cup {V}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)}=\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
29 6 28 ax-mp ${⊢}{\mathrm{Base}}_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)}=\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
30 29 eqcomi ${⊢}\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)={\mathrm{Base}}_{\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)}$
31 30 gsumwcl ${⊢}\left(\mathrm{freeMnd}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)\in \mathrm{Mnd}\wedge \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}\in \mathrm{Word}\mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {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)\in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
32 9 26 31 syl2anc ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\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)\in \mathrm{Word}\left(\mathrm{mCN}\left({T}\right)\cup {V}\right)$
33 32 13 eleqtrrd ${⊢}\left(\left({T}\in {W}\wedge {f}\in \left({R}{↑}_{𝑝𝑚}{V}\right)\right)\wedge {e}\in {R}\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)\in {R}$
34 33 fmpttd ${⊢}\left({T}\in {W}\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):{R}⟶{R}$
35 2 fvexi ${⊢}{R}\in \mathrm{V}$
36 35 35 elmap ${⊢}\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)\in \left({{R}}^{{R}}\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):{R}⟶{R}$
37 34 36 sylibr ${⊢}\left({T}\in {W}\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)\in \left({{R}}^{{R}}\right)$
38 37 fmpttd ${⊢}{T}\in {W}\to \left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\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)\right):{R}{↑}_{𝑝𝑚}{V}⟶{{R}}^{{R}}$
39 11 1 2 3 7 mrsubffval ${⊢}{T}\in {W}\to {S}=\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\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)\right)$
40 39 feq1d ${⊢}{T}\in {W}\to \left({S}:{R}{↑}_{𝑝𝑚}{V}⟶{{R}}^{{R}}↔\left({f}\in \left({R}{↑}_{𝑝𝑚}{V}\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)\right):{R}{↑}_{𝑝𝑚}{V}⟶{{R}}^{{R}}\right)$
41 38 40 mpbird ${⊢}{T}\in {W}\to {S}:{R}{↑}_{𝑝𝑚}{V}⟶{{R}}^{{R}}$