Detailed syntax breakdown of Definition df-mst
Step | Hyp | Ref
| Expression |
1 | | cmst 31489 |
. 2
class
mST |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3200 |
. . 3
class
V |
4 | | c0 3915 |
. . . . 5
class
∅ |
5 | 2 | cv 1482 |
. . . . . 6
class 𝑡 |
6 | | cmtree 31488 |
. . . . . 6
class
mTree |
7 | 5, 6 | cfv 5888 |
. . . . 5
class
(mTree‘𝑡) |
8 | 4, 4, 7 | co 6650 |
. . . 4
class
(∅(mTree‘𝑡)∅) |
9 | | cmex 31364 |
. . . . . 6
class
mEx |
10 | 5, 9 | cfv 5888 |
. . . . 5
class
(mEx‘𝑡) |
11 | | cmvt 31360 |
. . . . . 6
class
mVT |
12 | 5, 11 | cfv 5888 |
. . . . 5
class
(mVT‘𝑡) |
13 | 10, 12 | cres 5116 |
. . . 4
class
((mEx‘𝑡)
↾ (mVT‘𝑡)) |
14 | 8, 13 | cres 5116 |
. . 3
class
((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡))) |
15 | 2, 3, 14 | cmpt 4729 |
. 2
class (𝑡 ∈ V ↦
((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) |
16 | 1, 15 | wceq 1483 |
1
wff mST =
(𝑡 ∈ V ↦
((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡)))) |