Step | Hyp | Ref
| Expression |
1 | | cmrsub 34128 |
. 2
class
mRSubst |
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 | | cmcn 34118 |
. . . . . . . . 9
class
mCN |
14 | 5, 13 | cfv 6500 |
. . . . . . . 8
class
(mCNβπ‘) |
15 | 14, 9 | cun 3912 |
. . . . . . 7
class
((mCNβπ‘) βͺ
(mVRβπ‘)) |
16 | | cfrmd 18665 |
. . . . . . 7
class
freeMnd |
17 | 15, 16 | cfv 6500 |
. . . . . 6
class
(freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) |
18 | | vv |
. . . . . . . 8
setvar π£ |
19 | 18 | cv 1541 |
. . . . . . . . . 10
class π£ |
20 | 4 | cv 1541 |
. . . . . . . . . . 11
class π |
21 | 20 | cdm 5637 |
. . . . . . . . . 10
class dom π |
22 | 19, 21 | wcel 2107 |
. . . . . . . . 9
wff π£ β dom π |
23 | 19, 20 | cfv 6500 |
. . . . . . . . 9
class (πβπ£) |
24 | 19 | cs1 14492 |
. . . . . . . . 9
class
β¨βπ£ββ© |
25 | 22, 23, 24 | cif 4490 |
. . . . . . . 8
class if(π£ β dom π, (πβπ£), β¨βπ£ββ©) |
26 | 18, 15, 25 | cmpt 5192 |
. . . . . . 7
class (π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) |
27 | 12 | cv 1541 |
. . . . . . 7
class π |
28 | 26, 27 | ccom 5641 |
. . . . . 6
class ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π) |
29 | | cgsu 17330 |
. . . . . 6
class
Ξ£g |
30 | 17, 28, 29 | co 7361 |
. . . . 5
class
((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)) |
31 | 12, 7, 30 | cmpt 5192 |
. . . 4
class (π β (mRExβπ‘) β¦
((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))) |
32 | 4, 11, 31 | cmpt 5192 |
. . 3
class (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mRExβπ‘) β¦
((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)))) |
33 | 2, 3, 32 | cmpt 5192 |
. 2
class (π‘ β V β¦ (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mRExβπ‘) β¦
((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |
34 | 1, 33 | wceq 1542 |
1
wff mRSubst =
(π‘ β V β¦ (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mRExβπ‘) β¦
((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |