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 = ( 𝑡 ∈ V ↦ { ⟨ ⟨ 𝑠 , 𝑚 ⟩ , 𝑥 ⟩ ∣ ( ( 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ∧ 𝑚 ∈ ( mVL ‘ 𝑡 ) ) ∧ ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) 𝑚 dom ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ∧ 𝑥 = ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvsb ⊢ mVSubst
1 vt ⊢ 𝑡
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 vm ⊢ 𝑚
5 vx ⊢ 𝑥
6 3 cv ⊢ 𝑠
7 cmsub ⊢ mSubst
8 1 cv ⊢ 𝑡
9 8 7 cfv ⊢ ( mSubst ‘ 𝑡 )
10 9 crn ⊢ ran ( mSubst ‘ 𝑡 )
11 6 10 wcel ⊢ 𝑠 ∈ ran ( mSubst ‘ 𝑡 )
12 4 cv ⊢ 𝑚
13 cmvl ⊢ mVL
14 8 13 cfv ⊢ ( mVL ‘ 𝑡 )
15 12 14 wcel ⊢ 𝑚 ∈ ( mVL ‘ 𝑡 )
16 11 15 wa ⊢ ( 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ∧ 𝑚 ∈ ( mVL ‘ 𝑡 ) )
17 vv ⊢ 𝑣
18 cmvar ⊢ mVR
19 8 18 cfv ⊢ ( mVR ‘ 𝑡 )
20 cmevl ⊢ mEval
21 8 20 cfv ⊢ ( mEval ‘ 𝑡 )
22 21 cdm ⊢ dom ( mEval ‘ 𝑡 )
23 cmvh ⊢ mVH
24 8 23 cfv ⊢ ( mVH ‘ 𝑡 )
25 17 cv ⊢ 𝑣
26 25 24 cfv ⊢ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 )
27 26 6 cfv ⊢ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) )
28 12 27 22 wbr ⊢ 𝑚 dom ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) )
29 28 17 19 wral ⊢ ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) 𝑚 dom ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) )
30 5 cv ⊢ 𝑥
31 12 27 21 co ⊢ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) )
32 17 19 31 cmpt ⊢ ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ) )
33 30 32 wceq ⊢ 𝑥 = ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ) )
34 16 29 33 w3a ⊢ ( ( 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ∧ 𝑚 ∈ ( mVL ‘ 𝑡 ) ) ∧ ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) 𝑚 dom ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ∧ 𝑥 = ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ) ) )
35 34 3 4 5 coprab ⊢ { ⟨ ⟨ 𝑠 , 𝑚 ⟩ , 𝑥 ⟩ ∣ ( ( 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ∧ 𝑚 ∈ ( mVL ‘ 𝑡 ) ) ∧ ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) 𝑚 dom ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ∧ 𝑥 = ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ) ) ) }
36 1 2 35 cmpt ⊢ ( 𝑡 ∈ V ↦ { ⟨ ⟨ 𝑠 , 𝑚 ⟩ , 𝑥 ⟩ ∣ ( ( 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ∧ 𝑚 ∈ ( mVL ‘ 𝑡 ) ) ∧ ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) 𝑚 dom ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ∧ 𝑥 = ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ) ) ) } )
37 0 36 wceq ⊢ mVSubst = ( 𝑡 ∈ V ↦ { ⟨ ⟨ 𝑠 , 𝑚 ⟩ , 𝑥 ⟩ ∣ ( ( 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ∧ 𝑚 ∈ ( mVL ‘ 𝑡 ) ) ∧ ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) 𝑚 dom ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ∧ 𝑥 = ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ( 𝑚 ( mEval ‘ 𝑡 ) ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ) ) ) ) } )