Step |
Hyp |
Ref |
Expression |
1 |
|
blin2 |
|- ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> E. r e. RR+ ( z ( ball ` D ) r ) C_ ( x i^i y ) ) |
2 |
|
simpll |
|- ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> D e. ( *Met ` X ) ) |
3 |
|
elinel1 |
|- ( z e. ( x i^i y ) -> z e. x ) |
4 |
|
elunii |
|- ( ( z e. x /\ x e. ran ( ball ` D ) ) -> z e. U. ran ( ball ` D ) ) |
5 |
3 4
|
sylan |
|- ( ( z e. ( x i^i y ) /\ x e. ran ( ball ` D ) ) -> z e. U. ran ( ball ` D ) ) |
6 |
5
|
ad2ant2lr |
|- ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> z e. U. ran ( ball ` D ) ) |
7 |
|
unirnbl |
|- ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X ) |
8 |
7
|
ad2antrr |
|- ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> U. ran ( ball ` D ) = X ) |
9 |
6 8
|
eleqtrd |
|- ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> z e. X ) |
10 |
|
blssex |
|- ( ( D e. ( *Met ` X ) /\ z e. X ) -> ( E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) <-> E. r e. RR+ ( z ( ball ` D ) r ) C_ ( x i^i y ) ) ) |
11 |
2 9 10
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> ( E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) <-> E. r e. RR+ ( z ( ball ` D ) r ) C_ ( x i^i y ) ) ) |
12 |
1 11
|
mpbird |
|- ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) |
13 |
12
|
ex |
|- ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) -> ( ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) -> E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) ) |
14 |
13
|
ralrimdva |
|- ( D e. ( *Met ` X ) -> ( ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) -> A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) ) |
15 |
14
|
ralrimivv |
|- ( D e. ( *Met ` X ) -> A. x e. ran ( ball ` D ) A. y e. ran ( ball ` D ) A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) |
16 |
|
fvex |
|- ( ball ` D ) e. _V |
17 |
16
|
rnex |
|- ran ( ball ` D ) e. _V |
18 |
|
isbasis2g |
|- ( ran ( ball ` D ) e. _V -> ( ran ( ball ` D ) e. TopBases <-> A. x e. ran ( ball ` D ) A. y e. ran ( ball ` D ) A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) ) |
19 |
17 18
|
ax-mp |
|- ( ran ( ball ` D ) e. TopBases <-> A. x e. ran ( ball ` D ) A. y e. ran ( ball ` D ) A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) |
20 |
15 19
|
sylibr |
|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) e. TopBases ) |