| Step |
Hyp |
Ref |
Expression |
| 1 |
|
blin2 |
β’ ( ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) ) β β π β β+ ( π§ ( ball β π· ) π ) β ( π₯ β© π¦ ) ) |
| 2 |
|
simpll |
β’ ( ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) ) β π· β ( βMet β π ) ) |
| 3 |
|
elinel1 |
β’ ( π§ β ( π₯ β© π¦ ) β π§ β π₯ ) |
| 4 |
|
elunii |
β’ ( ( π§ β π₯ β§ π₯ β ran ( ball β π· ) ) β π§ β βͺ ran ( ball β π· ) ) |
| 5 |
3 4
|
sylan |
β’ ( ( π§ β ( π₯ β© π¦ ) β§ π₯ β ran ( ball β π· ) ) β π§ β βͺ ran ( ball β π· ) ) |
| 6 |
5
|
ad2ant2lr |
β’ ( ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) ) β π§ β βͺ ran ( ball β π· ) ) |
| 7 |
|
unirnbl |
β’ ( π· β ( βMet β π ) β βͺ ran ( ball β π· ) = π ) |
| 8 |
7
|
ad2antrr |
β’ ( ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) ) β βͺ ran ( ball β π· ) = π ) |
| 9 |
6 8
|
eleqtrd |
β’ ( ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) ) β π§ β π ) |
| 10 |
|
blssex |
β’ ( ( π· β ( βMet β π ) β§ π§ β π ) β ( β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) β β π β β+ ( π§ ( ball β π· ) π ) β ( π₯ β© π¦ ) ) ) |
| 11 |
2 9 10
|
syl2anc |
β’ ( ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) ) β ( β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) β β π β β+ ( π§ ( ball β π· ) π ) β ( π₯ β© π¦ ) ) ) |
| 12 |
1 11
|
mpbird |
β’ ( ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) ) β β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) ) |
| 13 |
12
|
ex |
β’ ( ( π· β ( βMet β π ) β§ π§ β ( π₯ β© π¦ ) ) β ( ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) β β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) ) ) |
| 14 |
13
|
ralrimdva |
β’ ( π· β ( βMet β π ) β ( ( π₯ β ran ( ball β π· ) β§ π¦ β ran ( ball β π· ) ) β β π§ β ( π₯ β© π¦ ) β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) ) ) |
| 15 |
14
|
ralrimivv |
β’ ( π· β ( βMet β π ) β β π₯ β ran ( ball β π· ) β π¦ β ran ( ball β π· ) β π§ β ( π₯ β© π¦ ) β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) ) |
| 16 |
|
fvex |
β’ ( ball β π· ) β V |
| 17 |
16
|
rnex |
β’ ran ( ball β π· ) β V |
| 18 |
|
isbasis2g |
β’ ( ran ( ball β π· ) β V β ( ran ( ball β π· ) β TopBases β β π₯ β ran ( ball β π· ) β π¦ β ran ( ball β π· ) β π§ β ( π₯ β© π¦ ) β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) ) ) |
| 19 |
17 18
|
ax-mp |
β’ ( ran ( ball β π· ) β TopBases β β π₯ β ran ( ball β π· ) β π¦ β ran ( ball β π· ) β π§ β ( π₯ β© π¦ ) β π β ran ( ball β π· ) ( π§ β π β§ π β ( π₯ β© π¦ ) ) ) |
| 20 |
15 19
|
sylibr |
β’ ( π· β ( βMet β π ) β ran ( ball β π· ) β TopBases ) |