Definition df-mvl

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

	Ref	Expression
Assertion	df-mvl	$$⊢\mathrm{mVL}=\left(t\in \mathrm{V}⟼\underset{v\in \mathrm{mVR}\left(t\right)}{⨉}\mathrm{mUV}\left(t\right)\left[\left\{\mathrm{mType}\left(t\right)\left(v\right)\right\}\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvl	$$class\mathrm{mVL}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		vv	$$setvarv$$
4		cmvar	$$class\mathrm{mVR}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mVR}\left(t\right)$$
7		cmuv	$$class\mathrm{mUV}$$
8	5 7	cfv	$$class\mathrm{mUV}\left(t\right)$$
9		cmty	$$class\mathrm{mType}$$
10	5 9	cfv	$$class\mathrm{mType}\left(t\right)$$
11	3	cv	$$setvarv$$
12	11 10	cfv	$$class\mathrm{mType}\left(t\right)\left(v\right)$$
13	12	csn	$$class\left\{\mathrm{mType}\left(t\right)\left(v\right)\right\}$$
14	8 13	cima	$$class\mathrm{mUV}\left(t\right)\left[\left\{\mathrm{mType}\left(t\right)\left(v\right)\right\}\right]$$
15	3 6 14	cixp	$$class\underset{v\in \mathrm{mVR}\left(t\right)}{⨉}\mathrm{mUV}\left(t\right)\left[\left\{\mathrm{mType}\left(t\right)\left(v\right)\right\}\right]$$
16	1 2 15	cmpt	$$class\left(t\in \mathrm{V}⟼\underset{v\in \mathrm{mVR}\left(t\right)}{⨉}\mathrm{mUV}\left(t\right)\left[\left\{\mathrm{mType}\left(t\right)\left(v\right)\right\}\right]\right)$$
17	0 16	wceq	$$wff\mathrm{mVL}=\left(t\in \mathrm{V}⟼\underset{v\in \mathrm{mVR}\left(t\right)}{⨉}\mathrm{mUV}\left(t\right)\left[\left\{\mathrm{mType}\left(t\right)\left(v\right)\right\}\right]\right)$$