Definition df-mvl

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

	Ref	Expression
Assertion	df-mvl	|- mVL = ( t e. _V |-> X_ v e. ( mVR ` t ) ( ( mUV ` t ) " { ( ( mType ` t ) ` v ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvl	|- mVL
1		vt	|- t
2		cvv	|- _V
3		vv	|- v
4		cmvar	|- mVR
5	1	cv	|- t
6	5 4	cfv	|- ( mVR ` t )
7		cmuv	|- mUV
8	5 7	cfv	|- ( mUV ` t )
9		cmty	|- mType
10	5 9	cfv	|- ( mType ` t )
11	3	cv	|- v
12	11 10	cfv	|- ( ( mType ` t ) ` v )
13	12	csn	|- { ( ( mType ` t ) ` v ) }
14	8 13	cima	|- ( ( mUV ` t ) " { ( ( mType ` t ) ` v ) } )
15	3 6 14	cixp	|- X_ v e. ( mVR ` t ) ( ( mUV ` t ) " { ( ( mType ` t ) ` v ) } )
16	1 2 15	cmpt	|- ( t e. _V |-> X_ v e. ( mVR ` t ) ( ( mUV ` t ) " { ( ( mType ` t ) ` v ) } ) )
17	0 16	wceq	|- mVL = ( t e. _V |-> X_ v e. ( mVR ` t ) ( ( mUV ` t ) " { ( ( mType ` t ) ` v ) } ) )