Definition df-mrsub 35495

Description: Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-mrsub	⊢ mRSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))

Distinct variable group:   𝑒,𝑓,𝑡,𝑣

Detailed syntax breakdown of Definition df-mrsub

Step	Hyp	Ref	Expression
1		cmrsub 35475	. 2 class mRSubst
2		vt	. . 3 setvar 𝑡
3		cvv 3480	. . 3 class V
4		vf	. . . 4 setvar 𝑓
5	2	cv 1539	. . . . . 6 class 𝑡
6		cmrex 35471	. . . . . 6 class mREx
7	5, 6	cfv 6561	. . . . 5 class (mREx‘𝑡)
8		cmvar 35466	. . . . . 6 class mVR
9	5, 8	cfv 6561	. . . . 5 class (mVR‘𝑡)
10		cpm 8867	. . . . 5 class ↑pm
11	7, 9, 10	co 7431	. . . 4 class ((mREx‘𝑡) ↑pm (mVR‘𝑡))
12		ve	. . . . 5 setvar 𝑒
13		cmcn 35465	. . . . . . . . 9 class mCN
14	5, 13	cfv 6561	. . . . . . . 8 class (mCN‘𝑡)
15	14, 9	cun 3949	. . . . . . 7 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
16		cfrmd 18860	. . . . . . 7 class freeMnd
17	15, 16	cfv 6561	. . . . . 6 class (freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡)))
18		vv	. . . . . . . 8 setvar 𝑣
19	18	cv 1539	. . . . . . . . . 10 class 𝑣
20	4	cv 1539	. . . . . . . . . . 11 class 𝑓
21	20	cdm 5685	. . . . . . . . . 10 class dom 𝑓
22	19, 21	wcel 2108	. . . . . . . . 9 wff 𝑣 ∈ dom 𝑓
23	19, 20	cfv 6561	. . . . . . . . 9 class (𝑓‘𝑣)
24	19	cs1 14633	. . . . . . . . 9 class ⟨“𝑣”⟩
25	22, 23, 24	cif 4525	. . . . . . . 8 class if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)
26	18, 15, 25	cmpt 5225	. . . . . . 7 class (𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩))
27	12	cv 1539	. . . . . . 7 class 𝑒
28	26, 27	ccom 5689	. . . . . 6 class ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)
29		cgsu 17485	. . . . . 6 class Σg
30	17, 28, 29	co 7431	. . . . 5 class ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))
31	12, 7, 30	cmpt 5225	. . . 4 class (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))
32	4, 11, 31	cmpt 5225	. . 3 class (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
33	2, 3, 32	cmpt 5225	. 2 class (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
34	1, 33	wceq 1540	1 wff mRSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))

This definition is referenced by:  mrsubffval  35512