Step | Hyp | Ref
| Expression |
1 | | df-metid 32558 |
. 2
β’
~Met = (π
β βͺ ran PsMet β¦ {β¨π₯, π¦β© β£ ((π₯ β dom dom π β§ π¦ β dom dom π) β§ (π₯ππ¦) = 0)}) |
2 | | simpr 485 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ π = π·) β π = π·) |
3 | 2 | dmeqd 5866 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π = π·) β dom π = dom π·) |
4 | 3 | dmeqd 5866 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = dom dom π·) |
5 | | psmetdmdm 23695 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β π = dom dom π·) |
6 | 5 | adantr 481 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π = π·) β π = dom dom π·) |
7 | 4, 6 | eqtr4d 2774 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = π) |
8 | 7 | eleq2d 2818 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β (π₯ β dom dom π β π₯ β π)) |
9 | 7 | eleq2d 2818 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β (π¦ β dom dom π β π¦ β π)) |
10 | 8, 9 | anbi12d 631 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β ((π₯ β dom dom π β§ π¦ β dom dom π) β (π₯ β π β§ π¦ β π))) |
11 | 2 | oveqd 7379 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β (π₯ππ¦) = (π₯π·π¦)) |
12 | 11 | eqeq1d 2733 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β ((π₯ππ¦) = 0 β (π₯π·π¦) = 0)) |
13 | 10, 12 | anbi12d 631 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β (((π₯ β dom dom π β§ π¦ β dom dom π) β§ (π₯ππ¦) = 0) β ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0))) |
14 | 13 | opabbidv 5176 |
. 2
β’ ((π· β (PsMetβπ) β§ π = π·) β {β¨π₯, π¦β© β£ ((π₯ β dom dom π β§ π¦ β dom dom π) β§ (π₯ππ¦) = 0)} = {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0)}) |
15 | | elfvunirn 6879 |
. 2
β’ (π· β (PsMetβπ) β π· β βͺ ran
PsMet) |
16 | | opabssxp 5729 |
. . 3
β’
{β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0)} β (π Γ π) |
17 | | elfvex 6885 |
. . . 4
β’ (π· β (PsMetβπ) β π β V) |
18 | 17, 17 | xpexd 7690 |
. . 3
β’ (π· β (PsMetβπ) β (π Γ π) β V) |
19 | | ssexg 5285 |
. . 3
β’
(({β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0)} β (π Γ π) β§ (π Γ π) β V) β {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0)} β V) |
20 | 16, 18, 19 | sylancr 587 |
. 2
β’ (π· β (PsMetβπ) β {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0)} β V) |
21 | 1, 14, 15, 20 | fvmptd2 6961 |
1
β’ (π· β (PsMetβπ) β
(~Metβπ·) =
{β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0)}) |