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 34148
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 34128 . 2 class mRSubst
2 vt . . 3 setvar 𝑑
3 cvv 3447 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1541 . . . . . 6 class 𝑑
6 cmrex 34124 . . . . . 6 class mREx
75, 6cfv 6500 . . . . 5 class (mRExβ€˜π‘‘)
8 cmvar 34119 . . . . . 6 class mVR
95, 8cfv 6500 . . . . 5 class (mVRβ€˜π‘‘)
10 cpm 8772 . . . . 5 class ↑pm
117, 9, 10co 7361 . . . 4 class ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘))
12 ve . . . . 5 setvar 𝑒
13 cmcn 34118 . . . . . . . . 9 class mCN
145, 13cfv 6500 . . . . . . . 8 class (mCNβ€˜π‘‘)
1514, 9cun 3912 . . . . . . 7 class ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))
16 cfrmd 18665 . . . . . . 7 class freeMnd
1715, 16cfv 6500 . . . . . 6 class (freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)))
18 vv . . . . . . . 8 setvar 𝑣
1918cv 1541 . . . . . . . . . 10 class 𝑣
204cv 1541 . . . . . . . . . . 11 class 𝑓
2120cdm 5637 . . . . . . . . . 10 class dom 𝑓
2219, 21wcel 2107 . . . . . . . . 9 wff 𝑣 ∈ dom 𝑓
2319, 20cfv 6500 . . . . . . . . 9 class (π‘“β€˜π‘£)
2419cs1 14492 . . . . . . . . 9 class βŸ¨β€œπ‘£β€βŸ©
2522, 23, 24cif 4490 . . . . . . . 8 class if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)
2618, 15, 25cmpt 5192 . . . . . . 7 class (𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©))
2712cv 1541 . . . . . . 7 class 𝑒
2826, 27ccom 5641 . . . . . 6 class ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒)
29 cgsu 17330 . . . . . 6 class Ξ£g
3017, 28, 29co 7361 . . . . 5 class ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒))
3112, 7, 30cmpt 5192 . . . 4 class (𝑒 ∈ (mRExβ€˜π‘‘) ↦ ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒)))
324, 11, 31cmpt 5192 . . 3 class (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mRExβ€˜π‘‘) ↦ ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒))))
332, 3, 32cmpt 5192 . 2 class (𝑑 ∈ V ↦ (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mRExβ€˜π‘‘) ↦ ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒)))))
341, 33wceq 1542 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  34165
  Copyright terms: Public domain W3C validator