Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) |
2 |
|
n0 |
|- ( S =/= (/) <-> E. z z e. S ) |
3 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
4 |
1
|
metdsf |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) ) |
5 |
3 4
|
sylan |
|- ( ( D e. ( Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) ) |
6 |
5
|
adantr |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> F : X --> ( 0 [,] +oo ) ) |
7 |
6
|
ffnd |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> F Fn X ) |
8 |
5
|
adantr |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> F : X --> ( 0 [,] +oo ) ) |
9 |
|
simprr |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> w e. X ) |
10 |
8 9
|
ffvelrnd |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) e. ( 0 [,] +oo ) ) |
11 |
|
eliccxr |
|- ( ( F ` w ) e. ( 0 [,] +oo ) -> ( F ` w ) e. RR* ) |
12 |
10 11
|
syl |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) e. RR* ) |
13 |
|
simpll |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> D e. ( Met ` X ) ) |
14 |
|
simpr |
|- ( ( D e. ( Met ` X ) /\ S C_ X ) -> S C_ X ) |
15 |
14
|
sselda |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> z e. X ) |
16 |
15
|
adantrr |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> z e. X ) |
17 |
|
metcl |
|- ( ( D e. ( Met ` X ) /\ z e. X /\ w e. X ) -> ( z D w ) e. RR ) |
18 |
13 16 9 17
|
syl3anc |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( z D w ) e. RR ) |
19 |
|
elxrge0 |
|- ( ( F ` w ) e. ( 0 [,] +oo ) <-> ( ( F ` w ) e. RR* /\ 0 <_ ( F ` w ) ) ) |
20 |
19
|
simprbi |
|- ( ( F ` w ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` w ) ) |
21 |
10 20
|
syl |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> 0 <_ ( F ` w ) ) |
22 |
1
|
metdsle |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) <_ ( z D w ) ) |
23 |
3 22
|
sylanl1 |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) <_ ( z D w ) ) |
24 |
|
xrrege0 |
|- ( ( ( ( F ` w ) e. RR* /\ ( z D w ) e. RR ) /\ ( 0 <_ ( F ` w ) /\ ( F ` w ) <_ ( z D w ) ) ) -> ( F ` w ) e. RR ) |
25 |
12 18 21 23 24
|
syl22anc |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) e. RR ) |
26 |
25
|
anassrs |
|- ( ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) /\ w e. X ) -> ( F ` w ) e. RR ) |
27 |
26
|
ralrimiva |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> A. w e. X ( F ` w ) e. RR ) |
28 |
|
ffnfv |
|- ( F : X --> RR <-> ( F Fn X /\ A. w e. X ( F ` w ) e. RR ) ) |
29 |
7 27 28
|
sylanbrc |
|- ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> F : X --> RR ) |
30 |
29
|
ex |
|- ( ( D e. ( Met ` X ) /\ S C_ X ) -> ( z e. S -> F : X --> RR ) ) |
31 |
30
|
exlimdv |
|- ( ( D e. ( Met ` X ) /\ S C_ X ) -> ( E. z z e. S -> F : X --> RR ) ) |
32 |
2 31
|
syl5bi |
|- ( ( D e. ( Met ` X ) /\ S C_ X ) -> ( S =/= (/) -> F : X --> RR ) ) |
33 |
32
|
3impia |
|- ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F : X --> RR ) |