Definition df-mvl 31514

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

Assertion

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

Distinct variable group:   v, t

Detailed syntax breakdown of Definition df-mvl

Step	Hyp	Ref	Expression
1		cmvl 31501	. 2 class mVL
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vv	. . . 4 setvar v
5	2	cv 1482	. . . . 5 class t
6		cmvar 31358	. . . . 5 class mVR
7	5, 6	cfv 5888	. . . 4 class (mVR ` t )
8		cmuv 31500	. . . . . 6 class mUV
9	5, 8	cfv 5888	. . . . 5 class (mUV ` t )
10	4	cv 1482	. . . . . . 7 class v
11		cmty 31359	. . . . . . . 8 class mType
12	5, 11	cfv 5888	. . . . . . 7 class (mType ` t )
13	10, 12	cfv 5888	. . . . . 6 class ( (mType ` t ) ` v )
14	13	csn 4177	. . . . 5 class { ( (mType ` t ) ` v ) }
15	9, 14	cima 5117	. . . 4 class ( (mUV ` t ) " { ( (mType ` t ) ` v ) } )
16	4, 7, 15	cixp 7908	. . 3 class X_ v e. (mVR ` t ) ( (mUV ` t ) " { ( (mType ` t ) ` v ) } )
17	2, 3, 16	cmpt 4729	. 2 class ( t e. _V |-> X_ v e. (mVR ` t ) ( (mUV ` t ) " { ( (mType ` t ) ` v ) } ) )
18	1, 17	wceq 1483	1 wff mVL = ( t e. _V |-> X_ v e. (mVR ` t ) ( (mUV ` t ) " { ( (mType ` t ) ` v ) } ) )

This definition is referenced by: (None)