Metamath Proof Explorer

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 = t ∈ V ⟼ v ∈ mVR ⁡ t ⟼ mType ⁡ t ⁡ v ⟨“ v ”⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvh class mVH
1 vt setvar t
2 cvv class V
3 vv setvar v
4 cmvar class mVR
5 1 cv setvar t
6 5 4 cfv class mVR ⁡ t
7 cmty class mType
8 5 7 cfv class mType ⁡ t
9 3 cv setvar v
10 9 8 cfv class mType ⁡ t ⁡ v
11 9 cs1 class ⟨“ v ”⟩
12 10 11 cop class mType ⁡ t ⁡ v ⟨“ v ”⟩
13 3 6 12 cmpt class v ∈ mVR ⁡ t ⟼ mType ⁡ t ⁡ v ⟨“ v ”⟩
14 1 2 13 cmpt class t ∈ V ⟼ v ∈ mVR ⁡ t ⟼ mType ⁡ t ⁡ v ⟨“ v ”⟩
15 0 14 wceq wff mVH = t ∈ V ⟼ v ∈ mVR ⁡ t ⟼ mType ⁡ t ⁡ v ⟨“ v ”⟩