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 32757
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 32737 . 2 class mRSubst
2 vt . . 3 setvar 𝑡
3 cvv 3479 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1537 . . . . . 6 class 𝑡
6 cmrex 32733 . . . . . 6 class mREx
75, 6cfv 6338 . . . . 5 class (mREx‘𝑡)
8 cmvar 32728 . . . . . 6 class mVR
95, 8cfv 6338 . . . . 5 class (mVR‘𝑡)
10 cpm 8392 . . . . 5 class pm
117, 9, 10co 7140 . . . 4 class ((mREx‘𝑡) ↑pm (mVR‘𝑡))
12 ve . . . . 5 setvar 𝑒
13 cmcn 32727 . . . . . . . . 9 class mCN
145, 13cfv 6338 . . . . . . . 8 class (mCN‘𝑡)
1514, 9cun 3916 . . . . . . 7 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
16 cfrmd 18003 . . . . . . 7 class freeMnd
1715, 16cfv 6338 . . . . . 6 class (freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡)))
18 vv . . . . . . . 8 setvar 𝑣
1918cv 1537 . . . . . . . . . 10 class 𝑣
204cv 1537 . . . . . . . . . . 11 class 𝑓
2120cdm 5538 . . . . . . . . . 10 class dom 𝑓
2219, 21wcel 2115 . . . . . . . . 9 wff 𝑣 ∈ dom 𝑓
2319, 20cfv 6338 . . . . . . . . 9 class (𝑓𝑣)
2419cs1 13940 . . . . . . . . 9 class ⟨“𝑣”⟩
2522, 23, 24cif 4448 . . . . . . . 8 class if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)
2618, 15, 25cmpt 5129 . . . . . . 7 class (𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩))
2712cv 1537 . . . . . . 7 class 𝑒
2826, 27ccom 5542 . . . . . 6 class ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)
29 cgsu 16705 . . . . . 6 class Σg
3017, 28, 29co 7140 . . . . 5 class ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))
3112, 7, 30cmpt 5129 . . . 4 class (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))
324, 11, 31cmpt 5129 . . 3 class (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
332, 3, 32cmpt 5129 . 2 class (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
341, 33wceq 1538 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  32774
  Copyright terms: Public domain W3C validator