Step | Hyp | Ref
| Expression |
1 | | cmvsb 33868 |
. 2
class
mVSubst |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3441 |
. . 3
class
V |
4 | | vs |
. . . . . . . 8
setvar π |
5 | 4 | cv 1539 |
. . . . . . 7
class π |
6 | 2 | cv 1539 |
. . . . . . . . 9
class π‘ |
7 | | cmsub 33732 |
. . . . . . . . 9
class
mSubst |
8 | 6, 7 | cfv 6479 |
. . . . . . . 8
class
(mSubstβπ‘) |
9 | 8 | crn 5621 |
. . . . . . 7
class ran
(mSubstβπ‘) |
10 | 5, 9 | wcel 2105 |
. . . . . 6
wff π β ran (mSubstβπ‘) |
11 | | vm |
. . . . . . . 8
setvar π |
12 | 11 | cv 1539 |
. . . . . . 7
class π |
13 | | cmvl 33867 |
. . . . . . . 8
class
mVL |
14 | 6, 13 | cfv 6479 |
. . . . . . 7
class
(mVLβπ‘) |
15 | 12, 14 | wcel 2105 |
. . . . . 6
wff π β (mVLβπ‘) |
16 | 10, 15 | wa 396 |
. . . . 5
wff (π β ran (mSubstβπ‘) β§ π β (mVLβπ‘)) |
17 | | vv |
. . . . . . . . . 10
setvar π£ |
18 | 17 | cv 1539 |
. . . . . . . . 9
class π£ |
19 | | cmvh 33733 |
. . . . . . . . . 10
class
mVH |
20 | 6, 19 | cfv 6479 |
. . . . . . . . 9
class
(mVHβπ‘) |
21 | 18, 20 | cfv 6479 |
. . . . . . . 8
class
((mVHβπ‘)βπ£) |
22 | 21, 5 | cfv 6479 |
. . . . . . 7
class (π β((mVHβπ‘)βπ£)) |
23 | | cmevl 33871 |
. . . . . . . . 9
class
mEval |
24 | 6, 23 | cfv 6479 |
. . . . . . . 8
class
(mEvalβπ‘) |
25 | 24 | cdm 5620 |
. . . . . . 7
class dom
(mEvalβπ‘) |
26 | 12, 22, 25 | wbr 5092 |
. . . . . 6
wff πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) |
27 | | cmvar 33722 |
. . . . . . 7
class
mVR |
28 | 6, 27 | cfv 6479 |
. . . . . 6
class
(mVRβπ‘) |
29 | 26, 17, 28 | wral 3061 |
. . . . 5
wff
βπ£ β
(mVRβπ‘)πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) |
30 | | vx |
. . . . . . 7
setvar π₯ |
31 | 30 | cv 1539 |
. . . . . 6
class π₯ |
32 | 12, 22, 24 | co 7337 |
. . . . . . 7
class (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£))) |
33 | 17, 28, 32 | cmpt 5175 |
. . . . . 6
class (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£)))) |
34 | 31, 33 | wceq 1540 |
. . . . 5
wff π₯ = (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£)))) |
35 | 16, 29, 34 | w3a 1086 |
. . . 4
wff ((π β ran (mSubstβπ‘) β§ π β (mVLβπ‘)) β§ βπ£ β (mVRβπ‘)πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) β§ π₯ = (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£))))) |
36 | 35, 4, 11, 30 | coprab 7338 |
. . 3
class
{β¨β¨π ,
πβ©, π₯β© β£ ((π β ran (mSubstβπ‘) β§ π β (mVLβπ‘)) β§ βπ£ β (mVRβπ‘)πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) β§ π₯ = (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£)))))} |
37 | 2, 3, 36 | cmpt 5175 |
. 2
class (π‘ β V β¦
{β¨β¨π , πβ©, π₯β© β£ ((π β ran (mSubstβπ‘) β§ π β (mVLβπ‘)) β§ βπ£ β (mVRβπ‘)πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) β§ π₯ = (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£)))))}) |
38 | 1, 37 | wceq 1540 |
1
wff mVSubst =
(π‘ β V β¦
{β¨β¨π , πβ©, π₯β© β£ ((π β ran (mSubstβπ‘) β§ π β (mVLβπ‘)) β§ βπ£ β (mVRβπ‘)πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) β§ π₯ = (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£)))))}) |