Step |
Hyp |
Ref |
Expression |
1 |
|
blval |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π ( ball β π· ) π
) = { π₯ β π β£ ( π π· π₯ ) < π
} ) |
2 |
1
|
eleq2d |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π΄ β ( π ( ball β π· ) π
) β π΄ β { π₯ β π β£ ( π π· π₯ ) < π
} ) ) |
3 |
|
oveq2 |
β’ ( π₯ = π΄ β ( π π· π₯ ) = ( π π· π΄ ) ) |
4 |
3
|
breq1d |
β’ ( π₯ = π΄ β ( ( π π· π₯ ) < π
β ( π π· π΄ ) < π
) ) |
5 |
4
|
elrab |
β’ ( π΄ β { π₯ β π β£ ( π π· π₯ ) < π
} β ( π΄ β π β§ ( π π· π΄ ) < π
) ) |
6 |
2 5
|
bitrdi |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π΄ β ( π ( ball β π· ) π
) β ( π΄ β π β§ ( π π· π΄ ) < π
) ) ) |