Step | Hyp | Ref
| Expression |
1 | | cmwgfs 34573 |
. 2
class
mWGFS |
2 | | vd |
. . . . . . . . . . 11
setvar π |
3 | 2 | cv 1540 |
. . . . . . . . . 10
class π |
4 | | vh |
. . . . . . . . . . 11
setvar β |
5 | 4 | cv 1540 |
. . . . . . . . . 10
class β |
6 | | va |
. . . . . . . . . . 11
setvar π |
7 | 6 | cv 1540 |
. . . . . . . . . 10
class π |
8 | 3, 5, 7 | cotp 4636 |
. . . . . . . . 9
class
β¨π, β, πβ© |
9 | | vt |
. . . . . . . . . . 11
setvar π‘ |
10 | 9 | cv 1540 |
. . . . . . . . . 10
class π‘ |
11 | | cmax 34451 |
. . . . . . . . . 10
class
mAx |
12 | 10, 11 | cfv 6543 |
. . . . . . . . 9
class
(mAxβπ‘) |
13 | 8, 12 | wcel 2106 |
. . . . . . . 8
wff β¨π, β, πβ© β (mAxβπ‘) |
14 | | c1st 7972 |
. . . . . . . . . 10
class
1st |
15 | 7, 14 | cfv 6543 |
. . . . . . . . 9
class
(1st βπ) |
16 | | cmvt 34449 |
. . . . . . . . . 10
class
mVT |
17 | 10, 16 | cfv 6543 |
. . . . . . . . 9
class
(mVTβπ‘) |
18 | 15, 17 | wcel 2106 |
. . . . . . . 8
wff
(1st βπ) β (mVTβπ‘) |
19 | 13, 18 | wa 396 |
. . . . . . 7
wff
(β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) |
20 | | vs |
. . . . . . . . . . 11
setvar π |
21 | 20 | cv 1540 |
. . . . . . . . . 10
class π |
22 | | cmsa 34572 |
. . . . . . . . . . 11
class
mSA |
23 | 10, 22 | cfv 6543 |
. . . . . . . . . 10
class
(mSAβπ‘) |
24 | 21, 23 | cima 5679 |
. . . . . . . . 9
class (π β (mSAβπ‘)) |
25 | 7, 24 | wcel 2106 |
. . . . . . . 8
wff π β (π β (mSAβπ‘)) |
26 | | cmsub 34457 |
. . . . . . . . . 10
class
mSubst |
27 | 10, 26 | cfv 6543 |
. . . . . . . . 9
class
(mSubstβπ‘) |
28 | 27 | crn 5677 |
. . . . . . . 8
class ran
(mSubstβπ‘) |
29 | 25, 20, 28 | wrex 3070 |
. . . . . . 7
wff
βπ β ran
(mSubstβπ‘)π β (π β (mSAβπ‘)) |
30 | 19, 29 | wi 4 |
. . . . . 6
wff
((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘))) |
31 | 30, 6 | wal 1539 |
. . . . 5
wff
βπ((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘))) |
32 | 31, 4 | wal 1539 |
. . . 4
wff
βββπ((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘))) |
33 | 32, 2 | wal 1539 |
. . 3
wff
βπβββπ((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘))) |
34 | | cmfs 34462 |
. . 3
class
mFS |
35 | 33, 9, 34 | crab 3432 |
. 2
class {π‘ β mFS β£
βπβββπ((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘)))} |
36 | 1, 35 | wceq 1541 |
1
wff mWGFS =
{π‘ β mFS β£
βπβββπ((β¨π, β, πβ© β (mAxβπ‘) β§ (1st βπ) β (mVTβπ‘)) β βπ β ran (mSubstβπ‘)π β (π β (mSAβπ‘)))} |