Definition df-mvl

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

	Ref	Expression
Assertion	df-mvl	⊢ mVL = ( 𝑡 ∈ V ↦ X 𝑣 ∈ ( mVR ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvl	⊢ mVL
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cmvar	⊢ mVR
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mVR ‘ 𝑡 )
7		cmuv	⊢ mUV
8	5 7	cfv	⊢ ( mUV ‘ 𝑡 )
9		cmty	⊢ mType
10	5 9	cfv	⊢ ( mType ‘ 𝑡 )
11	3	cv	⊢ 𝑣
12	11 10	cfv	⊢ ( ( mType ‘ 𝑡 ) ‘ 𝑣 )
13	12	csn	⊢ { ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) }
14	8 13	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) } )
15	3 6 14	cixp	⊢ X 𝑣 ∈ ( mVR ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) } )
16	1 2 15	cmpt	⊢ ( 𝑡 ∈ V ↦ X 𝑣 ∈ ( mVR ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) } ) )
17	0 16	wceq	⊢ mVL = ( 𝑡 ∈ V ↦ X 𝑣 ∈ ( mVR ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) } ) )