Step | Hyp | Ref
| Expression |
1 | | cmpps 34136 |
. 2
class
mPPSt |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vd |
. . . . . . . 8
setvar π |
5 | 4 | cv 1541 |
. . . . . . 7
class π |
6 | | vh |
. . . . . . . 8
setvar β |
7 | 6 | cv 1541 |
. . . . . . 7
class β |
8 | | va |
. . . . . . . 8
setvar π |
9 | 8 | cv 1541 |
. . . . . . 7
class π |
10 | 5, 7, 9 | cotp 4598 |
. . . . . 6
class
β¨π, β, πβ© |
11 | 2 | cv 1541 |
. . . . . . 7
class π‘ |
12 | | cmpst 34131 |
. . . . . . 7
class
mPreSt |
13 | 11, 12 | cfv 6500 |
. . . . . 6
class
(mPreStβπ‘) |
14 | 10, 13 | wcel 2107 |
. . . . 5
wff β¨π, β, πβ© β (mPreStβπ‘) |
15 | | cmcls 34135 |
. . . . . . . 8
class
mCls |
16 | 11, 15 | cfv 6500 |
. . . . . . 7
class
(mClsβπ‘) |
17 | 5, 7, 16 | co 7361 |
. . . . . 6
class (π(mClsβπ‘)β) |
18 | 9, 17 | wcel 2107 |
. . . . 5
wff π β (π(mClsβπ‘)β) |
19 | 14, 18 | wa 397 |
. . . 4
wff
(β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β)) |
20 | 19, 4, 6, 8 | coprab 7362 |
. . 3
class
{β¨β¨π,
ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))} |
21 | 2, 3, 20 | cmpt 5192 |
. 2
class (π‘ β V β¦
{β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))}) |
22 | 1, 21 | wceq 1542 |
1
wff mPPSt =
(π‘ β V β¦
{β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))}) |