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 |
|
metnrmlem.1 |
|- ( ph -> D e. ( *Met ` X ) ) |
4 |
|
metnrmlem.2 |
|- ( ph -> S e. ( Clsd ` J ) ) |
5 |
|
metnrmlem.3 |
|- ( ph -> T e. ( Clsd ` J ) ) |
6 |
|
metnrmlem.4 |
|- ( ph -> ( S i^i T ) = (/) ) |
7 |
|
1xr |
|- 1 e. RR* |
8 |
3
|
adantr |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> D e. ( *Met ` X ) ) |
9 |
4
|
adantr |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> S e. ( Clsd ` J ) ) |
10 |
|
eqid |
|- U. J = U. J |
11 |
10
|
cldss |
|- ( S e. ( Clsd ` J ) -> S C_ U. J ) |
12 |
9 11
|
syl |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> S C_ U. J ) |
13 |
2
|
mopnuni |
|- ( D e. ( *Met ` X ) -> X = U. J ) |
14 |
8 13
|
syl |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> X = U. J ) |
15 |
12 14
|
sseqtrrd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> S C_ X ) |
16 |
1
|
metdsf |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) ) |
17 |
8 15 16
|
syl2anc |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> F : X --> ( 0 [,] +oo ) ) |
18 |
5
|
adantr |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> T e. ( Clsd ` J ) ) |
19 |
10
|
cldss |
|- ( T e. ( Clsd ` J ) -> T C_ U. J ) |
20 |
18 19
|
syl |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> T C_ U. J ) |
21 |
20 14
|
sseqtrrd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> T C_ X ) |
22 |
|
simprr |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> B e. T ) |
23 |
21 22
|
sseldd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> B e. X ) |
24 |
17 23
|
ffvelrnd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) e. ( 0 [,] +oo ) ) |
25 |
|
eliccxr |
|- ( ( F ` B ) e. ( 0 [,] +oo ) -> ( F ` B ) e. RR* ) |
26 |
24 25
|
syl |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) e. RR* ) |
27 |
|
ifcl |
|- ( ( 1 e. RR* /\ ( F ` B ) e. RR* ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) e. RR* ) |
28 |
7 26 27
|
sylancr |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) e. RR* ) |
29 |
|
simprl |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> A e. S ) |
30 |
15 29
|
sseldd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> A e. X ) |
31 |
|
xmetcl |
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* ) |
32 |
8 30 23 31
|
syl3anc |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( A D B ) e. RR* ) |
33 |
|
xrmin2 |
|- ( ( 1 e. RR* /\ ( F ` B ) e. RR* ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( F ` B ) ) |
34 |
7 26 33
|
sylancr |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( F ` B ) ) |
35 |
1
|
metdstri |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( B e. X /\ A e. X ) ) -> ( F ` B ) <_ ( ( B D A ) +e ( F ` A ) ) ) |
36 |
8 15 23 30 35
|
syl22anc |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) <_ ( ( B D A ) +e ( F ` A ) ) ) |
37 |
|
xmetsym |
|- ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) -> ( B D A ) = ( A D B ) ) |
38 |
8 23 30 37
|
syl3anc |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( B D A ) = ( A D B ) ) |
39 |
1
|
metds0 |
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) = 0 ) |
40 |
8 15 29 39
|
syl3anc |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` A ) = 0 ) |
41 |
38 40
|
oveq12d |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( ( B D A ) +e ( F ` A ) ) = ( ( A D B ) +e 0 ) ) |
42 |
32
|
xaddid1d |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( ( A D B ) +e 0 ) = ( A D B ) ) |
43 |
41 42
|
eqtrd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( ( B D A ) +e ( F ` A ) ) = ( A D B ) ) |
44 |
36 43
|
breqtrd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) <_ ( A D B ) ) |
45 |
28 26 32 34 44
|
xrletrd |
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( A D B ) ) |