Step | Hyp | Ref
| Expression |
1 | | cmesy 34575 |
. 2
class
mESyn |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3474 |
. . 3
class
V |
4 | | vc |
. . . 4
setvar π |
5 | | ve |
. . . 4
setvar π |
6 | 2 | cv 1540 |
. . . . 5
class π‘ |
7 | | cmtc 34450 |
. . . . 5
class
mTC |
8 | 6, 7 | cfv 6543 |
. . . 4
class
(mTCβπ‘) |
9 | | cmrex 34452 |
. . . . 5
class
mREx |
10 | 6, 9 | cfv 6543 |
. . . 4
class
(mRExβπ‘) |
11 | 4 | cv 1540 |
. . . . . 6
class π |
12 | | cmsy 34574 |
. . . . . . 7
class
mSyn |
13 | 6, 12 | cfv 6543 |
. . . . . 6
class
(mSynβπ‘) |
14 | 11, 13 | cfv 6543 |
. . . . 5
class
((mSynβπ‘)βπ) |
15 | 5 | cv 1540 |
. . . . 5
class π |
16 | | cm0s 34571 |
. . . . 5
class
m0St |
17 | 14, 15, 16 | co 7408 |
. . . 4
class
(((mSynβπ‘)βπ)m0Stπ) |
18 | 4, 5, 8, 10, 17 | cmpo 7410 |
. . 3
class (π β (mTCβπ‘), π β (mRExβπ‘) β¦ (((mSynβπ‘)βπ)m0Stπ)) |
19 | 2, 3, 18 | cmpt 5231 |
. 2
class (π‘ β V β¦ (π β (mTCβπ‘), π β (mRExβπ‘) β¦ (((mSynβπ‘)βπ)m0Stπ))) |
20 | 1, 19 | wceq 1541 |
1
wff mESyn =
(π‘ β V β¦ (π β (mTCβπ‘), π β (mRExβπ‘) β¦ (((mSynβπ‘)βπ)m0Stπ))) |