Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mvh Structured version   Visualization version   GIF version

Definition df-mvh 32743
Description: Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mvh mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
Distinct variable group:   𝑣,𝑡

Detailed syntax breakdown of Definition df-mvh
StepHypRef Expression
1 cmvh 32723 . 2 class mVH
2 vt . . 3 setvar 𝑡
3 cvv 3497 . . 3 class V
4 vv . . . 4 setvar 𝑣
52cv 1535 . . . . 5 class 𝑡
6 cmvar 32712 . . . . 5 class mVR
75, 6cfv 6358 . . . 4 class (mVR‘𝑡)
84cv 1535 . . . . . 6 class 𝑣
9 cmty 32713 . . . . . . 7 class mType
105, 9cfv 6358 . . . . . 6 class (mType‘𝑡)
118, 10cfv 6358 . . . . 5 class ((mType‘𝑡)‘𝑣)
128cs1 13952 . . . . 5 class ⟨“𝑣”⟩
1311, 12cop 4576 . . . 4 class ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩
144, 7, 13cmpt 5149 . . 3 class (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩)
152, 3, 14cmpt 5149 . 2 class (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
161, 15wceq 1536 1 wff mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
Colors of variables: wff setvar class
This definition is referenced by:  mvhfval  32784
  Copyright terms: Public domain W3C validator