Definition df-mvh

Description: Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mvh	⊢ mVH = ( 𝑡 ∈ V ↦ ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvh	⊢ mVH
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cmvar	⊢ mVR
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mVR ‘ 𝑡 )
7		cmty	⊢ mType
8	5 7	cfv	⊢ ( mType ‘ 𝑡 )
9	3	cv	⊢ 𝑣
10	9 8	cfv	⊢ ( ( mType ‘ 𝑡 ) ‘ 𝑣 )
11	9	cs1	⊢ ⟨“ 𝑣 ”⟩
12	10 11	cop	⊢ ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩
13	3 6 12	cmpt	⊢ ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )
14	1 2 13	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )
15	0 14	wceq	⊢ mVH = ( 𝑡 ∈ V ↦ ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )