Step | Hyp | Ref
| Expression |
1 | | mpstval.p |
. 2
β’ π = (mPreStβπ) |
2 | | fveq2 6843 |
. . . . . . . . 9
β’ (π‘ = π β (mDVβπ‘) = (mDVβπ)) |
3 | | mpstval.v |
. . . . . . . . 9
β’ π = (mDVβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . . 8
β’ (π‘ = π β (mDVβπ‘) = π) |
5 | 4 | pweqd 4578 |
. . . . . . 7
β’ (π‘ = π β π« (mDVβπ‘) = π« π) |
6 | 5 | rabeqdv 3421 |
. . . . . 6
β’ (π‘ = π β {π β π« (mDVβπ‘) β£ β‘π = π} = {π β π« π β£ β‘π = π}) |
7 | | fveq2 6843 |
. . . . . . . . 9
β’ (π‘ = π β (mExβπ‘) = (mExβπ)) |
8 | | mpstval.e |
. . . . . . . . 9
β’ πΈ = (mExβπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . 8
β’ (π‘ = π β (mExβπ‘) = πΈ) |
10 | 9 | pweqd 4578 |
. . . . . . 7
β’ (π‘ = π β π« (mExβπ‘) = π« πΈ) |
11 | 10 | ineq1d 4172 |
. . . . . 6
β’ (π‘ = π β (π« (mExβπ‘) β© Fin) = (π« πΈ β© Fin)) |
12 | 6, 11 | xpeq12d 5665 |
. . . . 5
β’ (π‘ = π β ({π β π« (mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) = ({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin))) |
13 | 12, 9 | xpeq12d 5665 |
. . . 4
β’ (π‘ = π β (({π β π« (mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ
(mExβπ‘)) = (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ)) |
14 | | df-mpst 34144 |
. . . 4
β’ mPreSt =
(π‘ β V β¦
(({π β π«
(mDVβπ‘) β£ β‘π = π} Γ (π« (mExβπ‘) β© Fin)) Γ
(mExβπ‘))) |
15 | 3 | fvexi 6857 |
. . . . . . . 8
β’ π β V |
16 | 15 | pwex 5336 |
. . . . . . 7
β’ π«
π β V |
17 | 16 | rabex 5290 |
. . . . . 6
β’ {π β π« π β£ β‘π = π} β V |
18 | 8 | fvexi 6857 |
. . . . . . . 8
β’ πΈ β V |
19 | 18 | pwex 5336 |
. . . . . . 7
β’ π«
πΈ β V |
20 | 19 | inex1 5275 |
. . . . . 6
β’
(π« πΈ β©
Fin) β V |
21 | 17, 20 | xpex 7688 |
. . . . 5
β’ ({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) β V |
22 | 21, 18 | xpex 7688 |
. . . 4
β’ (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) β V |
23 | 13, 14, 22 | fvmpt 6949 |
. . 3
β’ (π β V β
(mPreStβπ) = (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ)) |
24 | | xp0 6111 |
. . . . 5
β’ (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ β
) =
β
|
25 | 24 | eqcomi 2742 |
. . . 4
β’ β
=
(({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ
β
) |
26 | | fvprc 6835 |
. . . 4
β’ (Β¬
π β V β
(mPreStβπ) =
β
) |
27 | | fvprc 6835 |
. . . . . 6
β’ (Β¬
π β V β
(mExβπ) =
β
) |
28 | 8, 27 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β πΈ = β
) |
29 | 28 | xpeq2d 5664 |
. . . 4
β’ (Β¬
π β V β (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) = (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ
β
)) |
30 | 25, 26, 29 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β
(mPreStβπ) = (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ)) |
31 | 23, 30 | pm2.61i 182 |
. 2
β’
(mPreStβπ) =
(({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) |
32 | 1, 31 | eqtri 2761 |
1
β’ π = (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) |