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 33098
 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 33085 . 2 class mVSubst
2 vt . . 3 setvar 𝑡
3 cvv 3409 . . 3 class V
4 vs . . . . . . . 8 setvar 𝑠
54cv 1537 . . . . . . 7 class 𝑠
62cv 1537 . . . . . . . . 9 class 𝑡
7 cmsub 32949 . . . . . . . . 9 class mSubst
86, 7cfv 6335 . . . . . . . 8 class (mSubst‘𝑡)
98crn 5525 . . . . . . 7 class ran (mSubst‘𝑡)
105, 9wcel 2111 . . . . . 6 wff 𝑠 ∈ ran (mSubst‘𝑡)
11 vm . . . . . . . 8 setvar 𝑚
1211cv 1537 . . . . . . 7 class 𝑚
13 cmvl 33084 . . . . . . . 8 class mVL
146, 13cfv 6335 . . . . . . 7 class (mVL‘𝑡)
1512, 14wcel 2111 . . . . . 6 wff 𝑚 ∈ (mVL‘𝑡)
1610, 15wa 399 . . . . 5 wff (𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡))
17 vv . . . . . . . . . 10 setvar 𝑣
1817cv 1537 . . . . . . . . 9 class 𝑣
19 cmvh 32950 . . . . . . . . . 10 class mVH
206, 19cfv 6335 . . . . . . . . 9 class (mVH‘𝑡)
2118, 20cfv 6335 . . . . . . . 8 class ((mVH‘𝑡)‘𝑣)
2221, 5cfv 6335 . . . . . . 7 class (𝑠‘((mVH‘𝑡)‘𝑣))
23 cmevl 33088 . . . . . . . . 9 class mEval
246, 23cfv 6335 . . . . . . . 8 class (mEval‘𝑡)
2524cdm 5524 . . . . . . 7 class dom (mEval‘𝑡)
2612, 22, 25wbr 5032 . . . . . 6 wff 𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))
27 cmvar 32939 . . . . . . 7 class mVR
286, 27cfv 6335 . . . . . 6 class (mVR‘𝑡)
2926, 17, 28wral 3070 . . . . 5 wff 𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))
30 vx . . . . . . 7 setvar 𝑥
3130cv 1537 . . . . . 6 class 𝑥
3212, 22, 24co 7150 . . . . . . 7 class (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))
3317, 28, 32cmpt 5112 . . . . . 6 class (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))))
3431, 33wceq 1538 . . . . 5 wff 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))))
3516, 29, 34w3a 1084 . . . 4 wff ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))
3635, 4, 11, 30coprab 7151 . . 3 class {⟨⟨𝑠, 𝑚⟩, 𝑥⟩ ∣ ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))}
372, 3, 36cmpt 5112 . 2 class (𝑡 ∈ V ↦ {⟨⟨𝑠, 𝑚⟩, 𝑥⟩ ∣ ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))})
381, 37wceq 1538 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