Metamath Proof Explorer

Definition df-mvl

Description: Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mvl ⊢ mVL = t ∈ V ⟼ ⨉ v ∈ mVR ⁡ t mUV ⁡ t mType ⁡ t ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvl class mVL
1 vt setvar t
2 cvv class V
3 vv setvar v
4 cmvar class mVR
5 1 cv setvar t
6 5 4 cfv class mVR ⁡ t
7 cmuv class mUV
8 5 7 cfv class mUV ⁡ t
9 cmty class mType
10 5 9 cfv class mType ⁡ t
11 3 cv setvar v
12 11 10 cfv class mType ⁡ t ⁡ v
13 12 csn class mType ⁡ t ⁡ v
14 8 13 cima class mUV ⁡ t mType ⁡ t ⁡ v
15 3 6 14 cixp class ⨉ v ∈ mVR ⁡ t mUV ⁡ t mType ⁡ t ⁡ v
16 1 2 15 cmpt class t ∈ V ⟼ ⨉ v ∈ mVR ⁡ t mUV ⁡ t mType ⁡ t ⁡ v
17 0 16 wceq wff mVL = t ∈ V ⟼ ⨉ v ∈ mVR ⁡ t mUV ⁡ t mType ⁡ t ⁡ v