Step | Hyp | Ref
| Expression |
1 | | cmvh 34130 |
. 2
class
mVH |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vv |
. . . 4
setvar 𝑣 |
5 | 2 | cv 1541 |
. . . . 5
class 𝑡 |
6 | | cmvar 34119 |
. . . . 5
class
mVR |
7 | 5, 6 | cfv 6500 |
. . . 4
class
(mVR‘𝑡) |
8 | 4 | cv 1541 |
. . . . . 6
class 𝑣 |
9 | | cmty 34120 |
. . . . . . 7
class
mType |
10 | 5, 9 | cfv 6500 |
. . . . . 6
class
(mType‘𝑡) |
11 | 8, 10 | cfv 6500 |
. . . . 5
class
((mType‘𝑡)‘𝑣) |
12 | 8 | cs1 14492 |
. . . . 5
class
⟨“𝑣”⟩ |
13 | 11, 12 | cop 4596 |
. . . 4
class
⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩ |
14 | 4, 7, 13 | cmpt 5192 |
. . 3
class (𝑣 ∈ (mVR‘𝑡) ↦
⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩) |
15 | 2, 3, 14 | cmpt 5192 |
. 2
class (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦
⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩)) |
16 | 1, 15 | wceq 1542 |
1
wff mVH =
(𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦
⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩)) |