Definition df-mvsb 35562

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

Step	Hyp	Ref	Expression
1		cmvsb 35549	. 2 class mVSubst
2		vt	. . 3 setvar 𝑡
3		cvv 3464	. . 3 class V
4		vs	. . . . . . . 8 setvar 𝑠
5	4	cv 1538	. . . . . . 7 class 𝑠
6	2	cv 1538	. . . . . . . . 9 class 𝑡
7		cmsub 35413	. . . . . . . . 9 class mSubst
8	6, 7	cfv 6542	. . . . . . . 8 class (mSubst‘𝑡)
9	8	crn 5668	. . . . . . 7 class ran (mSubst‘𝑡)
10	5, 9	wcel 2107	. . . . . 6 wff 𝑠 ∈ ran (mSubst‘𝑡)
11		vm	. . . . . . . 8 setvar 𝑚
12	11	cv 1538	. . . . . . 7 class 𝑚
13		cmvl 35548	. . . . . . . 8 class mVL
14	6, 13	cfv 6542	. . . . . . 7 class (mVL‘𝑡)
15	12, 14	wcel 2107	. . . . . 6 wff 𝑚 ∈ (mVL‘𝑡)
16	10, 15	wa 395	. . . . 5 wff (𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡))
17		vv	. . . . . . . . . 10 setvar 𝑣
18	17	cv 1538	. . . . . . . . 9 class 𝑣
19		cmvh 35414	. . . . . . . . . 10 class mVH
20	6, 19	cfv 6542	. . . . . . . . 9 class (mVH‘𝑡)
21	18, 20	cfv 6542	. . . . . . . 8 class ((mVH‘𝑡)‘𝑣)
22	21, 5	cfv 6542	. . . . . . 7 class (𝑠‘((mVH‘𝑡)‘𝑣))
23		cmevl 35552	. . . . . . . . 9 class mEval
24	6, 23	cfv 6542	. . . . . . . 8 class (mEval‘𝑡)
25	24	cdm 5667	. . . . . . 7 class dom (mEval‘𝑡)
26	12, 22, 25	wbr 5125	. . . . . 6 wff 𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))
27		cmvar 35403	. . . . . . 7 class mVR
28	6, 27	cfv 6542	. . . . . 6 class (mVR‘𝑡)
29	26, 17, 28	wral 3050	. . . . 5 wff ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))
30		vx	. . . . . . 7 setvar 𝑥
31	30	cv 1538	. . . . . 6 class 𝑥
32	12, 22, 24	co 7414	. . . . . . 7 class (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))
33	17, 28, 32	cmpt 5207	. . . . . 6 class (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))))
34	31, 33	wceq 1539	. . . . 5 wff 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣))))
35	16, 29, 34	w3a 1086	. . . 4 wff ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))
36	35, 4, 11, 30	coprab 7415	. . 3 class {⟨⟨𝑠, 𝑚⟩, 𝑥⟩ ∣ ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))}
37	2, 3, 36	cmpt 5207	. 2 class (𝑡 ∈ V ↦ {⟨⟨𝑠, 𝑚⟩, 𝑥⟩ ∣ ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))})
38	1, 37	wceq 1539	1 wff mVSubst = (𝑡 ∈ V ↦ {⟨⟨𝑠, 𝑚⟩, 𝑥⟩ ∣ ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))})

This definition is referenced by: (None)