Step | Hyp | Ref
| Expression |
1 | | df-bl 20744 |
. 2
β’ ball =
(π β V β¦ (π₯ β dom dom π, π β β* β¦ {π¦ β dom dom π β£ (π₯ππ¦) < π})) |
2 | | dmeq 5857 |
. . . . 5
β’ (π = π· β dom π = dom π·) |
3 | 2 | dmeqd 5859 |
. . . 4
β’ (π = π· β dom dom π = dom dom π·) |
4 | | psmetdmdm 23610 |
. . . . 5
β’ (π· β (PsMetβπ) β π = dom dom π·) |
5 | 4 | eqcomd 2743 |
. . . 4
β’ (π· β (PsMetβπ) β dom dom π· = π) |
6 | 3, 5 | sylan9eqr 2799 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = π) |
7 | | eqidd 2738 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β β* =
β*) |
8 | | simpr 485 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π = π·) β π = π·) |
9 | 8 | oveqd 7368 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β (π₯ππ¦) = (π₯π·π¦)) |
10 | 9 | breq1d 5113 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β ((π₯ππ¦) < π β (π₯π·π¦) < π)) |
11 | 6, 10 | rabeqbidv 3422 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β {π¦ β dom dom π β£ (π₯ππ¦) < π} = {π¦ β π β£ (π₯π·π¦) < π}) |
12 | 6, 7, 11 | mpoeq123dv 7426 |
. 2
β’ ((π· β (PsMetβπ) β§ π = π·) β (π₯ β dom dom π, π β β* β¦ {π¦ β dom dom π β£ (π₯ππ¦) < π}) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π})) |
13 | | elex 3461 |
. 2
β’ (π· β (PsMetβπ) β π· β V) |
14 | | ssrab2 4035 |
. . . . . 6
β’ {π¦ β π β£ (π₯π·π¦) < π} β π |
15 | | elfvdm 6876 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β π β dom PsMet) |
16 | 15 | adantr 481 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π β β*)) β π β dom
PsMet) |
17 | | elpw2g 5299 |
. . . . . . 7
β’ (π β dom PsMet β ({π¦ β π β£ (π₯π·π¦) < π} β π« π β {π¦ β π β£ (π₯π·π¦) < π} β π)) |
18 | 16, 17 | syl 17 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π β β*)) β ({π¦ β π β£ (π₯π·π¦) < π} β π« π β {π¦ β π β£ (π₯π·π¦) < π} β π)) |
19 | 14, 18 | mpbiri 257 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π β β*)) β {π¦ β π β£ (π₯π·π¦) < π} β π« π) |
20 | 19 | ralrimivva 3195 |
. . . 4
β’ (π· β (PsMetβπ) β βπ₯ β π βπ β β* {π¦ β π β£ (π₯π·π¦) < π} β π« π) |
21 | | eqid 2737 |
. . . . 5
β’ (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) |
22 | 21 | fmpo 7992 |
. . . 4
β’
(βπ₯ β
π βπ β β*
{π¦ β π β£ (π₯π·π¦) < π} β π« π β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π) |
23 | 20, 22 | sylib 217 |
. . 3
β’ (π· β (PsMetβπ) β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π) |
24 | | xrex 12866 |
. . . 4
β’
β* β V |
25 | | xpexg 7676 |
. . . 4
β’ ((π β dom PsMet β§
β* β V) β (π Γ β*) β
V) |
26 | 15, 24, 25 | sylancl 586 |
. . 3
β’ (π· β (PsMetβπ) β (π Γ β*) β
V) |
27 | 15 | pwexd 5332 |
. . 3
β’ (π· β (PsMetβπ) β π« π β V) |
28 | | fex2 7862 |
. . 3
β’ (((π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π β§ (π Γ β*) β V β§
π« π β V)
β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) β V) |
29 | 23, 26, 27, 28 | syl3anc 1371 |
. 2
β’ (π· β (PsMetβπ) β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) β V) |
30 | 1, 12, 13, 29 | fvmptd2 6953 |
1
β’ (π· β (PsMetβπ) β (ballβπ·) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π})) |