Step | Hyp | Ref
| Expression |
1 | | cmgfs 34576 |
. 2
class
mGFS |
2 | | vt |
. . . . . . 7
setvar π‘ |
3 | 2 | cv 1540 |
. . . . . 6
class π‘ |
4 | | cmtc 34450 |
. . . . . 6
class
mTC |
5 | 3, 4 | cfv 6543 |
. . . . 5
class
(mTCβπ‘) |
6 | | cmvt 34449 |
. . . . . 6
class
mVT |
7 | 3, 6 | cfv 6543 |
. . . . 5
class
(mVTβπ‘) |
8 | | cmsy 34574 |
. . . . . 6
class
mSyn |
9 | 3, 8 | cfv 6543 |
. . . . 5
class
(mSynβπ‘) |
10 | 5, 7, 9 | wf 6539 |
. . . 4
wff
(mSynβπ‘):(mTCβπ‘)βΆ(mVTβπ‘) |
11 | | vc |
. . . . . . . 8
setvar π |
12 | 11 | cv 1540 |
. . . . . . 7
class π |
13 | 12, 9 | cfv 6543 |
. . . . . 6
class
((mSynβπ‘)βπ) |
14 | 13, 12 | wceq 1541 |
. . . . 5
wff
((mSynβπ‘)βπ) = π |
15 | 14, 11, 7 | wral 3061 |
. . . 4
wff
βπ β
(mVTβπ‘)((mSynβπ‘)βπ) = π |
16 | | vd |
. . . . . . . . . . 11
setvar π |
17 | 16 | cv 1540 |
. . . . . . . . . 10
class π |
18 | | vh |
. . . . . . . . . . 11
setvar β |
19 | 18 | cv 1540 |
. . . . . . . . . 10
class β |
20 | | va |
. . . . . . . . . . 11
setvar π |
21 | 20 | cv 1540 |
. . . . . . . . . 10
class π |
22 | 17, 19, 21 | cotp 4636 |
. . . . . . . . 9
class
β¨π, β, πβ© |
23 | | cmax 34451 |
. . . . . . . . . 10
class
mAx |
24 | 3, 23 | cfv 6543 |
. . . . . . . . 9
class
(mAxβπ‘) |
25 | 22, 24 | wcel 2106 |
. . . . . . . 8
wff β¨π, β, πβ© β (mAxβπ‘) |
26 | | ve |
. . . . . . . . . . . 12
setvar π |
27 | 26 | cv 1540 |
. . . . . . . . . . 11
class π |
28 | | cmesy 34575 |
. . . . . . . . . . . 12
class
mESyn |
29 | 3, 28 | cfv 6543 |
. . . . . . . . . . 11
class
(mESynβπ‘) |
30 | 27, 29 | cfv 6543 |
. . . . . . . . . 10
class
((mESynβπ‘)βπ) |
31 | | cmpps 34464 |
. . . . . . . . . . 11
class
mPPSt |
32 | 3, 31 | cfv 6543 |
. . . . . . . . . 10
class
(mPPStβπ‘) |
33 | 30, 32 | wcel 2106 |
. . . . . . . . 9
wff
((mESynβπ‘)βπ) β (mPPStβπ‘) |
34 | 21 | csn 4628 |
. . . . . . . . . 10
class {π} |
35 | 19, 34 | cun 3946 |
. . . . . . . . 9
class (β βͺ {π}) |
36 | 33, 26, 35 | wral 3061 |
. . . . . . . 8
wff
βπ β
(β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘) |
37 | 25, 36 | wi 4 |
. . . . . . 7
wff
(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)) |
38 | 37, 20 | wal 1539 |
. . . . . 6
wff
βπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)) |
39 | 38, 18 | wal 1539 |
. . . . 5
wff
βββπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)) |
40 | 39, 16 | wal 1539 |
. . . 4
wff
βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)) |
41 | 10, 15, 40 | w3a 1087 |
. . 3
wff
((mSynβπ‘):(mTCβπ‘)βΆ(mVTβπ‘) β§ βπ β (mVTβπ‘)((mSynβπ‘)βπ) = π β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘))) |
42 | | cmwgfs 34573 |
. . 3
class
mWGFS |
43 | 41, 2, 42 | crab 3432 |
. 2
class {π‘ β mWGFS β£
((mSynβπ‘):(mTCβπ‘)βΆ(mVTβπ‘) β§ βπ β (mVTβπ‘)((mSynβπ‘)βπ) = π β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)))} |
44 | 1, 43 | wceq 1541 |
1
wff mGFS =
{π‘ β mWGFS β£
((mSynβπ‘):(mTCβπ‘)βΆ(mVTβπ‘) β§ βπ β (mVTβπ‘)((mSynβπ‘)βπ) = π β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β βπ β (β βͺ {π})((mESynβπ‘)βπ) β (mPPStβπ‘)))} |