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

Definition df-mvsb 33881
Description: Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mvsb mVSubst = (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘ , π‘šβŸ©, π‘₯⟩ ∣ ((𝑠 ∈ ran (mSubstβ€˜π‘‘) ∧ π‘š ∈ (mVLβ€˜π‘‘)) ∧ βˆ€π‘£ ∈ (mVRβ€˜π‘‘)π‘šdom (mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)) ∧ π‘₯ = (𝑣 ∈ (mVRβ€˜π‘‘) ↦ (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)))))})
Distinct variable group:   π‘š,𝑠,𝑑,𝑣,π‘₯

Detailed syntax breakdown of Definition df-mvsb
StepHypRef Expression
1 cmvsb 33868 . 2 class mVSubst
2 vt . . 3 setvar 𝑑
3 cvv 3441 . . 3 class V
4 vs . . . . . . . 8 setvar 𝑠
54cv 1539 . . . . . . 7 class 𝑠
62cv 1539 . . . . . . . . 9 class 𝑑
7 cmsub 33732 . . . . . . . . 9 class mSubst
86, 7cfv 6479 . . . . . . . 8 class (mSubstβ€˜π‘‘)
98crn 5621 . . . . . . 7 class ran (mSubstβ€˜π‘‘)
105, 9wcel 2105 . . . . . 6 wff 𝑠 ∈ ran (mSubstβ€˜π‘‘)
11 vm . . . . . . . 8 setvar π‘š
1211cv 1539 . . . . . . 7 class π‘š
13 cmvl 33867 . . . . . . . 8 class mVL
146, 13cfv 6479 . . . . . . 7 class (mVLβ€˜π‘‘)
1512, 14wcel 2105 . . . . . 6 wff π‘š ∈ (mVLβ€˜π‘‘)
1610, 15wa 396 . . . . 5 wff (𝑠 ∈ ran (mSubstβ€˜π‘‘) ∧ π‘š ∈ (mVLβ€˜π‘‘))
17 vv . . . . . . . . . 10 setvar 𝑣
1817cv 1539 . . . . . . . . 9 class 𝑣
19 cmvh 33733 . . . . . . . . . 10 class mVH
206, 19cfv 6479 . . . . . . . . 9 class (mVHβ€˜π‘‘)
2118, 20cfv 6479 . . . . . . . 8 class ((mVHβ€˜π‘‘)β€˜π‘£)
2221, 5cfv 6479 . . . . . . 7 class (π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£))
23 cmevl 33871 . . . . . . . . 9 class mEval
246, 23cfv 6479 . . . . . . . 8 class (mEvalβ€˜π‘‘)
2524cdm 5620 . . . . . . 7 class dom (mEvalβ€˜π‘‘)
2612, 22, 25wbr 5092 . . . . . 6 wff π‘šdom (mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£))
27 cmvar 33722 . . . . . . 7 class mVR
286, 27cfv 6479 . . . . . 6 class (mVRβ€˜π‘‘)
2926, 17, 28wral 3061 . . . . 5 wff βˆ€π‘£ ∈ (mVRβ€˜π‘‘)π‘šdom (mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£))
30 vx . . . . . . 7 setvar π‘₯
3130cv 1539 . . . . . 6 class π‘₯
3212, 22, 24co 7337 . . . . . . 7 class (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)))
3317, 28, 32cmpt 5175 . . . . . 6 class (𝑣 ∈ (mVRβ€˜π‘‘) ↦ (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£))))
3431, 33wceq 1540 . . . . 5 wff π‘₯ = (𝑣 ∈ (mVRβ€˜π‘‘) ↦ (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£))))
3516, 29, 34w3a 1086 . . . 4 wff ((𝑠 ∈ ran (mSubstβ€˜π‘‘) ∧ π‘š ∈ (mVLβ€˜π‘‘)) ∧ βˆ€π‘£ ∈ (mVRβ€˜π‘‘)π‘šdom (mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)) ∧ π‘₯ = (𝑣 ∈ (mVRβ€˜π‘‘) ↦ (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)))))
3635, 4, 11, 30coprab 7338 . . 3 class {βŸ¨βŸ¨π‘ , π‘šβŸ©, π‘₯⟩ ∣ ((𝑠 ∈ ran (mSubstβ€˜π‘‘) ∧ π‘š ∈ (mVLβ€˜π‘‘)) ∧ βˆ€π‘£ ∈ (mVRβ€˜π‘‘)π‘šdom (mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)) ∧ π‘₯ = (𝑣 ∈ (mVRβ€˜π‘‘) ↦ (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)))))}
372, 3, 36cmpt 5175 . 2 class (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘ , π‘šβŸ©, π‘₯⟩ ∣ ((𝑠 ∈ ran (mSubstβ€˜π‘‘) ∧ π‘š ∈ (mVLβ€˜π‘‘)) ∧ βˆ€π‘£ ∈ (mVRβ€˜π‘‘)π‘šdom (mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)) ∧ π‘₯ = (𝑣 ∈ (mVRβ€˜π‘‘) ↦ (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)))))})
381, 37wceq 1540 1 wff mVSubst = (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘ , π‘šβŸ©, π‘₯⟩ ∣ ((𝑠 ∈ ran (mSubstβ€˜π‘‘) ∧ π‘š ∈ (mVLβ€˜π‘‘)) ∧ βˆ€π‘£ ∈ (mVRβ€˜π‘‘)π‘šdom (mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)) ∧ π‘₯ = (𝑣 ∈ (mVRβ€˜π‘‘) ↦ (π‘š(mEvalβ€˜π‘‘)(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘£)))))})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator