Step | Hyp | Ref
| Expression |
1 | | cmfitp 34601 |
. 2
class
mFromItp |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3474 |
. . 3
class
V |
4 | | vf |
. . . 4
setvar π |
5 | | va |
. . . . 5
setvar π |
6 | 2 | cv 1540 |
. . . . . 6
class π‘ |
7 | | cmsa 34572 |
. . . . . 6
class
mSA |
8 | 6, 7 | cfv 6543 |
. . . . 5
class
(mSAβπ‘) |
9 | | cmuv 34591 |
. . . . . . . 8
class
mUV |
10 | 6, 9 | cfv 6543 |
. . . . . . 7
class
(mUVβπ‘) |
11 | 5 | cv 1540 |
. . . . . . . . 9
class π |
12 | | c1st 7972 |
. . . . . . . . . 10
class
1st |
13 | 6, 12 | cfv 6543 |
. . . . . . . . 9
class
(1st βπ‘) |
14 | 11, 13 | cfv 6543 |
. . . . . . . 8
class
((1st βπ‘)βπ) |
15 | 14 | csn 4628 |
. . . . . . 7
class
{((1st βπ‘)βπ)} |
16 | 10, 15 | cima 5679 |
. . . . . 6
class
((mUVβπ‘)
β {((1st βπ‘)βπ)}) |
17 | | vi |
. . . . . . 7
setvar π |
18 | | cmvrs 34455 |
. . . . . . . . 9
class
mVars |
19 | 6, 18 | cfv 6543 |
. . . . . . . 8
class
(mVarsβπ‘) |
20 | 11, 19 | cfv 6543 |
. . . . . . 7
class
((mVarsβπ‘)βπ) |
21 | 17 | cv 1540 |
. . . . . . . . . 10
class π |
22 | | cmty 34448 |
. . . . . . . . . . 11
class
mType |
23 | 6, 22 | cfv 6543 |
. . . . . . . . . 10
class
(mTypeβπ‘) |
24 | 21, 23 | cfv 6543 |
. . . . . . . . 9
class
((mTypeβπ‘)βπ) |
25 | 24 | csn 4628 |
. . . . . . . 8
class
{((mTypeβπ‘)βπ)} |
26 | 10, 25 | cima 5679 |
. . . . . . 7
class
((mUVβπ‘)
β {((mTypeβπ‘)βπ)}) |
27 | 17, 20, 26 | cixp 8890 |
. . . . . 6
class Xπ β
((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)}) |
28 | | cmap 8819 |
. . . . . 6
class
βm |
29 | 16, 27, 28 | co 7408 |
. . . . 5
class
(((mUVβπ‘)
β {((1st βπ‘)βπ)}) βm Xπ β
((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)})) |
30 | 5, 8, 29 | cixp 8890 |
. . . 4
class Xπ β
(mSAβπ‘)(((mUVβπ‘) β {((1st βπ‘)βπ)}) βm Xπ β
((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)})) |
31 | | vm |
. . . . . . . . . . 11
setvar π |
32 | 31 | cv 1540 |
. . . . . . . . . 10
class π |
33 | | vv |
. . . . . . . . . . . 12
setvar π£ |
34 | 33 | cv 1540 |
. . . . . . . . . . 11
class π£ |
35 | | cmvh 34458 |
. . . . . . . . . . . 12
class
mVH |
36 | 6, 35 | cfv 6543 |
. . . . . . . . . . 11
class
(mVHβπ‘) |
37 | 34, 36 | cfv 6543 |
. . . . . . . . . 10
class
((mVHβπ‘)βπ£) |
38 | 32, 37 | cop 4634 |
. . . . . . . . 9
class
β¨π,
((mVHβπ‘)βπ£)β© |
39 | 34, 32 | cfv 6543 |
. . . . . . . . 9
class (πβπ£) |
40 | | vn |
. . . . . . . . . 10
setvar π |
41 | 40 | cv 1540 |
. . . . . . . . 9
class π |
42 | 38, 39, 41 | wbr 5148 |
. . . . . . . 8
wff β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) |
43 | | cmvar 34447 |
. . . . . . . . 9
class
mVR |
44 | 6, 43 | cfv 6543 |
. . . . . . . 8
class
(mVRβπ‘) |
45 | 42, 33, 44 | wral 3061 |
. . . . . . 7
wff
βπ£ β
(mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) |
46 | | ve |
. . . . . . . . . . . . 13
setvar π |
47 | 46 | cv 1540 |
. . . . . . . . . . . 12
class π |
48 | | vg |
. . . . . . . . . . . . . 14
setvar π |
49 | 48 | cv 1540 |
. . . . . . . . . . . . 13
class π |
50 | 11, 49 | cop 4634 |
. . . . . . . . . . . 12
class
β¨π, πβ© |
51 | | cmst 34578 |
. . . . . . . . . . . . 13
class
mST |
52 | 6, 51 | cfv 6543 |
. . . . . . . . . . . 12
class
(mSTβπ‘) |
53 | 47, 50, 52 | wbr 5148 |
. . . . . . . . . . 11
wff π(mSTβπ‘)β¨π, πβ© |
54 | 32, 47 | cop 4634 |
. . . . . . . . . . . 12
class
β¨π, πβ© |
55 | 21, 36 | cfv 6543 |
. . . . . . . . . . . . . . . 16
class
((mVHβπ‘)βπ) |
56 | 55, 49 | cfv 6543 |
. . . . . . . . . . . . . . 15
class (πβ((mVHβπ‘)βπ)) |
57 | 32, 56, 41 | co 7408 |
. . . . . . . . . . . . . 14
class (ππ(πβ((mVHβπ‘)βπ))) |
58 | 17, 20, 57 | cmpt 5231 |
. . . . . . . . . . . . 13
class (π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))) |
59 | 4 | cv 1540 |
. . . . . . . . . . . . 13
class π |
60 | 58, 59 | cfv 6543 |
. . . . . . . . . . . 12
class (πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ))))) |
61 | 54, 60, 41 | wbr 5148 |
. . . . . . . . . . 11
wff β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ))))) |
62 | 53, 61 | wi 4 |
. . . . . . . . . 10
wff (π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) |
63 | 62, 48 | wal 1539 |
. . . . . . . . 9
wff
βπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) |
64 | 63, 5 | wal 1539 |
. . . . . . . 8
wff
βπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) |
65 | 64, 46 | wal 1539 |
. . . . . . 7
wff
βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) |
66 | 54 | csn 4628 |
. . . . . . . . . 10
class
{β¨π, πβ©} |
67 | 41, 66 | cima 5679 |
. . . . . . . . 9
class (π β {β¨π, πβ©}) |
68 | | cmesy 34575 |
. . . . . . . . . . . . . . 15
class
mESyn |
69 | 6, 68 | cfv 6543 |
. . . . . . . . . . . . . 14
class
(mESynβπ‘) |
70 | 47, 69 | cfv 6543 |
. . . . . . . . . . . . 13
class
((mESynβπ‘)βπ) |
71 | 32, 70 | cop 4634 |
. . . . . . . . . . . 12
class
β¨π,
((mESynβπ‘)βπ)β© |
72 | 71 | csn 4628 |
. . . . . . . . . . 11
class
{β¨π,
((mESynβπ‘)βπ)β©} |
73 | 41, 72 | cima 5679 |
. . . . . . . . . 10
class (π β {β¨π, ((mESynβπ‘)βπ)β©}) |
74 | 47, 12 | cfv 6543 |
. . . . . . . . . . . 12
class
(1st βπ) |
75 | 74 | csn 4628 |
. . . . . . . . . . 11
class
{(1st βπ)} |
76 | 10, 75 | cima 5679 |
. . . . . . . . . 10
class
((mUVβπ‘)
β {(1st βπ)}) |
77 | 73, 76 | cin 3947 |
. . . . . . . . 9
class ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})) |
78 | 67, 77 | wceq 1541 |
. . . . . . . 8
wff (π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})) |
79 | | cmex 34453 |
. . . . . . . . 9
class
mEx |
80 | 6, 79 | cfv 6543 |
. . . . . . . 8
class
(mExβπ‘) |
81 | 78, 46, 80 | wral 3061 |
. . . . . . 7
wff
βπ β
(mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})) |
82 | 45, 65, 81 | w3a 1087 |
. . . . . 6
wff
(βπ£ β
(mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)}))) |
83 | | cmvl 34592 |
. . . . . . 7
class
mVL |
84 | 6, 83 | cfv 6543 |
. . . . . 6
class
(mVLβπ‘) |
85 | 82, 31, 84 | wral 3061 |
. . . . 5
wff
βπ β
(mVLβπ‘)(βπ£ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)}))) |
86 | 84, 80 | cxp 5674 |
. . . . . 6
class
((mVLβπ‘)
Γ (mExβπ‘)) |
87 | | cpm 8820 |
. . . . . 6
class
βpm |
88 | 10, 86, 87 | co 7408 |
. . . . 5
class
((mUVβπ‘)
βpm ((mVLβπ‘) Γ (mExβπ‘))) |
89 | 85, 40, 88 | crio 7363 |
. . . 4
class
(β©π
β ((mUVβπ‘)
βpm ((mVLβπ‘) Γ (mExβπ‘)))βπ β (mVLβπ‘)(βπ£ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})))) |
90 | 4, 30, 89 | cmpt 5231 |
. . 3
class (π β Xπ β
(mSAβπ‘)(((mUVβπ‘) β {((1st βπ‘)βπ)}) βm Xπ β
((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)})) β¦ (β©π β ((mUVβπ‘) βpm
((mVLβπ‘) Γ
(mExβπ‘)))βπ β (mVLβπ‘)(βπ£ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)}))))) |
91 | 2, 3, 90 | cmpt 5231 |
. 2
class (π‘ β V β¦ (π β Xπ β
(mSAβπ‘)(((mUVβπ‘) β {((1st βπ‘)βπ)}) βm Xπ β
((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)})) β¦ (β©π β ((mUVβπ‘) βpm
((mVLβπ‘) Γ
(mExβπ‘)))βπ β (mVLβπ‘)(βπ£ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})))))) |
92 | 1, 91 | wceq 1541 |
1
wff mFromItp =
(π‘ β V β¦ (π β Xπ β
(mSAβπ‘)(((mUVβπ‘) β {((1st βπ‘)βπ)}) βm Xπ β
((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)})) β¦ (β©π β ((mUVβπ‘) βpm
((mVLβπ‘) Γ
(mExβπ‘)))βπ β (mVLβπ‘)(βπ£ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st
βπ)})))))) |