Step | Hyp | Ref
| Expression |
1 | | cmpst 34131 |
. 2
class
mPreSt |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vd |
. . . . . . . . 9
setvar π |
5 | 4 | cv 1541 |
. . . . . . . 8
class π |
6 | 5 | ccnv 5636 |
. . . . . . 7
class β‘π |
7 | 6, 5 | wceq 1542 |
. . . . . 6
wff β‘π = π |
8 | 2 | cv 1541 |
. . . . . . . 8
class π‘ |
9 | | cmdv 34126 |
. . . . . . . 8
class
mDV |
10 | 8, 9 | cfv 6500 |
. . . . . . 7
class
(mDVβπ‘) |
11 | 10 | cpw 4564 |
. . . . . 6
class π«
(mDVβπ‘) |
12 | 7, 4, 11 | crab 3406 |
. . . . 5
class {π β π«
(mDVβπ‘) β£ β‘π = π} |
13 | | cmex 34125 |
. . . . . . . 8
class
mEx |
14 | 8, 13 | cfv 6500 |
. . . . . . 7
class
(mExβπ‘) |
15 | 14 | cpw 4564 |
. . . . . 6
class π«
(mExβπ‘) |
16 | | cfn 8889 |
. . . . . 6
class
Fin |
17 | 15, 16 | cin 3913 |
. . . . 5
class
(π« (mExβπ‘) β© Fin) |
18 | 12, 17 | cxp 5635 |
. . . 4
class ({π β π«
(mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) |
19 | 18, 14 | cxp 5635 |
. . 3
class (({π β π«
(mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ
(mExβπ‘)) |
20 | 2, 3, 19 | cmpt 5192 |
. 2
class (π‘ β V β¦ (({π β π«
(mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ
(mExβπ‘))) |
21 | 1, 20 | wceq 1542 |
1
wff mPreSt =
(π‘ β V β¦
(({π β π«
(mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ
(mExβπ‘))) |