Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) |
2 |
|
simplll |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> D e. ( *Met ` X ) ) |
3 |
|
simplr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> x e. X ) |
4 |
|
simplr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> S C_ X ) |
5 |
4
|
sselda |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> y e. X ) |
6 |
|
xmetcl |
|- ( ( D e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) e. RR* ) |
7 |
2 3 5 6
|
syl3anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> ( x D y ) e. RR* ) |
8 |
|
eqid |
|- ( y e. S |-> ( x D y ) ) = ( y e. S |-> ( x D y ) ) |
9 |
7 8
|
fmptd |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> ( y e. S |-> ( x D y ) ) : S --> RR* ) |
10 |
9
|
frnd |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> ran ( y e. S |-> ( x D y ) ) C_ RR* ) |
11 |
|
infxrcl |
|- ( ran ( y e. S |-> ( x D y ) ) C_ RR* -> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. RR* ) |
12 |
10 11
|
syl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. RR* ) |
13 |
|
xmetge0 |
|- ( ( D e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> 0 <_ ( x D y ) ) |
14 |
2 3 5 13
|
syl3anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> 0 <_ ( x D y ) ) |
15 |
14
|
ralrimiva |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> A. y e. S 0 <_ ( x D y ) ) |
16 |
|
ovex |
|- ( x D y ) e. _V |
17 |
16
|
rgenw |
|- A. y e. S ( x D y ) e. _V |
18 |
|
breq2 |
|- ( z = ( x D y ) -> ( 0 <_ z <-> 0 <_ ( x D y ) ) ) |
19 |
8 18
|
ralrnmptw |
|- ( A. y e. S ( x D y ) e. _V -> ( A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z <-> A. y e. S 0 <_ ( x D y ) ) ) |
20 |
17 19
|
ax-mp |
|- ( A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z <-> A. y e. S 0 <_ ( x D y ) ) |
21 |
15 20
|
sylibr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z ) |
22 |
|
0xr |
|- 0 e. RR* |
23 |
|
infxrgelb |
|- ( ( ran ( y e. S |-> ( x D y ) ) C_ RR* /\ 0 e. RR* ) -> ( 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) <-> A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z ) ) |
24 |
10 22 23
|
sylancl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> ( 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) <-> A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z ) ) |
25 |
21 24
|
mpbird |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) |
26 |
|
elxrge0 |
|- ( inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. ( 0 [,] +oo ) <-> ( inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. RR* /\ 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) ) |
27 |
12 25 26
|
sylanbrc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. ( 0 [,] +oo ) ) |
28 |
27 1
|
fmptd |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) ) |