Detailed syntax breakdown of Definition df-mthm
Step | Hyp | Ref
| Expression |
1 | | cmthm 31911 |
. 2
class
mThm |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3414 |
. . 3
class
V |
4 | 2 | cv 1655 |
. . . . . 6
class 𝑡 |
5 | | cmsr 31906 |
. . . . . 6
class
mStRed |
6 | 4, 5 | cfv 6123 |
. . . . 5
class
(mStRed‘𝑡) |
7 | 6 | ccnv 5341 |
. . . 4
class ◡(mStRed‘𝑡) |
8 | | cmpps 31910 |
. . . . . 6
class
mPPSt |
9 | 4, 8 | cfv 6123 |
. . . . 5
class
(mPPSt‘𝑡) |
10 | 6, 9 | cima 5345 |
. . . 4
class
((mStRed‘𝑡)
“ (mPPSt‘𝑡)) |
11 | 7, 10 | cima 5345 |
. . 3
class (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡))) |
12 | 2, 3, 11 | cmpt 4952 |
. 2
class (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡)))) |
13 | 1, 12 | wceq 1656 |
1
wff mThm =
(𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡)))) |