Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mrsub Structured version   Visualization version   GIF version

Definition df-mrsub 31092
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
StepHypRef Expression
1 cmrsub 31072 . 2 class mRSubst
2 vt . . 3 setvar 𝑡
3 cvv 3186 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1479 . . . . . 6 class 𝑡
6 cmrex 31068 . . . . . 6 class mREx
75, 6cfv 5847 . . . . 5 class (mREx‘𝑡)
8 cmvar 31063 . . . . . 6 class mVR
95, 8cfv 5847 . . . . 5 class (mVR‘𝑡)
10 cpm 7803 . . . . 5 class pm
117, 9, 10co 6604 . . . 4 class ((mREx‘𝑡) ↑pm (mVR‘𝑡))
12 ve . . . . 5 setvar 𝑒
13 cmcn 31062 . . . . . . . . 9 class mCN
145, 13cfv 5847 . . . . . . . 8 class (mCN‘𝑡)
1514, 9cun 3553 . . . . . . 7 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
16 cfrmd 17305 . . . . . . 7 class freeMnd
1715, 16cfv 5847 . . . . . 6 class (freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡)))
18 vv . . . . . . . 8 setvar 𝑣
1918cv 1479 . . . . . . . . . 10 class 𝑣
204cv 1479 . . . . . . . . . . 11 class 𝑓
2120cdm 5074 . . . . . . . . . 10 class dom 𝑓
2219, 21wcel 1987 . . . . . . . . 9 wff 𝑣 ∈ dom 𝑓
2319, 20cfv 5847 . . . . . . . . 9 class (𝑓𝑣)
2419cs1 13233 . . . . . . . . 9 class ⟨“𝑣”⟩
2522, 23, 24cif 4058 . . . . . . . 8 class if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)
2618, 15, 25cmpt 4673 . . . . . . 7 class (𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩))
2712cv 1479 . . . . . . 7 class 𝑒
2826, 27ccom 5078 . . . . . 6 class ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)
29 cgsu 16022 . . . . . 6 class Σg
3017, 28, 29co 6604 . . . . 5 class ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))
3112, 7, 30cmpt 4673 . . . 4 class (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))
324, 11, 31cmpt 4673 . . 3 class (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
332, 3, 32cmpt 4673 . 2 class (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
341, 33wceq 1480 1 wff mRSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
Colors of variables: wff setvar class
This definition is referenced by:  mrsubffval  31109
  Copyright terms: Public domain W3C validator