Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) |
2 |
1
|
metdsf |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) ) |
3 |
2
|
3adant3 |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> F : X --> ( 0 [,] +oo ) ) |
4 |
|
ssel2 |
|- ( ( S C_ X /\ A e. S ) -> A e. X ) |
5 |
4
|
3adant1 |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> A e. X ) |
6 |
3 5
|
ffvelrnd |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) e. ( 0 [,] +oo ) ) |
7 |
|
eliccxr |
|- ( ( F ` A ) e. ( 0 [,] +oo ) -> ( F ` A ) e. RR* ) |
8 |
6 7
|
syl |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) e. RR* ) |
9 |
8
|
xrleidd |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) <_ ( F ` A ) ) |
10 |
|
simp1 |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> D e. ( *Met ` X ) ) |
11 |
|
simp2 |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> S C_ X ) |
12 |
1
|
metdsge |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ ( F ` A ) e. RR* ) -> ( ( F ` A ) <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) ) |
13 |
10 11 5 8 12
|
syl31anc |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( ( F ` A ) <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) ) |
14 |
9 13
|
mpbid |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) |
15 |
|
simpl3 |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> A e. S ) |
16 |
10
|
adantr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> D e. ( *Met ` X ) ) |
17 |
5
|
adantr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> A e. X ) |
18 |
8
|
adantr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> ( F ` A ) e. RR* ) |
19 |
|
simpr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> 0 < ( F ` A ) ) |
20 |
|
xblcntr |
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ ( ( F ` A ) e. RR* /\ 0 < ( F ` A ) ) ) -> A e. ( A ( ball ` D ) ( F ` A ) ) ) |
21 |
16 17 18 19 20
|
syl112anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> A e. ( A ( ball ` D ) ( F ` A ) ) ) |
22 |
|
inelcm |
|- ( ( A e. S /\ A e. ( A ( ball ` D ) ( F ` A ) ) ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) =/= (/) ) |
23 |
15 21 22
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) =/= (/) ) |
24 |
23
|
ex |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( 0 < ( F ` A ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) =/= (/) ) ) |
25 |
24
|
necon2bd |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) -> -. 0 < ( F ` A ) ) ) |
26 |
14 25
|
mpd |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> -. 0 < ( F ` A ) ) |
27 |
|
elxrge0 |
|- ( ( F ` A ) e. ( 0 [,] +oo ) <-> ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) ) |
28 |
27
|
simprbi |
|- ( ( F ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` A ) ) |
29 |
6 28
|
syl |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> 0 <_ ( F ` A ) ) |
30 |
|
0xr |
|- 0 e. RR* |
31 |
|
xrleloe |
|- ( ( 0 e. RR* /\ ( F ` A ) e. RR* ) -> ( 0 <_ ( F ` A ) <-> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) ) ) |
32 |
30 8 31
|
sylancr |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( 0 <_ ( F ` A ) <-> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) ) ) |
33 |
29 32
|
mpbid |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) ) |
34 |
33
|
ord |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( -. 0 < ( F ` A ) -> 0 = ( F ` A ) ) ) |
35 |
26 34
|
mpd |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> 0 = ( F ` A ) ) |
36 |
35
|
eqcomd |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) = 0 ) |