Step | Hyp | Ref
| Expression |
1 | | cgmdl 34890 |
. 2
class
mGMdl |
2 | | vt |
. . . . . . . . 9
setvar π‘ |
3 | 2 | cv 1540 |
. . . . . . . 8
class π‘ |
4 | | cmuv 34882 |
. . . . . . . 8
class
mUV |
5 | 3, 4 | cfv 6543 |
. . . . . . 7
class
(mUVβπ‘) |
6 | | vc |
. . . . . . . . 9
setvar π |
7 | 6 | cv 1540 |
. . . . . . . 8
class π |
8 | 7 | csn 4628 |
. . . . . . 7
class {π} |
9 | 5, 8 | cima 5679 |
. . . . . 6
class
((mUVβπ‘)
β {π}) |
10 | | cmsy 34865 |
. . . . . . . . . 10
class
mSyn |
11 | 3, 10 | cfv 6543 |
. . . . . . . . 9
class
(mSynβπ‘) |
12 | 7, 11 | cfv 6543 |
. . . . . . . 8
class
((mSynβπ‘)βπ) |
13 | 12 | csn 4628 |
. . . . . . 7
class
{((mSynβπ‘)βπ)} |
14 | 5, 13 | cima 5679 |
. . . . . 6
class
((mUVβπ‘)
β {((mSynβπ‘)βπ)}) |
15 | 9, 14 | wss 3948 |
. . . . 5
wff
((mUVβπ‘)
β {π}) β
((mUVβπ‘) β
{((mSynβπ‘)βπ)}) |
16 | | cmtc 34741 |
. . . . . 6
class
mTC |
17 | 3, 16 | cfv 6543 |
. . . . 5
class
(mTCβπ‘) |
18 | 15, 6, 17 | wral 3061 |
. . . 4
wff
βπ β
(mTCβπ‘)((mUVβπ‘) β {π}) β ((mUVβπ‘) β {((mSynβπ‘)βπ)}) |
19 | | vv |
. . . . . . . . 9
setvar π£ |
20 | 19 | cv 1540 |
. . . . . . . 8
class π£ |
21 | | vw |
. . . . . . . . 9
setvar π€ |
22 | 21 | cv 1540 |
. . . . . . . 8
class π€ |
23 | | cmfsh 34885 |
. . . . . . . . 9
class
mFresh |
24 | 3, 23 | cfv 6543 |
. . . . . . . 8
class
(mFreshβπ‘) |
25 | 20, 22, 24 | wbr 5148 |
. . . . . . 7
wff π£(mFreshβπ‘)π€ |
26 | | cusyn 34889 |
. . . . . . . . . 10
class
mUSyn |
27 | 3, 26 | cfv 6543 |
. . . . . . . . 9
class
(mUSynβπ‘) |
28 | 22, 27 | cfv 6543 |
. . . . . . . 8
class
((mUSynβπ‘)βπ€) |
29 | 20, 28, 24 | wbr 5148 |
. . . . . . 7
wff π£(mFreshβπ‘)((mUSynβπ‘)βπ€) |
30 | 25, 29 | wb 205 |
. . . . . 6
wff (π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) |
31 | 7, 4 | cfv 6543 |
. . . . . 6
class
(mUVβπ) |
32 | 30, 21, 31 | wral 3061 |
. . . . 5
wff
βπ€ β
(mUVβπ)(π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) |
33 | 32, 19, 31 | wral 3061 |
. . . 4
wff
βπ£ β
(mUVβπ)βπ€ β (mUVβπ)(π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) |
34 | | cmevl 34887 |
. . . . . . . . 9
class
mEval |
35 | 3, 34 | cfv 6543 |
. . . . . . . 8
class
(mEvalβπ‘) |
36 | | vm |
. . . . . . . . . . 11
setvar π |
37 | 36 | cv 1540 |
. . . . . . . . . 10
class π |
38 | | ve |
. . . . . . . . . . 11
setvar π |
39 | 38 | cv 1540 |
. . . . . . . . . 10
class π |
40 | 37, 39 | cop 4634 |
. . . . . . . . 9
class
β¨π, πβ© |
41 | 40 | csn 4628 |
. . . . . . . 8
class
{β¨π, πβ©} |
42 | 35, 41 | cima 5679 |
. . . . . . 7
class
((mEvalβπ‘)
β {β¨π, πβ©}) |
43 | | cmesy 34866 |
. . . . . . . . . . . . 13
class
mESyn |
44 | 3, 43 | cfv 6543 |
. . . . . . . . . . . 12
class
(mESynβπ‘) |
45 | 39, 44 | cfv 6543 |
. . . . . . . . . . 11
class
((mESynβπ‘)βπ) |
46 | 37, 45 | cop 4634 |
. . . . . . . . . 10
class
β¨π,
((mESynβπ‘)βπ)β© |
47 | 46 | csn 4628 |
. . . . . . . . 9
class
{β¨π,
((mESynβπ‘)βπ)β©} |
48 | 35, 47 | cima 5679 |
. . . . . . . 8
class
((mEvalβπ‘)
β {β¨π,
((mESynβπ‘)βπ)β©}) |
49 | | c1st 7975 |
. . . . . . . . . . 11
class
1st |
50 | 39, 49 | cfv 6543 |
. . . . . . . . . 10
class
(1st βπ) |
51 | 50 | csn 4628 |
. . . . . . . . 9
class
{(1st βπ)} |
52 | 5, 51 | cima 5679 |
. . . . . . . 8
class
((mUVβπ‘)
β {(1st βπ)}) |
53 | 48, 52 | cin 3947 |
. . . . . . 7
class
(((mEvalβπ‘)
β {β¨π,
((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})) |
54 | 42, 53 | wceq 1541 |
. . . . . 6
wff
((mEvalβπ‘)
β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})) |
55 | | cmex 34744 |
. . . . . . 7
class
mEx |
56 | 3, 55 | cfv 6543 |
. . . . . 6
class
(mExβπ‘) |
57 | 54, 38, 56 | wral 3061 |
. . . . 5
wff
βπ β
(mExβπ‘)((mEvalβπ‘) β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})) |
58 | | cmvl 34883 |
. . . . . 6
class
mVL |
59 | 3, 58 | cfv 6543 |
. . . . 5
class
(mVLβπ‘) |
60 | 57, 36, 59 | wral 3061 |
. . . 4
wff
βπ β
(mVLβπ‘)βπ β (mExβπ‘)((mEvalβπ‘) β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})) |
61 | 18, 33, 60 | w3a 1087 |
. . 3
wff
(βπ β
(mTCβπ‘)((mUVβπ‘) β {π}) β ((mUVβπ‘) β {((mSynβπ‘)βπ)}) β§ βπ£ β (mUVβπ)βπ€ β (mUVβπ)(π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) β§ βπ β (mVLβπ‘)βπ β (mExβπ‘)((mEvalβπ‘) β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)}))) |
62 | | cmgfs 34867 |
. . . 4
class
mGFS |
63 | | cmdl 34888 |
. . . 4
class
mMdl |
64 | 62, 63 | cin 3947 |
. . 3
class (mGFS
β© mMdl) |
65 | 61, 2, 64 | crab 3432 |
. 2
class {π‘ β (mGFS β© mMdl)
β£ (βπ β
(mTCβπ‘)((mUVβπ‘) β {π}) β ((mUVβπ‘) β {((mSynβπ‘)βπ)}) β§ βπ£ β (mUVβπ)βπ€ β (mUVβπ)(π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) β§ βπ β (mVLβπ‘)βπ β (mExβπ‘)((mEvalβπ‘) β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})))} |
66 | 1, 65 | wceq 1541 |
1
wff mGMdl =
{π‘ β (mGFS β© mMdl)
β£ (βπ β
(mTCβπ‘)((mUVβπ‘) β {π}) β ((mUVβπ‘) β {((mSynβπ‘)βπ)}) β§ βπ£ β (mUVβπ)βπ€ β (mUVβπ)(π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) β§ βπ β (mVLβπ‘)βπ β (mExβπ‘)((mEvalβπ‘) β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})))} |