Step | Hyp | Ref
| Expression |
1 | | cmthm 34470 |
. 2
class
mThm |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3475 |
. . 3
class
V |
4 | 2 | cv 1541 |
. . . . . 6
class 𝑡 |
5 | | cmsr 34465 |
. . . . . 6
class
mStRed |
6 | 4, 5 | cfv 6544 |
. . . . 5
class
(mStRed‘𝑡) |
7 | 6 | ccnv 5676 |
. . . 4
class ◡(mStRed‘𝑡) |
8 | | cmpps 34469 |
. . . . . 6
class
mPPSt |
9 | 4, 8 | cfv 6544 |
. . . . 5
class
(mPPSt‘𝑡) |
10 | 6, 9 | cima 5680 |
. . . 4
class
((mStRed‘𝑡)
“ (mPPSt‘𝑡)) |
11 | 7, 10 | cima 5680 |
. . 3
class (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡))) |
12 | 2, 3, 11 | cmpt 5232 |
. 2
class (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡)))) |
13 | 1, 12 | wceq 1542 |
1
wff mThm =
(𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡)))) |