Step | Hyp | Ref
| Expression |
1 | | mppsval.j |
. 2
β’ π½ = (mPPStβπ) |
2 | | fveq2 6846 |
. . . . . . . 8
β’ (π‘ = π β (mPreStβπ‘) = (mPreStβπ)) |
3 | | mppsval.p |
. . . . . . . 8
β’ π = (mPreStβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
β’ (π‘ = π β (mPreStβπ‘) = π) |
5 | 4 | eleq2d 2820 |
. . . . . 6
β’ (π‘ = π β (β¨π, β, πβ© β (mPreStβπ‘) β β¨π, β, πβ© β π)) |
6 | | fveq2 6846 |
. . . . . . . . 9
β’ (π‘ = π β (mClsβπ‘) = (mClsβπ)) |
7 | | mppsval.c |
. . . . . . . . 9
β’ πΆ = (mClsβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . 8
β’ (π‘ = π β (mClsβπ‘) = πΆ) |
9 | 8 | oveqd 7378 |
. . . . . . 7
β’ (π‘ = π β (π(mClsβπ‘)β) = (ππΆβ)) |
10 | 9 | eleq2d 2820 |
. . . . . 6
β’ (π‘ = π β (π β (π(mClsβπ‘)β) β π β (ππΆβ))) |
11 | 5, 10 | anbi12d 632 |
. . . . 5
β’ (π‘ = π β ((β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β)) β (β¨π, β, πβ© β π β§ π β (ππΆβ)))) |
12 | 11 | oprabbidv 7427 |
. . . 4
β’ (π‘ = π β {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))} = {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))}) |
13 | | df-mpps 34156 |
. . . 4
β’ mPPSt =
(π‘ β V β¦
{β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β (mPreStβπ‘) β§ π β (π(mClsβπ‘)β))}) |
14 | 3 | fvexi 6860 |
. . . . 5
β’ π β V |
15 | 3, 1, 7 | mppspstlem 34229 |
. . . . 5
β’
{β¨β¨π,
ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} β π |
16 | 14, 15 | ssexi 5283 |
. . . 4
β’
{β¨β¨π,
ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} β V |
17 | 12, 13, 16 | fvmpt 6952 |
. . 3
β’ (π β V β
(mPPStβπ) =
{β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))}) |
18 | | fvprc 6838 |
. . . 4
β’ (Β¬
π β V β
(mPPStβπ) =
β
) |
19 | | df-oprab 7365 |
. . . . 5
β’
{β¨β¨π,
ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} = {π₯ β£ βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ)))} |
20 | | abn0 4344 |
. . . . . . 7
β’ ({π₯ β£ βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ)))} β β
β βπ₯βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ)))) |
21 | | elfvex 6884 |
. . . . . . . . . . 11
β’
(β¨π, β, πβ© β (mPreStβπ) β π β V) |
22 | 21, 3 | eleq2s 2852 |
. . . . . . . . . 10
β’
(β¨π, β, πβ© β π β π β V) |
23 | 22 | ad2antrl 727 |
. . . . . . . . 9
β’ ((π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ))) β π β V) |
24 | 23 | exlimivv 1936 |
. . . . . . . 8
β’
(βββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ))) β π β V) |
25 | 24 | exlimivv 1936 |
. . . . . . 7
β’
(βπ₯βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ))) β π β V) |
26 | 20, 25 | sylbi 216 |
. . . . . 6
β’ ({π₯ β£ βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ)))} β β
β π β V) |
27 | 26 | necon1bi 2969 |
. . . . 5
β’ (Β¬
π β V β {π₯ β£ βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ)))} = β
) |
28 | 19, 27 | eqtrid 2785 |
. . . 4
β’ (Β¬
π β V β
{β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} = β
) |
29 | 18, 28 | eqtr4d 2776 |
. . 3
β’ (Β¬
π β V β
(mPPStβπ) =
{β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))}) |
30 | 17, 29 | pm2.61i 182 |
. 2
β’
(mPPStβπ) =
{β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} |
31 | 1, 30 | eqtri 2761 |
1
β’ π½ = {β¨β¨π, ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} |