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 ∈ V ⟼ s m x | s ∈ ran ⁡ mSubst ⁡ t ∧ m ∈ mVL ⁡ t ∧ ∀ v ∈ mVR ⁡ t m dom ⁡ mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v ∧ x = v ∈ mVR ⁡ t ⟼ m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvsb class mVSubst
1 vt setvar t
2 cvv class V
3 vs setvar s
4 vm setvar m
5 vx setvar x
6 3 cv setvar s
7 cmsub class mSubst
8 1 cv setvar t
9 8 7 cfv class mSubst ⁡ t
10 9 crn class ran ⁡ mSubst ⁡ t
11 6 10 wcel wff s ∈ ran ⁡ mSubst ⁡ t
12 4 cv setvar m
13 cmvl class mVL
14 8 13 cfv class mVL ⁡ t
15 12 14 wcel wff m ∈ mVL ⁡ t
16 11 15 wa wff s ∈ ran ⁡ mSubst ⁡ t ∧ m ∈ mVL ⁡ t
17 vv setvar v
18 cmvar class mVR
19 8 18 cfv class mVR ⁡ t
20 cmevl class mEval
21 8 20 cfv class mEval ⁡ t
22 21 cdm class dom ⁡ mEval ⁡ t
23 cmvh class mVH
24 8 23 cfv class mVH ⁡ t
25 17 cv setvar v
26 25 24 cfv class mVH ⁡ t ⁡ v
27 26 6 cfv class s ⁡ mVH ⁡ t ⁡ v
28 12 27 22 wbr wff m dom ⁡ mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
29 28 17 19 wral wff ∀ v ∈ mVR ⁡ t m dom ⁡ mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
30 5 cv setvar x
31 12 27 21 co class m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
32 17 19 31 cmpt class v ∈ mVR ⁡ t ⟼ m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
33 30 32 wceq wff x = v ∈ mVR ⁡ t ⟼ m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
34 16 29 33 w3a wff s ∈ ran ⁡ mSubst ⁡ t ∧ m ∈ mVL ⁡ t ∧ ∀ v ∈ mVR ⁡ t m dom ⁡ mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v ∧ x = v ∈ mVR ⁡ t ⟼ m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
35 34 3 4 5 coprab class s m x | s ∈ ran ⁡ mSubst ⁡ t ∧ m ∈ mVL ⁡ t ∧ ∀ v ∈ mVR ⁡ t m dom ⁡ mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v ∧ x = v ∈ mVR ⁡ t ⟼ m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
36 1 2 35 cmpt class t ∈ V ⟼ s m x | s ∈ ran ⁡ mSubst ⁡ t ∧ m ∈ mVL ⁡ t ∧ ∀ v ∈ mVR ⁡ t m dom ⁡ mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v ∧ x = v ∈ mVR ⁡ t ⟼ m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v
37 0 36 wceq wff mVSubst = t ∈ V ⟼ s m x | s ∈ ran ⁡ mSubst ⁡ t ∧ m ∈ mVL ⁡ t ∧ ∀ v ∈ mVR ⁡ t m dom ⁡ mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v ∧ x = v ∈ mVR ⁡ t ⟼ m mEval ⁡ t s ⁡ mVH ⁡ t ⁡ v