Step | Hyp | Ref
| Expression |
1 | | df-bl 13420 |
. . 3
β’ ball =
(π β V β¦ (π₯ β dom dom π, π β β* β¦ {π¦ β dom dom π β£ (π₯ππ¦) < π})) |
2 | 1 | a1i 9 |
. 2
β’ (π· β (PsMetβπ) β ball = (π β V β¦ (π₯ β dom dom π, π β β* β¦ {π¦ β dom dom π β£ (π₯ππ¦) < π}))) |
3 | | dmeq 4827 |
. . . . 5
β’ (π = π· β dom π = dom π·) |
4 | 3 | dmeqd 4829 |
. . . 4
β’ (π = π· β dom dom π = dom dom π·) |
5 | | psmetdmdm 13794 |
. . . . 5
β’ (π· β (PsMetβπ) β π = dom dom π·) |
6 | 5 | eqcomd 2183 |
. . . 4
β’ (π· β (PsMetβπ) β dom dom π· = π) |
7 | 4, 6 | sylan9eqr 2232 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = π) |
8 | | eqidd 2178 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β β* =
β*) |
9 | | simpr 110 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π = π·) β π = π·) |
10 | 9 | oveqd 5891 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β (π₯ππ¦) = (π₯π·π¦)) |
11 | 10 | breq1d 4013 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β ((π₯ππ¦) < π β (π₯π·π¦) < π)) |
12 | 7, 11 | rabeqbidv 2732 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β {π¦ β dom dom π β£ (π₯ππ¦) < π} = {π¦ β π β£ (π₯π·π¦) < π}) |
13 | 7, 8, 12 | mpoeq123dv 5936 |
. 2
β’ ((π· β (PsMetβπ) β§ π = π·) β (π₯ β dom dom π, π β β* β¦ {π¦ β dom dom π β£ (π₯ππ¦) < π}) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π})) |
14 | | elex 2748 |
. 2
β’ (π· β (PsMetβπ) β π· β V) |
15 | | ssrab2 3240 |
. . . . . 6
β’ {π¦ β π β£ (π₯π·π¦) < π} β π |
16 | | psmetrel 13792 |
. . . . . . . . 9
β’ Rel
PsMet |
17 | | relelfvdm 5547 |
. . . . . . . . 9
β’ ((Rel
PsMet β§ π· β
(PsMetβπ)) β
π β dom
PsMet) |
18 | 16, 17 | mpan 424 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β π β dom PsMet) |
19 | 18 | adantr 276 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π β β*)) β π β dom
PsMet) |
20 | | elpw2g 4156 |
. . . . . . 7
β’ (π β dom PsMet β ({π¦ β π β£ (π₯π·π¦) < π} β π« π β {π¦ β π β£ (π₯π·π¦) < π} β π)) |
21 | 19, 20 | syl 14 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π β β*)) β ({π¦ β π β£ (π₯π·π¦) < π} β π« π β {π¦ β π β£ (π₯π·π¦) < π} β π)) |
22 | 15, 21 | mpbiri 168 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π β β*)) β {π¦ β π β£ (π₯π·π¦) < π} β π« π) |
23 | 22 | ralrimivva 2559 |
. . . 4
β’ (π· β (PsMetβπ) β βπ₯ β π βπ β β* {π¦ β π β£ (π₯π·π¦) < π} β π« π) |
24 | | eqid 2177 |
. . . . 5
β’ (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) |
25 | 24 | fmpo 6201 |
. . . 4
β’
(βπ₯ β
π βπ β β*
{π¦ β π β£ (π₯π·π¦) < π} β π« π β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π) |
26 | 23, 25 | sylib 122 |
. . 3
β’ (π· β (PsMetβπ) β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π) |
27 | | xrex 9855 |
. . . 4
β’
β* β V |
28 | | xpexg 4740 |
. . . 4
β’ ((π β dom PsMet β§
β* β V) β (π Γ β*) β
V) |
29 | 18, 27, 28 | sylancl 413 |
. . 3
β’ (π· β (PsMetβπ) β (π Γ β*) β
V) |
30 | 18 | pwexd 4181 |
. . 3
β’ (π· β (PsMetβπ) β π« π β V) |
31 | | fex2 5384 |
. . 3
β’ (((π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π β§ (π Γ β*) β V β§
π« π β V)
β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) β V) |
32 | 26, 29, 30, 31 | syl3anc 1238 |
. 2
β’ (π· β (PsMetβπ) β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) β V) |
33 | 2, 13, 14, 32 | fvmptd 5597 |
1
β’ (π· β (PsMetβπ) β (ballβπ·) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π})) |