Detailed syntax breakdown of Definition df-mvh
Step | Hyp | Ref
| Expression |
1 | | cmvh 33178 |
. 2
class
mVH |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3423 |
. . 3
class
V |
4 | | vv |
. . . 4
setvar 𝑣 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑡 |
6 | | cmvar 33167 |
. . . . 5
class
mVR |
7 | 5, 6 | cfv 6401 |
. . . 4
class
(mVR‘𝑡) |
8 | 4 | cv 1542 |
. . . . . 6
class 𝑣 |
9 | | cmty 33168 |
. . . . . . 7
class
mType |
10 | 5, 9 | cfv 6401 |
. . . . . 6
class
(mType‘𝑡) |
11 | 8, 10 | cfv 6401 |
. . . . 5
class
((mType‘𝑡)‘𝑣) |
12 | 8 | cs1 14185 |
. . . . 5
class
〈“𝑣”〉 |
13 | 11, 12 | cop 4564 |
. . . 4
class
〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉 |
14 | 4, 7, 13 | cmpt 5152 |
. . 3
class (𝑣 ∈ (mVR‘𝑡) ↦
〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉) |
15 | 2, 3, 14 | cmpt 5152 |
. 2
class (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦
〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉)) |
16 | 1, 15 | wceq 1543 |
1
wff mVH =
(𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦
〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉)) |