Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) |
2 |
|
metdscn.j |
|- J = ( MetOpen ` D ) |
3 |
|
metdscn.c |
|- C = ( dist ` RR*s ) |
4 |
|
metdscn.k |
|- K = ( MetOpen ` C ) |
5 |
1
|
metdsf |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) ) |
6 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
7 |
|
fss |
|- ( ( F : X --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : X --> RR* ) |
8 |
5 6 7
|
sylancl |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> RR* ) |
9 |
|
simprr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) -> r e. RR+ ) |
10 |
8
|
ad2antrr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> F : X --> RR* ) |
11 |
|
simplrl |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> z e. X ) |
12 |
10 11
|
ffvelrnd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( F ` z ) e. RR* ) |
13 |
|
simprl |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> w e. X ) |
14 |
10 13
|
ffvelrnd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( F ` w ) e. RR* ) |
15 |
3
|
xrsdsval |
|- ( ( ( F ` z ) e. RR* /\ ( F ` w ) e. RR* ) -> ( ( F ` z ) C ( F ` w ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) ) |
16 |
12 14 15
|
syl2anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` z ) C ( F ` w ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) ) |
17 |
|
simplll |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> D e. ( *Met ` X ) ) |
18 |
|
simpllr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> S C_ X ) |
19 |
|
simplrr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> r e. RR+ ) |
20 |
|
xmetsym |
|- ( ( D e. ( *Met ` X ) /\ w e. X /\ z e. X ) -> ( w D z ) = ( z D w ) ) |
21 |
17 13 11 20
|
syl3anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( w D z ) = ( z D w ) ) |
22 |
|
simprr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( z D w ) < r ) |
23 |
21 22
|
eqbrtrd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( w D z ) < r ) |
24 |
1 2 3 4 17 18 13 11 19 23
|
metdscnlem |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` w ) +e -e ( F ` z ) ) < r ) |
25 |
1 2 3 4 17 18 11 13 19 22
|
metdscnlem |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` z ) +e -e ( F ` w ) ) < r ) |
26 |
|
breq1 |
|- ( ( ( F ` w ) +e -e ( F ` z ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) -> ( ( ( F ` w ) +e -e ( F ` z ) ) < r <-> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r ) ) |
27 |
|
breq1 |
|- ( ( ( F ` z ) +e -e ( F ` w ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) -> ( ( ( F ` z ) +e -e ( F ` w ) ) < r <-> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r ) ) |
28 |
26 27
|
ifboth |
|- ( ( ( ( F ` w ) +e -e ( F ` z ) ) < r /\ ( ( F ` z ) +e -e ( F ` w ) ) < r ) -> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r ) |
29 |
24 25 28
|
syl2anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r ) |
30 |
16 29
|
eqbrtrd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` z ) C ( F ` w ) ) < r ) |
31 |
30
|
expr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ w e. X ) -> ( ( z D w ) < r -> ( ( F ` z ) C ( F ` w ) ) < r ) ) |
32 |
31
|
ralrimiva |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) -> A. w e. X ( ( z D w ) < r -> ( ( F ` z ) C ( F ` w ) ) < r ) ) |
33 |
|
breq2 |
|- ( s = r -> ( ( z D w ) < s <-> ( z D w ) < r ) ) |
34 |
33
|
rspceaimv |
|- ( ( r e. RR+ /\ A. w e. X ( ( z D w ) < r -> ( ( F ` z ) C ( F ` w ) ) < r ) ) -> E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) ) |
35 |
9 32 34
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) -> E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) ) |
36 |
35
|
ralrimivva |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> A. z e. X A. r e. RR+ E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) ) |
37 |
|
simpl |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> D e. ( *Met ` X ) ) |
38 |
3
|
xrsxmet |
|- C e. ( *Met ` RR* ) |
39 |
2 4
|
metcn |
|- ( ( D e. ( *Met ` X ) /\ C e. ( *Met ` RR* ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> RR* /\ A. z e. X A. r e. RR+ E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) ) ) ) |
40 |
37 38 39
|
sylancl |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( F e. ( J Cn K ) <-> ( F : X --> RR* /\ A. z e. X A. r e. RR+ E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) ) ) ) |
41 |
8 36 40
|
mpbir2and |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F e. ( J Cn K ) ) |