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 32634
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 32614 . 2 class mRSubst
2 vt . . 3 setvar 𝑡
3 cvv 3492 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1527 . . . . . 6 class 𝑡
6 cmrex 32610 . . . . . 6 class mREx
75, 6cfv 6348 . . . . 5 class (mREx‘𝑡)
8 cmvar 32605 . . . . . 6 class mVR
95, 8cfv 6348 . . . . 5 class (mVR‘𝑡)
10 cpm 8396 . . . . 5 class pm
117, 9, 10co 7145 . . . 4 class ((mREx‘𝑡) ↑pm (mVR‘𝑡))
12 ve . . . . 5 setvar 𝑒
13 cmcn 32604 . . . . . . . . 9 class mCN
145, 13cfv 6348 . . . . . . . 8 class (mCN‘𝑡)
1514, 9cun 3931 . . . . . . 7 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
16 cfrmd 18000 . . . . . . 7 class freeMnd
1715, 16cfv 6348 . . . . . 6 class (freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡)))
18 vv . . . . . . . 8 setvar 𝑣
1918cv 1527 . . . . . . . . . 10 class 𝑣
204cv 1527 . . . . . . . . . . 11 class 𝑓
2120cdm 5548 . . . . . . . . . 10 class dom 𝑓
2219, 21wcel 2105 . . . . . . . . 9 wff 𝑣 ∈ dom 𝑓
2319, 20cfv 6348 . . . . . . . . 9 class (𝑓𝑣)
2419cs1 13937 . . . . . . . . 9 class ⟨“𝑣”⟩
2522, 23, 24cif 4463 . . . . . . . 8 class if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)
2618, 15, 25cmpt 5137 . . . . . . 7 class (𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩))
2712cv 1527 . . . . . . 7 class 𝑒
2826, 27ccom 5552 . . . . . 6 class ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)
29 cgsu 16702 . . . . . 6 class Σg
3017, 28, 29co 7145 . . . . 5 class ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))
3112, 7, 30cmpt 5137 . . . 4 class (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))
324, 11, 31cmpt 5137 . . 3 class (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
332, 3, 32cmpt 5137 . 2 class (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
341, 33wceq 1528 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  32651
  Copyright terms: Public domain W3C validator