Metamath Proof Explorer

Definition df-mvsb

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

Ref Expression
Assertion 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 ) ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvsb 
 |-  mVSubst
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vs 
 |-  s
4 vm 
 |-  m
5 vx 
 |-  x
6 3 cv 
 |-  s
7 cmsub 
 |-  mSubst
8 1 cv 
 |-  t
9 8 7 cfv 
 |-  ( mSubst ` t )
10 9 crn 
 |-  ran ( mSubst ` t )
11 6 10 wcel 
 |-  s e. ran ( mSubst ` t )
12 4 cv 
 |-  m
13 cmvl 
 |-  mVL
14 8 13 cfv 
 |-  ( mVL ` t )
15 12 14 wcel 
 |-  m e. ( mVL ` t )
16 11 15 wa 
 |-  ( s e. ran ( mSubst ` t ) /\ m e. ( mVL ` t ) )
17 vv 
 |-  v
18 cmvar 
 |-  mVR
19 8 18 cfv 
 |-  ( mVR ` t )
20 cmevl 
 |-  mEval
21 8 20 cfv 
 |-  ( mEval ` t )
22 21 cdm 
 |-  dom ( mEval ` t )
23 cmvh 
 |-  mVH
24 8 23 cfv 
 |-  ( mVH ` t )
25 17 cv 
 |-  v
26 25 24 cfv 
 |-  ( ( mVH ` t ) ` v )
27 26 6 cfv 
 |-  ( s ` ( ( mVH ` t ) ` v ) )
28 12 27 22 wbr 
 |-  m dom ( mEval ` t ) ( s ` ( ( mVH ` t ) ` v ) )
29 28 17 19 wral 
 |-  A. v e. ( mVR ` t ) m dom ( mEval ` t ) ( s ` ( ( mVH ` t ) ` v ) )
30 5 cv 
 |-  x
31 12 27 21 co 
 |-  ( m ( mEval ` t ) ( s ` ( ( mVH ` t ) ` v ) ) )
32 17 19 31 cmpt 
 |-  ( v e. ( mVR ` t ) |-> ( m ( mEval ` t ) ( s ` ( ( mVH ` t ) ` v ) ) ) )
33 30 32 wceq 
 |-  x = ( v e. ( mVR ` t ) |-> ( m ( mEval ` t ) ( s ` ( ( mVH ` t ) ` v ) ) ) )
34 16 29 33 w3a 
 |-  ( ( 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 ) ) ) ) )
35 34 3 4 5 coprab 
 |-  { <. <. 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 ) ) ) ) ) }
36 1 2 35 cmpt 
 |-  ( 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 ) ) ) ) ) } )
37 0 36 wceq 
 |-  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 ) ) ) ) ) } )