Step | Hyp | Ref
| Expression |
1 | | cmsub 34129 |
. 2
class
mSubst |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vf |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . . 6
class π‘ |
6 | | cmrex 34124 |
. . . . . 6
class
mREx |
7 | 5, 6 | cfv 6500 |
. . . . 5
class
(mRExβπ‘) |
8 | | cmvar 34119 |
. . . . . 6
class
mVR |
9 | 5, 8 | cfv 6500 |
. . . . 5
class
(mVRβπ‘) |
10 | | cpm 8772 |
. . . . 5
class
βpm |
11 | 7, 9, 10 | co 7361 |
. . . 4
class
((mRExβπ‘)
βpm (mVRβπ‘)) |
12 | | ve |
. . . . 5
setvar π |
13 | | cmex 34125 |
. . . . . 6
class
mEx |
14 | 5, 13 | cfv 6500 |
. . . . 5
class
(mExβπ‘) |
15 | 12 | cv 1541 |
. . . . . . 7
class π |
16 | | c1st 7923 |
. . . . . . 7
class
1st |
17 | 15, 16 | cfv 6500 |
. . . . . 6
class
(1st βπ) |
18 | | c2nd 7924 |
. . . . . . . 8
class
2nd |
19 | 15, 18 | cfv 6500 |
. . . . . . 7
class
(2nd βπ) |
20 | 4 | cv 1541 |
. . . . . . . 8
class π |
21 | | cmrsub 34128 |
. . . . . . . . 9
class
mRSubst |
22 | 5, 21 | cfv 6500 |
. . . . . . . 8
class
(mRSubstβπ‘) |
23 | 20, 22 | cfv 6500 |
. . . . . . 7
class
((mRSubstβπ‘)βπ) |
24 | 19, 23 | cfv 6500 |
. . . . . 6
class
(((mRSubstβπ‘)βπ)β(2nd βπ)) |
25 | 17, 24 | cop 4596 |
. . . . 5
class
β¨(1st βπ), (((mRSubstβπ‘)βπ)β(2nd βπ))β© |
26 | 12, 14, 25 | cmpt 5192 |
. . . 4
class (π β (mExβπ‘) β¦ β¨(1st
βπ),
(((mRSubstβπ‘)βπ)β(2nd βπ))β©) |
27 | 4, 11, 26 | cmpt 5192 |
. . 3
class (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mExβπ‘) β¦ β¨(1st
βπ),
(((mRSubstβπ‘)βπ)β(2nd βπ))β©)) |
28 | 2, 3, 27 | cmpt 5192 |
. 2
class (π‘ β V β¦ (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mExβπ‘) β¦ β¨(1st
βπ),
(((mRSubstβπ‘)βπ)β(2nd βπ))β©))) |
29 | 1, 28 | wceq 1542 |
1
wff mSubst =
(π‘ β V β¦ (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mExβπ‘) β¦ β¨(1st
βπ),
(((mRSubstβπ‘)βπ)β(2nd βπ))β©))) |