Step | Hyp | Ref
| Expression |
1 | | ssrab2 3242 |
. . . . . 6
β’ {π¦ β π β£ (π₯π·π¦) < π} β π |
2 | | xmetrel 13928 |
. . . . . . . 8
β’ Rel
βMet |
3 | | relelfvdm 5549 |
. . . . . . . 8
β’ ((Rel
βMet β§ π· β
(βMetβπ))
β π β dom
βMet) |
4 | 2, 3 | mpan 424 |
. . . . . . 7
β’ (π· β (βMetβπ) β π β dom βMet) |
5 | | elpw2g 4158 |
. . . . . . 7
β’ (π β dom βMet β
({π¦ β π β£ (π₯π·π¦) < π} β π« π β {π¦ β π β£ (π₯π·π¦) < π} β π)) |
6 | 4, 5 | syl 14 |
. . . . . 6
β’ (π· β (βMetβπ) β ({π¦ β π β£ (π₯π·π¦) < π} β π« π β {π¦ β π β£ (π₯π·π¦) < π} β π)) |
7 | 1, 6 | mpbiri 168 |
. . . . 5
β’ (π· β (βMetβπ) β {π¦ β π β£ (π₯π·π¦) < π} β π« π) |
8 | 7 | a1d 22 |
. . . 4
β’ (π· β (βMetβπ) β ((π₯ β π β§ π β β*) β {π¦ β π β£ (π₯π·π¦) < π} β π« π)) |
9 | 8 | ralrimivv 2558 |
. . 3
β’ (π· β (βMetβπ) β βπ₯ β π βπ β β* {π¦ β π β£ (π₯π·π¦) < π} β π« π) |
10 | | eqid 2177 |
. . . 4
β’ (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}) |
11 | 10 | fmpo 6204 |
. . 3
β’
(βπ₯ β
π βπ β β*
{π¦ β π β£ (π₯π·π¦) < π} β π« π β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π) |
12 | 9, 11 | sylib 122 |
. 2
β’ (π· β (βMetβπ) β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π) |
13 | | blfval 13971 |
. . 3
β’ (π· β (βMetβπ) β (ballβπ·) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π})) |
14 | 13 | feq1d 5354 |
. 2
β’ (π· β (βMetβπ) β ((ballβπ·):(π Γ
β*)βΆπ« π β (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π}):(π Γ
β*)βΆπ« π)) |
15 | 12, 14 | mpbird 167 |
1
β’ (π· β (βMetβπ) β (ballβπ·):(π Γ
β*)βΆπ« π) |