Step |
Hyp |
Ref |
Expression |
1 |
|
blf |
β’ ( π· β ( βMet β π ) β ( ball β π· ) : ( π Γ β* ) βΆ π« π ) |
2 |
1
|
ffnd |
β’ ( π· β ( βMet β π ) β ( ball β π· ) Fn ( π Γ β* ) ) |
3 |
|
fnovrn |
β’ ( ( ( ball β π· ) Fn ( π Γ β* ) β§ π β π β§ π
β β* ) β ( π ( ball β π· ) π
) β ran ( ball β π· ) ) |
4 |
2 3
|
syl3an1 |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π ( ball β π· ) π
) β ran ( ball β π· ) ) |