Definition df-msub 30642

Description: Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-msub	⊢ mSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))⟩)))

Distinct variable group:   𝑒,𝑓,𝑡

Detailed syntax breakdown of Definition df-msub

Step	Hyp	Ref	Expression
1		cmsub 30622	. 2 class mSubst
2		vt	. . 3 setvar 𝑡
3		cvv 3173	. . 3 class V
4		vf	. . . 4 setvar 𝑓
5	2	cv 1474	. . . . . 6 class 𝑡
6		cmrex 30617	. . . . . 6 class mREx
7	5, 6	cfv 5804	. . . . 5 class (mREx‘𝑡)
8		cmvar 30612	. . . . . 6 class mVR
9	5, 8	cfv 5804	. . . . 5 class (mVR‘𝑡)
10		cpm 7745	. . . . 5 class ↑pm
11	7, 9, 10	co 6549	. . . 4 class ((mREx‘𝑡) ↑pm (mVR‘𝑡))
12		ve	. . . . 5 setvar 𝑒
13		cmex 30618	. . . . . 6 class mEx
14	5, 13	cfv 5804	. . . . 5 class (mEx‘𝑡)
15	12	cv 1474	. . . . . . 7 class 𝑒
16		c1st 7057	. . . . . . 7 class 1st
17	15, 16	cfv 5804	. . . . . 6 class (1st ‘𝑒)
18		c2nd 7058	. . . . . . . 8 class 2nd
19	15, 18	cfv 5804	. . . . . . 7 class (2nd ‘𝑒)
20	4	cv 1474	. . . . . . . 8 class 𝑓
21		cmrsub 30621	. . . . . . . . 9 class mRSubst
22	5, 21	cfv 5804	. . . . . . . 8 class (mRSubst‘𝑡)
23	20, 22	cfv 5804	. . . . . . 7 class ((mRSubst‘𝑡)‘𝑓)
24	19, 23	cfv 5804	. . . . . 6 class (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))
25	17, 24	cop 4131	. . . . 5 class ⟨(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))⟩
26	12, 14, 25	cmpt 4643	. . . 4 class (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))⟩)
27	4, 11, 26	cmpt 4643	. . 3 class (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))⟩))
28	2, 3, 27	cmpt 4643	. 2 class (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))⟩)))
29	1, 28	wceq 1475	1 wff mSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))⟩)))

This definition is referenced by:  msubffval  30674