Definition df-mvsb 31515

Description: Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-mvsb	|- mVSubst = ( t e. _V |-> { <. <. s , m >. , x >. | ( ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) ) /\ A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) /\ x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) ) ) } )

Distinct variable group:   m, s, t, v, x

Detailed syntax breakdown of Definition df-mvsb

Step	Hyp	Ref	Expression
1		cmvsb 31502	. 2 class mVSubst
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vs	. . . . . . . 8 setvar s
5	4	cv 1482	. . . . . . 7 class s
6	2	cv 1482	. . . . . . . . 9 class t
7		cmsub 31368	. . . . . . . . 9 class mSubst
8	6, 7	cfv 5888	. . . . . . . 8 class (mSubst ` t )
9	8	crn 5115	. . . . . . 7 class ran (mSubst ` t )
10	5, 9	wcel 1990	. . . . . 6 wff s e. ran (mSubst ` t )
11		vm	. . . . . . . 8 setvar m
12	11	cv 1482	. . . . . . 7 class m
13		cmvl 31501	. . . . . . . 8 class mVL
14	6, 13	cfv 5888	. . . . . . 7 class (mVL ` t )
15	12, 14	wcel 1990	. . . . . 6 wff m e. (mVL ` t )
16	10, 15	wa 384	. . . . 5 wff ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) )
17		vv	. . . . . . . . . 10 setvar v
18	17	cv 1482	. . . . . . . . 9 class v
19		cmvh 31369	. . . . . . . . . 10 class mVH
20	6, 19	cfv 5888	. . . . . . . . 9 class (mVH ` t )
21	18, 20	cfv 5888	. . . . . . . 8 class ( (mVH ` t ) ` v )
22	21, 5	cfv 5888	. . . . . . 7 class ( s ` ( (mVH ` t ) ` v ) )
23		cmevl 31505	. . . . . . . . 9 class mEval
24	6, 23	cfv 5888	. . . . . . . 8 class (mEval ` t )
25	24	cdm 5114	. . . . . . 7 class dom (mEval ` t )
26	12, 22, 25	wbr 4653	. . . . . 6 wff m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) )
27		cmvar 31358	. . . . . . 7 class mVR
28	6, 27	cfv 5888	. . . . . 6 class (mVR ` t )
29	26, 17, 28	wral 2912	. . . . 5 wff A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) )
30		vx	. . . . . . 7 setvar x
31	30	cv 1482	. . . . . 6 class x
32	12, 22, 24	co 6650	. . . . . . 7 class ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) )
33	17, 28, 32	cmpt 4729	. . . . . 6 class ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) )
34	31, 33	wceq 1483	. . . . 5 wff x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) )
35	16, 29, 34	w3a 1037	. . . 4 wff ( ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) ) /\ A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) /\ x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) ) )
36	35, 4, 11, 30	coprab 6651	. . 3 class { <. <. s , m >. , x >. | ( ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) ) /\ A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) /\ x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) ) ) }
37	2, 3, 36	cmpt 4729	. 2 class ( t e. _V |-> { <. <. s , m >. , x >. | ( ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) ) /\ A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) /\ x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) ) ) } )
38	1, 37	wceq 1483	1 wff mVSubst = ( t e. _V |-> { <. <. s , m >. , x >. | ( ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) ) /\ A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) /\ x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) ) ) } )

This definition is referenced by: (None)