Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (π β π β π β V) |
2 | | msubffval.s |
. . 3
β’ π = (mSubstβπ) |
3 | | fveq2 6846 |
. . . . . . 7
β’ (π‘ = π β (mRExβπ‘) = (mRExβπ)) |
4 | | msubffval.r |
. . . . . . 7
β’ π
= (mRExβπ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . 6
β’ (π‘ = π β (mRExβπ‘) = π
) |
6 | | fveq2 6846 |
. . . . . . 7
β’ (π‘ = π β (mVRβπ‘) = (mVRβπ)) |
7 | | msubffval.v |
. . . . . . 7
β’ π = (mVRβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . 6
β’ (π‘ = π β (mVRβπ‘) = π) |
9 | 5, 8 | oveq12d 7379 |
. . . . 5
β’ (π‘ = π β ((mRExβπ‘) βpm (mVRβπ‘)) = (π
βpm π)) |
10 | | fveq2 6846 |
. . . . . . 7
β’ (π‘ = π β (mExβπ‘) = (mExβπ)) |
11 | | msubffval.e |
. . . . . . 7
β’ πΈ = (mExβπ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . 6
β’ (π‘ = π β (mExβπ‘) = πΈ) |
13 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π‘ = π β (mRSubstβπ‘) = (mRSubstβπ)) |
14 | | msubffval.o |
. . . . . . . . . 10
β’ π = (mRSubstβπ) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π‘ = π β (mRSubstβπ‘) = π) |
16 | 15 | fveq1d 6848 |
. . . . . . . 8
β’ (π‘ = π β ((mRSubstβπ‘)βπ) = (πβπ)) |
17 | 16 | fveq1d 6848 |
. . . . . . 7
β’ (π‘ = π β (((mRSubstβπ‘)βπ)β(2nd βπ)) = ((πβπ)β(2nd βπ))) |
18 | 17 | opeq2d 4841 |
. . . . . 6
β’ (π‘ = π β β¨(1st βπ), (((mRSubstβπ‘)βπ)β(2nd βπ))β© = β¨(1st
βπ), ((πβπ)β(2nd βπ))β©) |
19 | 12, 18 | mpteq12dv 5200 |
. . . . 5
β’ (π‘ = π β (π β (mExβπ‘) β¦ β¨(1st βπ), (((mRSubstβπ‘)βπ)β(2nd βπ))β©) = (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©)) |
20 | 9, 19 | mpteq12dv 5200 |
. . . 4
β’ (π‘ = π β (π β ((mRExβπ‘) βpm (mVRβπ‘)) β¦ (π β (mExβπ‘) β¦ β¨(1st βπ), (((mRSubstβπ‘)βπ)β(2nd βπ))β©)) = (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |
21 | | df-msub 34149 |
. . . 4
β’ mSubst =
(π‘ β V β¦ (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mExβπ‘) β¦ β¨(1st
βπ),
(((mRSubstβπ‘)βπ)β(2nd βπ))β©))) |
22 | | ovex 7394 |
. . . . 5
β’ (π
βpm π) β V |
23 | 22 | mptex 7177 |
. . . 4
β’ (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©)) β
V |
24 | 20, 21, 23 | fvmpt 6952 |
. . 3
β’ (π β V β
(mSubstβπ) = (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |
25 | 2, 24 | eqtrid 2785 |
. 2
β’ (π β V β π = (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |
26 | 1, 25 | syl 17 |
1
β’ (π β π β π = (π β (π
βpm π) β¦ (π β πΈ β¦ β¨(1st βπ), ((πβπ)β(2nd βπ))β©))) |