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 34476
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 34456 . 2 class mRSubst
2 vt . . 3 setvar 𝑑
3 cvv 3474 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1540 . . . . . 6 class 𝑑
6 cmrex 34452 . . . . . 6 class mREx
75, 6cfv 6543 . . . . 5 class (mRExβ€˜π‘‘)
8 cmvar 34447 . . . . . 6 class mVR
95, 8cfv 6543 . . . . 5 class (mVRβ€˜π‘‘)
10 cpm 8820 . . . . 5 class ↑pm
117, 9, 10co 7408 . . . 4 class ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘))
12 ve . . . . 5 setvar 𝑒
13 cmcn 34446 . . . . . . . . 9 class mCN
145, 13cfv 6543 . . . . . . . 8 class (mCNβ€˜π‘‘)
1514, 9cun 3946 . . . . . . 7 class ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))
16 cfrmd 18727 . . . . . . 7 class freeMnd
1715, 16cfv 6543 . . . . . 6 class (freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)))
18 vv . . . . . . . 8 setvar 𝑣
1918cv 1540 . . . . . . . . . 10 class 𝑣
204cv 1540 . . . . . . . . . . 11 class 𝑓
2120cdm 5676 . . . . . . . . . 10 class dom 𝑓
2219, 21wcel 2106 . . . . . . . . 9 wff 𝑣 ∈ dom 𝑓
2319, 20cfv 6543 . . . . . . . . 9 class (π‘“β€˜π‘£)
2419cs1 14544 . . . . . . . . 9 class βŸ¨β€œπ‘£β€βŸ©
2522, 23, 24cif 4528 . . . . . . . 8 class if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)
2618, 15, 25cmpt 5231 . . . . . . 7 class (𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©))
2712cv 1540 . . . . . . 7 class 𝑒
2826, 27ccom 5680 . . . . . 6 class ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒)
29 cgsu 17385 . . . . . 6 class Ξ£g
3017, 28, 29co 7408 . . . . 5 class ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒))
3112, 7, 30cmpt 5231 . . . 4 class (𝑒 ∈ (mRExβ€˜π‘‘) ↦ ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒)))
324, 11, 31cmpt 5231 . . 3 class (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mRExβ€˜π‘‘) ↦ ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒))))
332, 3, 32cmpt 5231 . 2 class (𝑑 ∈ V ↦ (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mRExβ€˜π‘‘) ↦ ((freeMndβ€˜((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘))) Ξ£g ((𝑣 ∈ ((mCNβ€˜π‘‘) βˆͺ (mVRβ€˜π‘‘)) ↦ if(𝑣 ∈ dom 𝑓, (π‘“β€˜π‘£), βŸ¨β€œπ‘£β€βŸ©)) ∘ 𝑒)))))
341, 33wceq 1541 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  34493
  Copyright terms: Public domain W3C validator